TY - CHAP AU - Brucker, Achim D. AU - Herzberg, Michael ED - Jongmans, Sung-Shik ED - Arbab, Farhad PY - 2020 DA - 2020// TI - A Formally Verified Model of Web Components BT - Formal Aspects of Component Software (FACS) T3 - Lecture Notes in Computer Science IS - 12018 PB - Springer-Verlag CY - Heidelberg KW - Web Component, Shadow Tree, DOM, Isabelle/HOL AB - The trend towards ever more complex client-side web applications is unstoppable. Compared to traditional software development, client-side web development lacks a well-established component model, i.e., a method for easily and safely reusing already developed functionality. To address this issue, the web community started to adopt shadow trees as part of the Document Object Model (DOM): shadow trees allow developers to ”partition” a DOM instance into parts that should be safely separated, e.g., code modifying one part should not, unintentionally, affect other parts of the DOM. While shadow trees provide the technical basis for defining web components, the DOM standard neither defines the concept of web components nor specifies the safety properties that web components should guarantee. Consequently, the standard also does not discuss how or even if the methods for modifying the DOM respect component boundaries. In this paper, we present a formally verified model of web components and define safety properties which ensure that different web components can only interact with each other using well-defined interfaces. Moreover, our verification of the application programming interface (API) of the DOM revealed numerous invariants that implementations of the DOM API need to preserve to ensure the integrity of components. SN - 3-540-25109-X L1 - https://www.brucker.ch/bibliography/download/2019/brucker.ea-web-components-2019.pdf UR - https://www.brucker.ch/bibliography/abstract/brucker.ea-web-components-2019 UR - https://doi.org/10.1007/978-3-030-40914-2_3 DO - 10.1007/978-3-030-40914-2_3 LA - USenglish ID - brucker.ea:web-components:2019 ER -