Graphical specifications for concurrent software systems

Abstract

We present a description of a graphical interval logic that is the foundation of a toolset we are developing to support formal specification and verification of concurrent software systems. Experience has shown that most software engineers find standard temporal logics difficult to under- stand and to use. Our objective is to enable software engineers to specify and reason about temporal properties of concurrent systems more easily by providing them with a logic that has an intuitive graphical representation and with tools that support its use. To illustrate the use of our graphical interval logic, we provide a specification for a readers/writers database system and prove several properties of the specification.