Assume-guarantee scenarios: Semantics and synthesis

Abstract

The behavior of open reactive systems is best described in an assume-guarantee style specification: a system guarantees certain prescribed behavior provided that its environment follows certain given assumptions. Scenario-based modeling languages, such as variants of message sequence charts, have been used to specify reactive systems behavior in a visual, modular, intuitive way. However, none have yet provided full support for assume-guarantee style specifications. In this paper we present assume-guarantee scenarios, which extend live sequence charts (lsc) - a visual, expressive, scenario-based language - syntax and semantics, with an explicit distinction between system and environment entities and with support not only for safety and liveness system guarantees but also for safety and liveness environment assumptions. Moreover, the semantics is defined using a reduction to gr(1), a fragment of ltl that enables game-based, symbolic, efficient synthesis of a correct-by-construction controller. © 2012 Springer-Verlag.