Paper Info
Title
Compositional Synthesis of Controllers from Scenario-Based Assume-Guarantee Specifications.
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.
Year
DOI
Venue
2013
10.1007/978-3-642-41533-3_47
Lecture Notes in Computer Science
Keywords
Field
DocType
Scenario-Based Specification,Compositional Controller Synthesis,Consistency Checking,Assume-Guarantee
Formal synthesis,Sequence diagram,Programming language,Computer science,Correctness,Theoretical computer science,Formalism (philosophy),Technical systems,Modal,Reliability engineering
Conference
Volume
ISSN
Citations 
8107
0302-9743
2
PageRank 
References 
Authors
0.39
13
2
Name
Order
Citations
PageRank
Joel Greenyer122420.36
Ekkart Kindler21219105.52