Implementing A Graphical User Interface For An Automated Proof Tool For Message-Passing Concurrent System

As computer hardware and software systems become more and more complex, the problem of how to assure the correctness and reliability of such systems has attracted much attention from both industry and research communities. Among the solutions to the analysis and verification of such systems, model checking is one of the most successful automatic verification techniques in the past two decades. Because of its high level automation and high efficiency, model checking has been widely used in the analysis and verification of finite-state systems.Concurrent processes cooperate with each other by exchanging message. The existing model checking tools based on process algebras cannot directly handle data passing between processes. This thesis describes the implementation of a graphical user interface for an automated proof tool for message-passing concurrent system. The main work includes: Programming a graphical user interface for the tool using Motif toolkit. Presenting a solution to implementing the communication between functional programming language SML and C language, and designing a protocol between the two parts to cooperate with each other to accomplish verification commands. Discussing how to graphically display counter-example and presenting one solution. Extending the functionality of the tool by implementing a simulator.