Consistency checking scenario-based specifications of dynamic systems by combining simulation and synthesis

Modern technical systems often consist of multiple components that must fulfill complex functions in diverse and sometimes safety-critical situations. Precisely specifying the behavioral requirements for such systems is a challenge, especially because there may be inconsistent requirements in possibly unforeseen component configurations. We propose a scenario-based specification approach based on Modal Sequence Diagrams and a novel technique for finding inconsistencies in such specification based on a combination of simulation and synthesis techniques. The simulation via the play-out algorithm can be used to analyze the scenario requirements in large and dynamic systems. Play-out, however, may run into avoidable violations, so that the engineer cannot assume the specification's inconsistency nor its consistency. We thus propose to check specification parts for static component configurations via synthesis. Then, if the part specifications are consistent, the resulting controllers can guide the play-out for the complete specification, avoiding more avoidable violations in the next simulation run.