Using Diagrams to give a Formal Specification of Timing Constraints in Z

The need to represent timing requirements for computer systems in a formal way is being addressed by a growing number of specification techniques. However, a common weakness in these techniques is understandability, as a specification is often used to communicate between interested parties who may not possess the skills necessary to interpret a formal specification. Some atemporal specification languages deal with this problem by means of graphical notations with associated formal semantics (e.g. statecharts), although to the knowledge of the author, no such technique exists for dealing with temporal constraints in such a way. This paper presents causal timing diagrams, one possible approach for describing timing requirements graphically with an underlying formal semantics. 1. Introduction Where computer systems are to be used within high-integrity or safety-critical applications, it is essential that the risk of any kind of failure is minimised. The use of formal methods as a means..