ACTIVE: A Tool for Integrating Analysis Contracts
Ivan Ruchkin, Dionisio de Niz, Sagar Chaki, David Garlan · 2014
Development of modern Cyber-Physical Systems (CPS) re-lies on a number of analysis tools to verify critical prop-erties. The Architecture Analysis and Design Language (AADL) standard provides a common architectural model to which multiple CPS analyses can be applied. Unfortu-nately, interaction between these analyses can invalidate their results. In this paper we present ACTIVE, a tool de-veloped within the OSATE/AADL infrastructure to en-sure correct analysis interaction. We describe the prob-lems that occur when multiple analyses are applied to an AADL model and how these problems invalidate analysis results. Interactions between analyses, implemented as OS-ATE plugins, are formally described in ACTIVE in order to enable automatic verification. In particular, these interac-tions are captured in an analysis contract consisting of in-puts, outputs, assumptions, and guarantees. The inputs and outputs help determine the correct order of execution of the plugins. Assumptions capture the conditions that must be valid in order to execute an analysis plugin, while guar-antees are conditions that are expected to be valid after-wards. ACTIVE allows the use of any generic verification tool (e.g., a model checker) to validate these conditions. To coordinate these activities our tool uses two components: ACTIVE EXECUTER and ACTIVE VERIFIER. ACTIVE EX-ECUTER invokes the analysis plugins in the required or-der and uses ACTIVE VERIFIER to check assumptions and guarantees. ACTIVE VERIFIER identifies and executes the verification tool that needs to be invoked based on the tar-get formula. Together, they ensure that plugins are always executed in the correct order and under the correct con-ditions, guaranteeing correct results. To the best of our knowledge, ACTIVE is the first extensible framework that integrates independently-developed analysis plugins ensur-ing provably-correct interactions.