Mechanizing AADL in Coq - Extended Abstract
Jérôme Hugues · ACM SIGAda Ada Letters · 2024
In this extended abstract, we present a mechanization of the SAE AADL language using Coq along with specific analysis capabilities. Our contribution provides an unambiguous semantics for a large set of the language and can be used as a foundation to build rich analysis capabilities. Our contribution differs from typical language mechanization, it provides support for manipulating modeling constructs, perform verification - ranging from syntactic and semantics checks to formal verification of key properties, and support simulation capabilities.