AADL—architecture analysis and design language—has proven to be important in developing real-time embedded systems. However, its formalization capability is still limited, which makes it difficult to produce a consistent model; particularly, in the case where several models are combined together. Therefore, using formal verification is an effective way to meet the consistency requirements of the AADL model. This paper proposes a model-based engineering approach that uses timed automata (TA) formalism to aggregate multiple AADL models into a single composite model. Based on the set of input AADL models, the proposed approach creates a consistent composed model as well as support model checking verification. The effectiveness of this contribution is evaluated through two case studies; a multicamera surveillance system and a drone system.
|Publication status||Accepted/In press - 2023|
- systems engineering
- timed automata
ASJC Scopus subject areas
- Hardware and Architecture
- Computer Networks and Communications