DOC PREVIEW
USC CSCI 510 - usc-csse-2010-510

This preview shows page 1-2-3 out of 10 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 10 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 10 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 10 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 10 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

1 Introduction2 Background and Motivation2.1 Modal Transition Systems2.2 Motivating Examples2.3 Related Work3 Atomic Refinement Operations4 Refinement Under Composition4.1 Transition Refinement4.2 State Refinement5 Refinement Under Abstraction5.1 Transition Refinement5.2 State Refinement6 Case Studies7 Conclusions8 ReferencesSupporting Refinement of Partial Behavior ModelsUnder Model Composition and AbstractionIvo Krka and Nenad MedvidovicComputer Science DepartmentUniversity of Southern CaliforniaLos Angeles, CA 90089-0781, USA{krka,neno}@usc.eduABSTRACTDuring requirements elicitation and preliminary design, a system’sbehavior is typically partially specified: some behavior is definedas either forbidden or required, while other behavior is not yet cat-egorized as either of those. The goal is then to gradually refine thespecification and finally arrive at a complete behavioral description.Partial-behavior modeling formalisms, such as Modal TransitionSystems, can support such gradual refinement. However, severalchallenges still remain, particularly in the context of hierarchical ar-chitectural specifications where (sub)system models are composedof smaller subsystems and components, and, in turn, abstracted tobe made more compact and analyzable. Refinement of a behav-ior specification can be performed using models of varying scopes(e.g., different subsystems) and levels of abstraction, depending onthe stakeholder needs. The primary challenge then becomes ensur-ing that a refinement of a model is correct when that model is acomposition (or abstraction) of other models; this problem has notbeen addressed in the existing literature. In this paper, we proposea framework that supports reasoning about behavior refinement ofcomposite and abstract models. Our framework assures that (1) arefinement of a composition is realized with refinements of the indi-vidual composed models and (2) a refinement of an abstract modelis interpreted in terms of a refinement of the detailed model.1. INTRODUCTIONModeling software systems can provide rich benefits; this is par-ticularly the case for modern software that is increasingly large andcomplex [18]. During iterative requirements elicitation and pre-liminary design, one of the main goals of behavioral modeling andanalysis is to support incremental discovery, specification, and re-finement of the desired system behavior. The system specificationsused in these initial stages of a system’s life cycle, such as scenariosand safety properties, are intuitive and focus on narrow aspects of asystem’s behavior. For example, a scenario describes a single exe-cution sequence that should be exhibited by the system-to-be, whilea safety property prescribes some behavior as illegal. Notably, suchearly specifications do not exhaustively define a system’s behavior,but require or forbid particular instances. Informally, the goal ofthe subsequent requirements elicitation (or design) iterations is todetermine whether the behavior that is currently neither requirednor forbidden (i.e., the maybe behavior), should become requiredor forbidden. The specification refinement is complete when all thebehavior is categorized as either required or forbidden.The different aspects of early system specifications can be cap-tured using partial behavior modeling techniques, such as ModalTransition Systems (MTS) [13], which distinguish between required,maybe, and forbidden system state transitions. Hence, the speci-fied scenarios can be represented using required transitions, whilethe maybe transitions should not conflict with the safety properties.The specification refinement in this setting corresponds to modify-ing some of the maybe behavior to required or removing it. Sev-eral existing approaches leverage early requirements specificationsto synthesize partial behavior models [10, 11, 21]. Additionally,MTSs pertaining to the same component (or subsystem) can bemerged together [8, 19]. Even in the context of component reuse,partial behavior models are capable of capturing the behavior of in-dividual components [12], as well as product line components [6,7, 12]. The maybe transitions in the models of reused componentscorrespond to the variability in how a component can be used, orthe variability in a product line component’s behavior.Although partial behavior models provide a basis for early be-havioral analysis and incremental specification refinement, thereare significant practical challenges to their application on largerspecifications. In this paper, we address some of the foundationalchallenges that arise when applying partial behavior models in thecontext of hierarchical software architecture specifications. Infor-mally, software components are composed into subsystems1, whichare in turn composed into higher-level subsystems and, eventually,a system [2, 17, 20]. Assuming the availability of component- orsubsystem-level models, which can be synthesized using existingtechniques [10] or are readily available [12], a behavioral model ofa subsystem can be obtained by applying parallel composition tounderlying component models. To scale modeling and analysis, thesubsystem- or system-level models are in turn abstracted by hidingirrelevant actions and minimizing the resulting model [2].In iterative development, a behavioral specification can be re-fined at varying levels of scope and abstraction. For example, anon-expert stakeholder is concerned with behavior described in acoarse-grain model of a subsystem of interest, while an engineermay work with models of fine-grain components. While the exist-ing literature teaches us how to compose, abstract, and refine inde-pendent partial behavior models, the remaining challenges pertainto correctly refining a model of a wider scope (a composition) or ahigher level of abstraction. These challenges stem from the innatedependencies between (1) a composite model and the composedmodels, and (2) an abstract model and the detailed model.2Withoutconsidering such dependencies, the refinement process can resultin inconsistencies that render some models or refinement steps use-less thus wasting modeling effort. Therefore, a critical prerequisitefor behavior refinement in the context of hierarchical architecturalspecifications is to be able to reason about and propagate the impli-cations of model refinements; otherwise, the applicability of partialbehavior models in software development remains limited.In this paper, we propose a semi-automated


View Full Document

USC CSCI 510 - usc-csse-2010-510

Download usc-csse-2010-510
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view usc-csse-2010-510 and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view usc-csse-2010-510 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?