Proceedings Fifth IEEE International Symposium on Requirements Engineering (2001)
Aug. 27, 2001 to Aug. 31, 2001
Margaret H. Smith , Bell Laboratories
Gerard J. Holzmann , Bell Laboratories
Kousha Etessami , Bell Laboratories
Abstract: 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, 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 standards. The TimeLine editor simplified the task of converting a large body of English prose requirements into formal, yet readable, logic requirements.
model checking, software verification, testing, requirements.
M. H. Smith, G. J. Holzmann and K. Etessami, "Events and Constraints: A Graphical Editor for Capturing Logic Requirements of Programs," Proceedings Fifth IEEE International Symposium on Requirements Engineering(RE), Toronto, Canada, 2001, pp. 0014.