Compositional Verification using Model Checking and Theorem Proving

Collaborative embedded systems form groups in which individual systems collaborate to achieve an overall goal. To this end, new systems may join a group and participating systems can leave the group. Classical techniques for the formal modeling and analysis of distributed systems, however, are mainly based on a static notion of systems and thus are often not well suited for the modeling and analysis of collaborative embedded systems. In this chapter, we propose an alternative approach that allows for the verification of dynamically evolving systems and we demonstrate it in terms of a running example: a simple version of an adaptable and flexible factory.

Authors and Affiliations

1. Technical University of Munich, München, Germany

   Diego Marmsoler

Editors and Affiliations

1. Fakultät für Informatik, Technische Universität München, Garching, Germany

   Wolfgang Böhm

2. Fakultät für Informatik, Technische Universität München, Garching, Germany

   Manfred Broy

3. Corporate Technology, CT RDA SSI, Siemens AG, München, Germany

   Cornel Klein

4. Software Systems Engineering, University of Duisburg-Essen, Essen, Germany

   Klaus Pohl

5. Lehrstuhl Software Engineering, RWTH Aachen University, Aachen, Germany

   Bernhard Rumpe

6. Assembly Technique (CR/APA1), Robert Bosch (Germany), Renningen, Germany

   Sebastian Schröck

Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

Reprints and permissions

© 2021 The Author(s)

Policies and ethics