FU Berlin, Fachbereich Mathematik und Informatik, Institut für Informatik

Vortrag des Informatik-Kolloquiums

The talk describes a toolset for specification and verification of concurrent systems based on Graphical Interval Logic. Specifications in the logic have an intuitive visual representation that resembles the timing diagrams drawn by hardware and software engineers. The toolset includes a visual editor for drawing graphical formula on a workstation display, an automated proof checker for certifying the validity of proofs, and a simple proof management and database system. All user interaction is through the visual interface provided by the editor. An example is presented to illustrate the use of the tools in reasoning about behaviors of a system.