Proving Properties of Real-Time Distributed Systems: A Comparison of Three Approaches

Three formal methods for specifying properties of real-time systems are reviewed and used in a common example. Two of them offer a graphical representation and the third is an algebraic language. The example is that of an automatic railroad system with sensors to detect the train position and controls for the gate mechanism. Associated with each formalism is a proof methodology which is described and used to prove a safety property about the example. A comparison is made between the three formalisms according to various criteria including the expressiveness, readability, maintainability of the language, support for real-time concepts, method for expressing properties and proof mechanisms.