Temporal Logic Case Study
August 1989 • Technical Report
William G. Wood
This report is a case study applying temporal logic to specify the operation of a bank of identical elevators servicing a number of floors in a building.
Publisher:
Software Engineering Institute
CMU/SEI Report Number
CMU/SEI-89-TR-024
Abstract
This report is a case study applying temporal logic to specify the operation of a bank of identical elevators servicing a number of floors in a building. The goal of the study was to understand the application of temporal logic in a problem domain that is appropriate for the method, and to determine some of the strengths and weaknesses of temporal logic in this domain. The case study uses a finite state machine language to build a model of the system specification, and verifies that the temporal logic specifications are consistent using this model. The specification aspires to be complete, consistent, and unambiguous.