| Abstract: | ![]()
The 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-Research. |
