Automatic verification of properties in transition systems

摘要

AbstractThe aim of this paper is to show the use of MEC, an automated tool for analysing transition systems, for discovering deadlocks, livelocks and other properties of a given transition system. The features of MEC are shown with two instructive examples: first, the analysis of an electronic mail system, first analysed by G. Brebner using the concurrency work bench (another automated analysis tool); second, the analysis of a simple call‐processing system originating from Bell‐Northern‐Res