An ocarina extension for AADL formal semantics generation.

The formal verification has become a recommended practice in safety-critical software engineering. The hand-written of the formal specification requires a formal expertise and may become complex, especially with large systems. In such context, the automatic generation of the formal specification seems helpful and rewarding, 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 specification to draw a gateway for the CADP formal analysis toolbox.