Department of Computer Science
University Of Helsinki, Finland
|Topic:||Behavioral Equivalences in the Verification of Concurrent Systems|
|Date:||Thursday, November 16, 2000|
|Place:||Gould-Simpson, Room 701|
Labeled transition systems form an established formal model of concurrent systems. Many formal specification languages (e.g. CSP, CCS, and LOTOS) can be provided with semantics expressed in terms of transition systems. Behavioural equivalences between transition systems can be used widely in the verification of concurrent systems.
The lecture gives an introduction to process equivalence concepts and shows with application examples their utility in the verification of some simple class-room size examples of concurrency. Recent research results at the University of Helsinki achieved in this area are surveyed.