An Extended Symbolic Model For Concurrent Value-passing Processes

Model checking is one of the most successful automatic verification techniques in the past thirty years. To model check a value-passing concurrent system, an abstract model must be constructed, and Symbolic Transition Graphs with Assignment is such an abstract model.The choice of abstract models for value-passing concurrent systems directly influences the efficiency of model checking. Since processes with infinite data domains can have finite symbolic transition graphs, STGAs are a popular model for this purpose. However, using the standard symbolic operational semantics, a parameterized process definition may generate several copies of sub-graphs, one for each instantiation of actual data parameters. To overcome this drawback, a new variation of STGA, called STGA~2, is proposed in this thesis. The basic idea is to introduce assignment both before and after each input/output action in STGA. With such an extension, every parameterized process definition gives rise to exactly one copy in a STGA~2. In this way, the size of symbolic graph is reduced.The main contents of this thesis are: Define the Symbolic Transition Graph with bi-assignment, STGA~2 and its operating semantics; Prove the semantic equivalence between STGA~2 and STGA; Propose a set of transformation rules for STGA~2 and prove that they are semantic-preserving; Implement the operational semantics and transformation rules of STGA~2. Compare the efficiencies of STGA~2 and STGA by case studies.