VTS-based Specification and Verification of Behavioral Properties of AADL Models

MONTEVERDE, DANIEL; AFREDO OLIVERO; SERGIO YOVINE; VICTOR BRABERMAN

Toulouse, Francia

Workshop; Model Based Architecting and Construction of Embedded Systems; 2008

ArtistDesign European Network of Excellence on Embedded Systems Design

AADL is an aerospace standard for model-driven design of complex real-time embedded systems. Currently, behavioral properties of AADL models can be speci¯ed inside the system description using AADL concepts or outside it using external textual languages, and veri¯ed using schedulability analysis or (Time Petri Net-based) model-checking tools. This paper (1) proposes Visual Timed Scenarios (V TS) as a graphical property speci¯cation language for AADL, and (2) devises an e®ective 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).