Integrated Contract-Based Unit and System Testing for Component-Based Systems

This paper presents a system testing framework for development of AADL-based systems using the HAMR model-driven development framework. A key theme of the framework is the integration of unit testing and program verification based on formal contracts that are synchronized between models and code. HAMR’s scheduling framework is extended to enable test scripting aligned with AADL’s standardized run-time services (RTS) and real-time task structures. Libraries of state observers and injectors aligned with the AADL RTS are auto-generated, enabling system property tests to observe system state and force the state to contain certain values. Executable versions of component contracts are automatically checked during system tests. A randomized property-based testing approach is used to generate vectors of input values for subsystem ports, helping to achieve coverage with reduced developer effort. A server-based architecture automatically distributes system tests in a continuous integration environment and accumulates and correlates coverage information. Together with HAMR’s ability to generate system deployments on the verified seL4 micro-kernel, these capabilities provide another step towards the community’s long-term objectives of practical model-based development that integrates formal models, specifications, and rigorously-assured application and infrastructure code at many different levels of abstraction.