Date of Award

2001

Publication Type

Master Thesis

Degree Name

M.Sc.

Department

Computer Science

Keywords

Computer Science.

Supervisor

Chen, X.

Rights

info:eu-repo/semantics/openAccess

Abstract

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.

Download

Share

COinS