Conference paper
Compositional Synthesis of Controllers from Scenario-Based Assume-Guarantee Specifications
Modern software-intensive systems often consist of multiple components that interact to fulfill complex functions in sometimes safety-critical situations. During the design, it is crucial to specify the system's requirements formally and to detect inconsistencies as early as possible in order to avoid flaws in the product or costly iterations during its development.
We propose to use Modal Sequence Diagrams (MSDs), a formal, yet intuitive formalism for specifying the interaction of a system with its environment, and developed a formal synthesis approach that allows us to detect inconsistencies and even to automatically synthesize controllers from MSD specifications.
The technique is suited for specifications of technical systems with real-time constraints and environment assumptions. However, synthesis is computationally expensive. In order to employ synthesis also for larger specifications, we present, in this paper, a novel assume-guarantee-style compositional synthesis technique for MSD specifications.
We provide evaluation results underlining the benefit of our approach and formally justify its correctness.
Language: | English |
---|---|
Publisher: | Springer |
Year: | 2013 |
Pages: | 774-789 |
Proceedings: | 16th International Conference on Model Driven Engineering Languages and Systems (MODELS 2013)ACM/IEEE International Conference on Model Driven Engineering Languages and Systems |
Series: | Lecture Notes in Computer Science |
Journal subtitle: | 16th International Conference, Models 2013, Miami, Fl, Usa, September 29 – October 4, 2013. Proceedings |
ISBN: | 3642415326 , 3642415334 , 9783642415326 and 9783642415333 |
ISSN: | 03029743 |
Types: | Conference paper |
DOI: | 10.1007/978-3-642-41533-3_47 |
ORCIDs: | Kindler, Ekkart |