9402807 Cleaveland The goals of this project involve the development of practical approaches to the automatic verification of finite-state concurrent systems, including hardware designs, communications protocols, and software requirements specifications. Such systems are notoriously difficult to design, debug and maintain, owing to the subtle and often unanticipated interactions between components that parallelism induces. One appealing approach to overcoming these problems involves the use of mathematical reasoning to ensure that systems behave as intended; this research aims at making the use of such formal analysis practical by developing suitable techniques, and associated software tools, that enable designers to analyze their systems as they are building them. The proposed work would develop along the following lines: Research would undertaken into more efficient algorithms for determining the correctness of concurrent systems; techniques would investigated for enabling the analysis of larger systems than can currently be managed; he development of usable graphical and textual design languages would undertaken, and appropriate tools implemented; methods would develop and implement for reasoning about real-time systems and about the relative reliability of systems. ***
