A Graphical Interval Logic for Specifying Concurrent Systems

The paper describes a graphical interval logic that is the foundation of atoolset supporting formal specification and verification of concurrent softwaresystems. Experience has shown that most software engineers find standardtemporal logics difficult to understand and to use. The objective of this workis to enable software engineers to specify and reason about temporal propertiesof concurrent systems more easily by providing them with a logic that has anintuitive graphical representation and with tools that support its use. Toillustrate the use of the graphical logic, the paper provides somespecifications for an elevator system and proves several properties of thespecifications. The paper also describes the toolset and the implementation.Categories and Subject Descriptors:D.2.1 [Software Engineering] Requirements/Specifications;D.2.2 [Software Engineering] Tools and Techniques - Computer-aided softwareengineering (CASE);F.3.1 [Logics and meanings of programs] Specifying and verifying and reasoningabout programs---Specification techniques