Symbolic Test Generation Using a Temporal Logic with Constrained Events

摘要

A temporal logic with constrained event modallities, TLCE, is proposed to represent test purposes for testing concurrent programs. The logic is capable can express not only temporal relationships among input and output events, but also data dependencies between event parameters. A TLCE-based test generation algorithm is developed to automatically derive symbolic test cases that incorporate given data dependency constraints as verdict conditions. The advantage of the approach is demonstrated with a case study on a cache coherence protocol.