From system specifications to component behavioral models

Early system specifications, such as use-case scenarios and properties, rarely completely specify the system. Partial models of system-level behavior, derived from these specifications, have proven useful in early system analysis. We believe that the scope of possible analyses can be enhanced by utilizing component-level partial models. In this paper, we outline an algorithm for deriving a component-level Modal Transition System (MTS) from system-level scenario and property specifications. The generated MTSs capture the possible component implementations that (1) necessarily provide the behavior required by the scenarios, (2) restrict behavior forbidden by the properties, and (3) leave the behavior that is neither explicitly required nor forbidden as undefined. We discuss how these generated models can help discover system-design flaws, support requirements elicitation, and help select off-the-shelf components.