Partial Behavioural Models for Requirements and Early Design

In this paper, we first motivate and summarize our recent work on creation, management, and specifically merging of partial be- havioural models, expressed as model transition systems. We then ad- dress two issues coming out of MMOSS discussions: alphabet embedding as an alternative to common observational refinement and minimum re- finement steps. We show that the former is not possible, and discuss informally how to define the latter. 1 Introduction and Goals of the Project Event-based models such as Labeled Transition Systems (LTSs) (9) have been shown to be successful for modeling and reasoning about the behavior of software systems at the architectural level. These behavior models provide a basis for a wide range of successful automated analysis techniques, such as model-checking, animation, and simulation. However, the adoption of behavior modeling and analysis technology by practitioners has been slow. Partly, this is due to the complexity of building behavioral models in the first place - behavior modeling remains a difficult, labor-intensive task that requires considerable expertise. In addition, and per- haps more importantly, the benefits of the analysis appear only at the end of a costly process of constructing a comprehensive behavior model. The reason for the latter is that traditional behavior models are required to be complete descriptions of the system behavior up to some level of abstraction, i.e., the transition system is assumed to completely describe the system behavior with respect to a fixed alphabet of actions. This completeness assumption is limit- ing in the context of software development process best practices which include iterative development, adoption of use-case and scenario-based techniques and viewpoint- or stakeholder-based analysis; practices which require modeling and analysis in the presence of partial information about system behavior. Our aim is to address the limitations of existing behavior modeling ap- proaches by shifting the focus from traditional behavior models to partial be- havior models - models that are capable of distinguishing known behavior (both