Abstract
Live Sequence Charts (LSCs) is a visual requirements language for specifying reactive system behavior. When modeling and designing open reactive systems, it is often essential to have a guarantee that the requirements can be satisfied under all possible circumstances. We apply results in the area of controller synthesis to a subset of the LSC language to decide the realizability of LSC requirements. If realizable, we show how to generate system responses that are guaranteed to satisfy the requirements. We discuss one particular implementation of this result which is formulated as an extension of smart play-out, a method for direct execution of scenario-based requirements.
Cite
CITATION STYLE
Kugler, H., Plock, C., & Pnueli, A. (2009). Controller synthesis from LSC requirements. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5503, pp. 79–93). https://doi.org/10.1007/978-3-642-00593-0_6
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
