The common practice for verifying properties described as event occurrence patterns is to translate them into observer state machines. The resulting observer is then composed with (the components of) the system under analysis in order to verify a reachability property. Live Component Analysis is a "cone of influence" abstraction technique aiming at mitigating state explosion by detecting, at each observer location, which components are actually relevant for model checking purposes. Interestingly enough, the more locations the observer has, the more precise the relevance analysis becomes. This work proposes the formal underpinnings of a method to safely leverage this fact when properties are stated as event patterns (scenarios). That is, we present a sound and complete method of property manipulation based on specializing and complementing scenarios. The application of this method is illustrated on two case studies of distributed real-time system designs, showing dramatic improvements in the verification phase, even in situations where verification of the original scenario was unfeasible.

AADL is an aerospace standard for model-driven design of complex real-time embedded sys- tems. Currently, behavioral properties of AADL models can be specified inside the system description using AADL concepts or outside it using external textual languages, and verified using schedulability analysis or (Time Petri Net-based) model-checking tools. This paper (1) proposes Visual Timed Scenarios (V TS) as a graphical property specification language for AADL, and (2) devises an effective translation from V TS to Time Petri Nets (TPN) which enables model-checking properties expressed in V TS over AADL models using TPN-based tools integrated into AADL-compliant IDEs (e.g., TOPCASED).

AADL is an aerospace standard for model-driven design of complex real-time embedded systems. Currently, behavioral properties of AADL models can be specified inside the system description using AADL concepts or outside it using external textual languages, and verified using schedulability analysis or (Time Petri Net-based) model-checking tools. This paper (1) proposes Visual Timed Scenarios (V TS) as a graphical property specification language for AADL, and (2) devises an effective translation from V TS to Time Petri Nets (TPN) which enables model-checking properties expressed in V TS over AADL models using TPN-based tools integrated into AADL-compliant IDEs (e.g., TOPCASED).