Towards a formal specification for an AADL behavioural subset using the LNT language
| Autor: | Bechir Zalila, Jérôme Hugues, Hana Mkaouar, Mohamed Jmaiel |
|---|---|
| Rok vydání: | 2020 |
| Předmět: |
010302 applied physics
060102 archaeology Computer science Programming language Strategy and Management Architecture Analysis & Design Language Formal semantics (linguistics) 06 humanities and the arts computer.software_genre Formal methods 01 natural sciences Rotation formalisms in three dimensions Management Information Systems Formal specification 0103 physical sciences Robot 0601 history and archaeology Business and International Management computer Formal verification |
| Zdroj: | International Journal of Business and Systems Research. 14:162 |
| ISSN: | 1751-2018 1751-200X |
| DOI: | 10.1504/ijbsr.2020.10027613 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|