Constructing Multi-Formalism State-Space Analysis Tools: Using Rules to Specify Dynamic Semantics of Models

Abstract

State-space analysis techniques have been developed for several representations of concurrent systems, but each tool or technique has typically been targeted to a single design or program notation.We describe an approach to constructing multi-formalism state-space analysis tools for heterogeneous system descriptions, using a shared "inframodel" that represents only the essential information for interpretation by tool components that can be customized to reflect the semantics of each formalism.The (operational) semantics of each formalism, as well as interactions between components described in different formalisms, is described separately through rules governing enabling, matching, and firing of transitions.This results in more natural and compact internal representations, and more efficient analysis, than a purely translational approach.In a previous paper, execution semantics of the inframodel was controlled through a limited set of parameters.The rulebased approach described in this paper accomodates a wider range of state-transition formalisms.