search menu icon-carat-right cmu-wordmark

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.