Local mirror of the Archive of Formal Proof (AFP) entry "DOM_Components".
Nevar pievienot vairāk kā 25 tēmas Tēmai ir jāsākas ar burtu vai ciparu, tā var saturēt domu zīmes ('-') un var būt līdz 35 simboliem gara.
 
 
 

87 rindas
5.0 KiB

  1. To cite the use of this formal theory, please use
  2. Achim D. Brucker and Michael Herzberg. A Formalization of Web Components. In Archive of
  3. Formal Proofs, 2020. http://www.isa-afp.org/entries/DOM_Components.html,
  4. Formal proof development
  5. A BibTeX entry for LaTeX users is
  6. @Article{ brucker.ea:afp-dom-components:2020,
  7. author = {Achim D. Brucker and Michael Herzberg},
  8. title = {A Formalization of Web Components},
  9. journal = {Archive of Formal Proofs},
  10. month = sep,
  11. year = 2020,
  12. date = {2020-09-28},
  13. note = {\url{http://www.isa-afp.org/entries/DOM_Components.html}, Formal proof development},
  14. issn = {2150-914x},
  15. public = {yes},
  16. classification= {formal},
  17. categories = {websecurity},
  18. pdf = {http://www.brucker.ch/bibliography/download/2020/brucker.ea-afp-dom-components-2020.pdf},
  19. filelabel = {Outline},
  20. file = {http://www.brucker.ch/bibliography/download/2020/brucker.ea-afp-dom-components-outline-2020.pdf},
  21. areas = {formal methods, security, software engineering},
  22. abstract = { While the DOM with shadow trees provide the technical basis for defining web components, the DOM
  23. standard neither defines the concept of web components nor specifies the safety properties that web
  24. components should guarantee. Consequently, the standard also does not discuss how or even if the
  25. methods for modifying the DOM respect component boundaries.
  26. In AFP entry, we present a formally verified model of web components and define safety properties
  27. which ensure that different web components can only interact with each other using well-defined
  28. interfaces. Moreover, our verification of the application programming interface (API) of the DOM
  29. revealed numerous invariants that implementations of the DOM API need to preserve to ensure the
  30. integrity of components. },
  31. url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-afp-dom-components-2020}
  32. }
  33. An overview of the formalization is given in:
  34. Achim D. Brucker and Michael Herzberg. A Formally Verified Model of
  35. Web Components. In Formal Aspects of Component Software (FACS).
  36. Lecture Notes in Computer Science (12018), Springer-Verlag, 2020.
  37. http://www.brucker.ch/bibliography/abstract/brucker.ea-web-components-2019
  38. A BibTeX entry for LaTeX users is
  39. @InCollection{ brucker.ea:web-components:2019,
  40. abstract = {The trend towards ever more complex client-side web applications is unstoppable. Compared to
  41. traditional software development, client-side web development lacks a well-established component
  42. model, i.e., a method for easily and safely reusing already developed functionality. To address this
  43. issue, the web community started to adopt shadow trees as part of the Document Object Model (DOM):
  44. shadow trees allow developers to "partition" a DOM instance into parts that should be safely
  45. separated, e.g., code modifying one part should not, unintentionally, affect other parts of the DOM.
  46. While shadow trees provide the technical basis for defining web components, the DOM standard neither
  47. defines the concept of web components nor specifies the safety properties that web components should
  48. guarantee. Consequently, the standard also does not discuss how or even if the methods for modifying
  49. the DOM respect component boundaries. In this paper, we present a formally verified model of web
  50. components and define safety properties which ensure that different web components can only interact
  51. with each other using well-defined interfaces. Moreover, our verification of the application
  52. programming interface (API) of the DOM revealed numerous invariants that implementations of the DOM
  53. API need to preserve to ensure the integrity of components.},
  54. keywords = {Web Component, Shadow Tree, DOM, Isabelle/HOL},
  55. location = {Amsterdam, The Netherlands},
  56. author = {Achim D. Brucker and Michael Herzberg},
  57. booktitle = {Formal Aspects of Component Software (FACS)},
  58. language = {USenglish},
  59. publisher = pub-springer,
  60. address = pub-springer:adr,
  61. series = s-lncs,
  62. number = 12018,
  63. isbn = {3-540-25109-X},
  64. doi = {10.1007/978-3-030-40914-2_3},
  65. editor = {Sung-Shik Jongmans and Farhad Arbab},
  66. pdf = {http://www.brucker.ch/bibliography/download/2019/brucker.ea-web-components-2019.pdf},
  67. title = {A Formally Verified Model of Web Components},
  68. classification= {conference},
  69. areas = {formal methods, software},
  70. year = 2020,
  71. public = {yes},
  72. url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-web-components-2019}
  73. }