School of Computing

Verification of concurrent systems

Li Su

Technical Report 10-03, University of Kent, Computing Laboratory, University of Kent, Canterbury, Kent, UK, October 2003 Master thesis.

Abstract

In recent years, people are interested in real time and distributed systems. A vital characteristic of such systems is that they are usually concurrent. There are various techniques that support formal modeling of concurrency. One is Process Algebra; other techniques include Temporal Logic and Timed Automata. Moreover, one of the most successful verification techniques is called model checking, which is a technique for verifying finite state concurrent systems and tracing errors. We investigate the deadlock detection, especially timelock detection in UPPAAL. We also give a formal definition of Timed Automata and its semantics, following a classification of deadlocks, and two Progress Requirements. We then provide an algorithm and implement the algorithm to detect zeno-timelock. At the end the software is tested for its input and cycle detector and we give a case study of CSMA/CD. It is specified in UPPAAL, and then we use the software to verify it.

Download publication 844 kbytes (PostScript)

Bibtex Record

@techreport{2256,
author = {Li Su},
title = {Verification of Concurrent Systems},
month = {October},
year = {2003},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {Master thesis},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/2003/2256},
    publication_type = {techreport},
    submission_id = {14930_1128520382},
    type = {Technical Report },
    number = {10-03},
    address = {University of Kent, Canterbury, Kent, UK},
    institution = {University of Kent, Computing Laboratory},
}

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014