A Model-Checking Tool with Non-Trivial Data Structures

Model-checking is one of the most successful automatic verification techniques over the last 20 years, and the development of model-checking tools is the bridge that connects theories in this field and applications. In order to efficiently model-check value-passing current systems which involve non-trivial data structures. An extended symbolic transition graph with assignment （STGA） is introduced as the semantic model of concurrent systems, and a modal graph is used as the semantic model of logic formulae. And then following an on-the-fly algorithm, a prototype tool is implemented to model-check concurrent systems. In this paper model-checking is summarized by introducing non-trivial data structures into value-passing process specification language and STGA. A practical case is also presented to justify the tool’s efficiency.