An ocarina extension for AADL formal semantics generation
| Autor: | Hana Mkaouar, Mohamed Jmaiel, Jérôme Hugues, Bechir Zalila |
|---|---|
| Přispěvatelé: | Institut Supérieur de l'Aéronautique et de l'Espace - ISAE-SUPAERO (FRANCE), Digital Research Center of Sfax (TUNISIA), Université de Sfax (TUNISIA), Département d'Ingénierie des Systèmes Complexes - DISC (Toulouse, France), Université de Sfax - University of Sfax, Département d'Ingénierie des Systèmes Complexes (DISC), Institut Supérieur de l'Aéronautique et de l'Espace (ISAE-SUPAERO), Centre de Recherche en Numérique de Sfax (CRNS) |
| Jazyk: | angličtina |
| Rok vydání: | 2018 |
| Předmět: |
AADL
Computer science business.industry Model transformation Formal semantics (linguistics) 020207 software engineering 02 engineering and technology Systèmes embarqués LNT Formal semantics Formal specification Semantics of logic 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing [INFO.INFO-ES]Computer Science [cs]/Embedded Systems Software engineering business computer Formal verification computer.programming_language |
| Zdroj: | Proceedings of the 33rd Annual ACM Symposium on Applied Computing (SAC'18) ACM Symposium on Applied Computing (SAC'18) ACM Symposium on Applied Computing (SAC'18), Apr 2018, Pau, France. pp.1402-1409, ⟨10.1145/3167132.3167282⟩ SAC |
| DOI: | 10.1145/3167132.3167282⟩ |
| Popis: | International audience; The formal veri cation has become a recommended practice in safety-critical software engineering. The hand-written of the for- mal speci cation requires a formal expertise and may become com- plex especially with large systems. In such context, the automatic generation of the formal speci cation seems helpful and reward- ing, particularly for reused and generic mapping such as hardware representations and real-time features. In this paper, we aim to formally verify real-time systems designed by AADL language. We propose an extension AADL2LNT of the Ocarina tool suite allowing the automatic generation of an LNT speci cation to draw a gateway for the CADP formal analysis toolbox. This work is illustrated with the Pacemaker case study. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|