Title :
Adapting Models to Model Checkers, A Case Study : Analysing AADL Using Time or Colored Petri Nets
Author :
Renault, Xavier ; Kordon, Fabrice ; Hugues, Jérôme
Author_Institution :
Lab. d´´Inf. de Paris 6/MoVe, Univ. Pierre & Marie Curie, Paris, France
Abstract :
The verification of High-Integrity Real-Time systems combines heterogeneous concerns: preserving timing constraints, ensuring behavioral invariants, or specific execution patterns. Furthermore, each concern requires specific verification techniques; and combining all these techniques require automation to preserve semantics and consistency. Model-based approaches focus on the definition of representation of a system, and its transformation to equivalent representation for further processing, including verification and are thus good candidates to support such automation. In this paper, we show there is a strong requirement to automatically map high-level models to abstractions that are dedicated to specific analysis techniques taking full advantage of tools. We discuss this requirement on a case study: validating some aspects of AADL models using both coloured and time Petri Nets.
Keywords :
Petri nets; distributed processing; formal specification; formal verification; hardware description languages; real-time systems; AADL; behavioral invariants; colored Petri nets; execution patterns; high-integrity real-time systems; model checkers; specific verification techniques; time Petri nets; timing constraints; Automation; Dispatching; Formal specifications; Hardware; Model driven engineering; Petri nets; Prototypes; Real time systems; Telecommunications; Yarn;
Conference_Titel :
Rapid System Prototyping, 2009. RSP '09. IEEE/IFIP International Symposium on
Conference_Location :
Paris
Print_ISBN :
978-0-7695-3690-3
DOI :
10.1109/RSP.2009.30