Su, Li (2003) Verification of Concurrent Systems. Technical report. University of Kent, University of Kent, Canterbury, Kent, UK
| The full text of this publication is not available from this repository. (Contact us about this Publication) | |
| Official URL http://www.cs.kent.ac.uk/pubs/2003/2256 |
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.
| Item Type: | Monograph (Technical report) |
|---|---|
| Additional information: | Master thesis |
| Subjects: | Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming, |
| Divisions: | Faculties > Science Technology and Medical Studies > School of Computing > Theoretical Computing Group |
| Depositing User: | Mark Wheadon |
| Date Deposited: | 24 Nov 2008 18:00 |
| Last Modified: | 15 Mar 2009 13:52 |
| Resource URI: | http://kar.kent.ac.uk/id/eprint/13893 (The current URI for this page, for reference purposes) |
- Depositors only (login required):
