Virtual Integration for Pattern-Based Contracts with the KIND2 Model Checker

摘要

In component based design of embedded software, virtual integration verifies hierarchical decomposition of components and contracts. In this paper we present a virtual integration analysis that is based on the Kind2 state-of-the-art model checker. Our method focuses on pattern-based requirements with automata-based semantics. We propose the Simplified Universal Pattern that is used in the BTC EmbeddedPlatform as a specification language, but other languages may be used as well. The main contribution is a reduction of virtual integration to a reachability problem on so-called counter automata that form the semantics of the pattern language. The counter automata are translated to the synchronous data flow language LUSTRE, that serves as input for KIND2. KIND2 turns out to be quite powerful in proving the safety properties that result from the reachability problem for the automata. Thus, it yields a positive sound (but not complete) verification technique that gives a sufficient condition for virtual integration.