MOVE FROM COMPOSITE outlines this procedure. The only technical difference, compared to REFINETOREQUIRED, is an interactive query, which asks an engineer to select individual models that should be refined (line 5 in REMOVE FROM COMPOSITE). We suggest three ways of presenting the refinement choices to an engineer.
First, we present a list of candidate individual models. Second, we display the individual models and mark the transitions whose removal would realize the composite refinement. Third, we display the composite MTS, while annotating transitions that would be removed after refining the candidate model transitions. The different presentation choices assure that an engineer can thoroughly explore the implications of removing a transition from a composite model.
Our solution depicted in Figure 6 extensively uses the state mapping relation to discover and propagate the implications of a composite model transition refinement. Additionally, the mapping relation allows us to propagate the refinements of individual models back to the composition (lines 5-7 in REFINETOREQUIRED and lines 6-9 in REMOVEFROMCOMPOSITE), without re-composing the individual MTSs. The proposed solution is general because
it allows any transition refinement of an individual model, while a transition refinement in a composite model results in additional refinements only when they are necessary to maintain consistency.
Defines standard
Replaced/Superseded by document(s)
Cancelled by
Amended by
| File | MIME type | Size (KB) | Language | Download | |
|---|---|---|---|---|---|
| usc-csse-2010-510.pdf | application/pdf | 470.52 KB | English | DOWNLOAD! |
Provides definitions
Abstract
During requirements elicitation and preliminary design, a system’s
behavior is typically partially specified: some behavior is defined
as either forbidden or required, while other behavior is not yet categorized as either of those. The goal is then to gradually refine the specification and finally arrive at a complete behavioral description. Partial-behavior modeling formalisms, such as Modal Transition Systems, can support such gradual refinement. However, several challenges still remain, particularly in the context of hierarchical architectural specifications where (sub)system models are composed of smaller subsystems and components, and, in turn, abstracted to be made more compact and analyzable. Refinement of a behavior specification can be performed using models of varying scopes (e.g., different subsystems) and levels of abstraction, depending on the stakeholder needs. The primary challenge then becomes ensuring that a refinement of a model is correct when that model is a composition (or abstraction) of other models; this problem has not been addressed in the existing literature. In this paper, we propose a framework that supports reasoning about behavior refinement of composite and abstract models. Our framework assures that (1) a refinement of a composition is realized with refinements of the individual
composed models and (2) a refinement of an abstract model
is interpreted in terms of a refinement of the detailed model.