D. Monteverde, A. Olivero, S. Yovine, V. Braberman
VTS-based Specification and Verification of Behavioral Properties of AADL Models (2008)
VTS-based Specification and Verification of Behavioral Properties of AADL Models (2008)
TR-2008-11.pdf
Keywords: Embedded systems, component-based modeling, behavioral properties, visual specification, verification, scenarios, Time Petri Nets, VTS, AADL
Abstract: 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 ($vts$) as a graphical property specification language for AADL, and (2) devises an effective translation from $vts$ to Time Petri Nets (TPN) which enables model-checking properties expressed in $vts$ over AADL models using TPN-based tools integrated into AADL-compliant IDEs (e.g., TOPCASED).
