Verification of Concurrent Systems

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.