Towards a formal specification for an AADL behavioural subset using the LNT language

Hana Mkaouar, Bechir Zalila, Jérôme Hugues and Mohamed Jmaiel

International Journal of Business and Systems Research, 2020, vol. 14, issue 2, 162-190

Abstract: The analysis of real-time systems designed by architectural languages such as architecture analysis and design language (AADL) is a challenging research topic. In such a context, formal methods become an advocated practice in software engineering for rigorous analysis. Yet, they are applied on specific formalisms to be analysed on dedicated tools. This paper studies the formal verification of real-time systems modelled with the AADL language and its behaviour annex. We define a formal semantics of an AADL behavioural subset using the LNT language. This work is illustrated with a robot case study.

Keywords: real-time systems; formal verification; architecture analysis and design language; AADL; behaviour annex. (search for similar items in EconPapers)
Date: 2020
References: Add references at CitEc
Citations:

Downloads: (external link)
http://www.inderscience.com/link.php?id=106278 (text/html)
Access to full text is restricted to subscribers.

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:ids:ijbsre:v:14:y:2020:i:2:p:162-190

Access Statistics for this article

More articles in International Journal of Business and Systems Research from Inderscience Enterprises Ltd
Bibliographic data for series maintained by Sarah Parker ().