A graphic environment for temporal reasoning
G. Kutty · 1995
Temporal logic is widely recognized as an appropriate formalism for the study of reactive systems. However, traditional temporal logics can be tedious and unintuitive for designers of reactive systems to use. This dissertation develops techniques and tools that attempt to render the use of temporal specification and verification more accessible to system designers. This disaertation describes the use of Graphical Interval Logic, a visual language for temporal reasoning, as the basis of a working environment for tempora specification and verification. Graphical Internal Logic provides an intuitive graphical notation for representing the relative ordering of events in a concurrent system and the manner in which predicates that represent system properties change with time. It is, nevertheless, a formally defined language that retains the rigor of purely textual methods. A prototype graphical toolkit that supports tbe use of Graphical Interval Logic has been implemented. It enables one to construct and edit Graphical Interval Logic formulas using a graphical syntax-directed editor that provides high-level editing operations which are meaningful in terms of the constructs of the language and ensures that the formulas constructed using the editor are syntactically correct. The toolkit supports a verification methodology in which specifications, proofs and counterexamples are represented graphically. The dissertation also presents a deductive system for Graphical Interval Logic that formalizes the technique and a first-order extension that extends its scope. The relationship between Graphical Interval Logic and traditional temporal logics is shown by providing appropriate translation procedures between the logics. A detailed example is provided that illustrates the application of the methodology by developing a specification of the sliding window protocol using successive refinements and by establishing its correctness using the toolkit and the proof rules for the logic.