Formal verification in network of synchronizing FSMs with SPIN.
Fang Li · Library and Archives Canada (Government of Canada) · 2001
Concurrent systems are becoming more and more popular. Improving the qualities of these systems is an important issue we are facing. It is well known that developing concurrent software is a challenging task, mainly because of the non-determinism behavior involved in the system. One promising way to help the designer in this task is providing formal verification methods that can detect concurrency-related errors at the design stage. In this thesis, we present our study on model checking concurrency-related correctness of design artifacts for concurrent and distributed systems. We construct our model for design artifacts using a network of synchronizing finite state machines (NSFSM), which provides well known synchronization mechanisms from programming languages. The formal verification is performed by SPIN, which is based on visiting all the global system states reachable from a given initial state to check if some properties hold. The input language of SPIN is PROMELA, which features a C-like syntax, dynamic creation of processes, and various interprocess communication models. In order to apply SPIN, we provide an automatic translation from NSFSMs to PROMELA programs. Paper copy at Leddy Library: Theses & Major Papers - Basement, West Bldg. / Call Number: Thesis2001 .L5. Source: Masters Abstracts International, Volume: 40-03, page: 0724. Adviser: Xiaojun Chen. Thesis (M.Sc.)--University of Windsor (Canada), 2001.