Specification and Testing of Temporal Properties of ConcurrentSystem Designs

This paper investigates the use of Graphical Interval Logic for specificationand testing of concurrent and real-time systems. Past research produced atoolset for creating specifications in GIL and for reasoning about propertiesof systems that satisfy their specifications. Current research is exploringthe use of GIL specifications during system design and implementation.Our work to date has focused primarily on using GIL specifications as oraclesduring testing of executable designs. The paper presents an example in whichGIL specifications for an Ada design are used to uncover faults duringtesting. It also shows how the graphical representation of formulas can beused to advantage in displaying a trace that violates a specification. Thetesting methods have yet to be automated.