ACTIVE: A Tool for Integrating Analysis Contracts
Abstract
In this paper we present ACTIVE, a tool and framework to semantically integrate independently-developed analysis plugins in OSATE, a tool for modeling systems in the Architecture Analysis and Design Language (AADL). In the paper we analyze the problems that occur when independently-developed analysis plugins are executed on an AADL model and how these problems can lead to invalid analysis results. We show how our framework model plugin interactions in a formal way in order to enable automatic verification. These interactions are captured in an analysis contract that describes inputs, outputs, assumptions, and guarantees. The input and outputs in the contract allow us to determine the correct order in which plugins must execute. The assumptions and guarantees, on the other hand, capture the conditions that must be valid to execute a plugin and the one that are expected to be valid afterwards. The ACTIVE framework allows the inclusion of any generic verification tool (e.g. model checkers) to verify these conditions. To coordinate all these activities uses two components: the ACTIVE EXECUTER and the ACTIVE VERIFIER. The ACTIVE EXECUTER executes the plugins in the required order calling the ACTIVE VERIFIER every time assumption and guarantees need to be verified. The ACTIVE VERIFIER, in turn identifies and executes the verification tool that needs to be invoked based on the target formula. Together, they ensure that the plugins are always executed in the correct order and under the correct conditions guaranteeing a sound verification process. To the best of our knowledge ACTIVE is the first extensible framework able to integrate independently-developed analysis plugins guaranteeing their correct interaction and execution.
Document Details
- Document Type
- Technical Report
- Publication Date
- Oct 14, 2014
- Accession Number
- ADA610323
Entities
People
- David Garlan
- Dionisio de Niz
- Ivan Ruchkin
- Sagar Chaki
Organizations
- Carnegie Mellon University