Compositional Synthesis of Controllers from Scenario-Based Assume-Guarantee Specifications

Joel Greenyer, Ekkart Kindler

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review


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 languageEnglish
Title of host publicationModel-Driven Engineering Languages and Systems : 16th International Conference, MODELS 2013, Miami, FL, USA, September 29 – October 4, 2013. Proceedings
Publication date2013
ISBN (Print)978-3-642-41532-6
ISBN (Electronic)978-3-642-41533-3
Publication statusPublished - 2013
Event16th International Conference on Model Driven Engineering Languages and Systems (MODELS 2013) - Miami, Florida, United States
Duration: 29 Sept 20134 Oct 2013


Conference16th International Conference on Model Driven Engineering Languages and Systems (MODELS 2013)
Country/TerritoryUnited States
CityMiami, Florida
Internet address
SeriesLecture Notes in Computer Science


  • Scenario-Based Specification
  • Compositional Controller Synthesis
  • Consistency Checking
  • Assume-Guarantee


Dive into the research topics of 'Compositional Synthesis of Controllers from Scenario-Based Assume-Guarantee Specifications'. Together they form a unique fingerprint.

Cite this