Events and Constraints: A Graphical Editor for Capturing Logic Requirements of Programs

Margaret H. Smith, Gerard J. Holzmann, Kousha Etessami

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

A logic model checker can be an effective tool for debugging software applications. A stumbling block can be that model-checking tools expect the user to supply a formal statement of the correctness requirements to be checked in temporal logic. Expressing non-trivial requirements in logic, however, can be challenging. To address this problem, we developed a graphical tool, called the TimeLine Editor, that simplifies the formalization of certain kinds of requirements. A series of events and required system responses are placed on a timeline. The user converts the timeline specification automatically into a test automaton that can be used directly by a logic model checker or for traditional test-sequence generation. We have used the TimeLine Editor to verify the call processing code for Lucent's PathStar access server against the TelCordia LSSGR [LATA (local access and transport area) Switching Systems Generic Requirements] standards. The TimeLine Editor simplified the task of converting a large body of English prose requirements into formal, yet readable, logic requirements
Original languageEnglish
Title of host publication5th IEEE International Symposium on Requirements Engineering (RE 2001), 27-31 August 2001, Toronto, Canada
Number of pages9
Publication statusPublished - 2001


Dive into the research topics of 'Events and Constraints: A Graphical Editor for Capturing Logic Requirements of Programs'. Together they form a unique fingerprint.

Cite this