Smart Play-Out Extended: Time and Forbidden Elements

Smart play-out is a powerful technique for executing live sequence charts (LSCs). It uses verification techniques to help run a program, rather than to prove properties thereof. In this paper we extend smart play-out to cover a larger set of the LSC language features and to deal more efficiently with larger models. The extensions cover two key features of the rich version of LSCs, namely, time and forbidden elements. The former is crucial for systems with time constraints and/or time-driven behavior, and the latter allows specifying invariants and contracts on behavior. Forbidden elements can also help reduce the state space considered, thus enabling smart play-out to handle larger models.