© University of Kent - Contact | Feedback | Legal | FOI | Cookies
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},
}