Software Behavior Synthesis (Draft)

Early system requirements are often captured by declarative and property-based artifacts, such as scenarios and goals. While such artifacts are intuitive and useful, they are partial and typically lack an overarching structure to allow systematic elaboration of the partial behaviors they denote. We propose a structuring approach appropriate for scoping different partial behaviors, focusing on scenario-based behavior specifications. The approach is based on Parnas ’ notions of ‘modes ’ and ‘mode-classes’, where a mode is a set of states that satisfy some predicate, and a mode-class is a collection of disjoint modes that partitions the system’s state-space so that each state belongs to exactly one mode. There may be several mode-classes, in which case every state belongs to exactly one mode from each mode-class. We structure a scenario by partitioning its observed states into modes, allowing elaboration of the scenario’s parts independently without losing the overall system view. Having every scenario partitioned via a suitable mode-class, w