Abstract
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.
Original language | English |
---|---|
Title of host publication | Model-Driven Engineering Languages and Systems : 16th International Conference, MODELS 2013, Miami, FL, USA, September 29 – October 4, 2013. Proceedings |
Publisher | Springer |
Publication date | 2013 |
Pages | 774-789 |
ISBN (Print) | 978-3-642-41532-6 |
ISBN (Electronic) | 978-3-642-41533-3 |
DOIs | |
Publication status | Published - 2013 |
Event | 16th International Conference on Model Driven Engineering Languages and Systems (MODELS 2013) - Miami, Florida, United States Duration: 29 Sept 2013 → 4 Oct 2013 http://models2013.lcc.uma.es/ |
Conference
Conference | 16th International Conference on Model Driven Engineering Languages and Systems (MODELS 2013) |
---|---|
Country/Territory | United States |
City | Miami, Florida |
Period | 29/09/2013 → 04/10/2013 |
Internet address |
Series | Lecture Notes in Computer Science |
---|---|
Volume | 8107 |
ISSN | 0302-9743 |
Keywords
- Scenario-Based Specification
- Compositional Controller Synthesis
- Consistency Checking
- Assume-Guarantee