Temporal Logic Case Study Export

@techreport{citeulike:553397, 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.}, author = {Wood, William G.}, citeulike-article-id = {553397}, citeulike-linkout-0 = {http://www.sei.cmu.edu/publications/documents/89.reports/89.tr.024.html}, keywords = {applied, logic, modal, temporal}, posted-at = {2006-03-15 19:26:10}, priority = {3}, title = {Temporal Logic Case Study}, url = {http://www.sei.cmu.edu/publications/documents/89.reports/89.tr.024.html}, year = {1989} }

TY - RPRT ID - citeulike:553397 L3 - citeulike-article-id:553397 N2 - 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. TI - Temporal Logic Case Study KW - applied KW - logic KW - modal KW - temporal AU - Wood, William PY - 1989/// UR - http://www.sei.cmu.edu/publications/documents/89.reports/89.tr.024.html ER -