A Mechanized Semantics for Component-Based Systems in the HAMR AADL Runtime

Many visions for model-driven component-based development emphasize models as the “single source of truth” by which different forms of analysis, specification, verification, and code generation are integrated. Such a vision depends strongly on a clear modeling language semantics that provides different tools and stakeholders with a common understanding of a model’s meaning. In this paper, we report on a mechanization of a formal semantics in the Isabelle theorem prover for key aspects of the SAE standard AADL modeling language. A primary goal of this semantics is to support component-oriented contract specification and verification as well as code generation implemented in the HAMR AADL model-driven development tool chain. We provide formal definitions of run-time system state, execution steps, reachable states, and property verification. Use of the mechanization for real-world applications is supported by automated HAMR translation from AADL models into the Isabelle specifications. In addition to general verification support, we define well-formedness properties and associated proofs for models, system states, and traces that are automatically proven for HAMR-generated Isabelle models.