Analyzing multi-view models of software systems

(eng) The model-driven elaboration, validation, and documentation of system requirements and designs calls for rich system models. To be comprehensive, such models need to cover the intentional, structural, operational and behavioral dimensions of the target system. Building adequate, complete, and consistent models is not an easy task. Techniques should therefore be available for detecting and fixing modeling errors early and in a systematic way. The thesis provides an integrated set of tool-supported techniques for analyzing system models along the behavioral, operational and intentional dimensions. Our analysis techniques mainly focus on decision-based process models. The latter capture processes where the application of specific tasks and their sequencing depends on explicit decisions that are based on the state of the environment in which the process operates. Decision-based processes in areas such as healthcare are often critical in terms of timing and resources. The language of High-Level Message Sequence Charts is extended with guards, timing and resource constructs to model such processes. This language allows us to naturally integrate stakeholder material including multi-agent scenarios, decision trees and flowchart fragments. The proposed analysis techniques allow us to highlight a variety of modeling problems early and incrementally on partial models, including: inadequate decisions resulting from inaccurate or outdated information about the environment; incompleteness of decisions; unreachability of specific tasks along certain process paths; undesirable non-determinism in process decisions; and violations of temporal constraints. These techniques are demonstrated on the incremental building and analysis of a complex model of a real protocol for cancer therapy. Other techniques are proposed for analyzing interaction scenarios, specified as Message Sequence Charts, and state machines, specified as Labeled Transition Systems. The latter techniques allow us to infer a significant class of goals and domain properties from scenarios and to generate state invariants on each node of a state machine behavior model. Many of the analysis techniques proposed are based on different instantiations of a generic algorithm that propagates decorations through a model graph until a fixpoint is reached.