System verification for AADL-based systems

Abstract

The AADL HAMR Semantics Mechanization (AADL-HSM) is an Isabelle-based mechanization of the informal Architecture Analysis and Design Language (AADL) semantics that formalizes the structure and execution of AADL for the High-Assurance Model-based Rapid engineering for embedded systems (HAMR) toolkit. In addition, the AADL-HSM introduces the formalization of a property framework to support component-oriented contract specification and verification. However, the existing framework does not support system-level specification and verification. This report presents a sound system-level contract framework for an extension of the simplified variant of the AADL-HSM. The approach requires a workflow net representation of the scheduling constraints for a system to be constructed, which is then used to express assertions that should hold between the execution of two explicitly constrained disjoint sets of components in a constraint-compliant static schedule. From these assertions, along with the component-level contracts, verification conditions and independence requirements are systematically generated and then discharged via automatic methods such as SMT solvers. This approach provides a sound theoretical basis for the implementation of the framework into the full HAMR toolkit.