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 speci-fications, 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 pa-per, 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) necessar-ily provide the behavior required by the scenarios, (2) re-strict 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 elicita-tion, and help select off-the-shelf components.