PROJECT PLAN A Survey and Analysis on Metric Temporal Logic Yang Liu Department of Computer Sciences, The University of Texas at Austin [email protected] Abstract Temporal logics have been successfully used in specification, verification and validation of reactive system. However, real-time system cannot be well modeled by classic temporal logic because of its weak expressiveness on timing properties. Metric Temporal Logic (MTL) extends the classic temporal logic model by turning qualitative temporal operators into quantitative temporal operators. This paper examines a decent survey on MTL and its role in specifying properties by different verification methods outside of model checking, such as runtime monitoring, performance analysis and theorem proving. A sample system as a case study will be further presented to show how the timing properties in real-time system can be expressed by MTL and verified by a MTL model checker. Introduction Temporal logics have been successfully used in specification, verification and validation of reactive system. However, classic temporal logics have limitation on modeling real-time system. Since the quantitative properties could not be expressed by qualitative temporal operators. Metric Temporal Logic (MTL) as a timed temporal logic is an extension of Linear Temporal Logic (LTL) with time-constrained modalities that includes quantitative requirement on the elapse of time. This project examines a decent survey on MTL and its role in specifying properties by different verification methods outside of model checking, such as runtime monitoring, performance analysis and theorem proving. In additional, a system, which is modeled by MTL and is verified by a model checker, would be given as a case study. This paper will start from an overview of classic temporal logic and then claim the two ways of achieving the quantitative timing extension. In the following part, I will introduce and analyze the syntax and semantics of the basic and derived construction in MTL. The comparison and analyze of expressiveness between MTL and other timed temporal logics will be further proposed. MTL as a timed temporal logic is not only used in model checking but also plays an important role in some other verification methods. The second section of my project will survey MTL’ role in different verification methods rather than model checking. I intend to gather and summarize the different research jobs, which utilize MTL to be the model logic. The possible area would be runtime monitoring, performance analysis and theorem proving. In the third section, I will do a case study, which model and verify a time sensitive system by MTL. A special model checker would be chosen later. The result of model checking will be presented at last.Reference. [Koy90] R. Koymans. Specifying Real-Time Properties with Metric Temporal Logic Real-Time Systems 2(4), pages 255-299. Kluwer, 1990. [AH92] R. Alur and T. A. Henzinger. Logics and Models of Real-Time: A Survey. In Real Time: Theory in Practice, volume 600 of Lecture Notes in Computer Science, pages 74-106. Springer-Verlag, 1992. [PB00] P. Bellini, R. Mattolini, and P. Nesi. Temporal logics for real-time system specification. ACM Computing Surveys, 32(1):12–42, 2000. [DD03] D. Drusinsky, Monitoring temporal rules combined with time series, in: Proc. CAV’03: Computer Aided Verification, Lecture Notes in Computer Science, Vol. 2725, Boulder, USA, Springer, Berlin, 2003, pp. 114–118. [PT04] P. Thati, G. Rosu, Monitoring algorithms for metric temporal logic, in: Proc. RV’04: Fourth Internat. Workshop on Runtime Verification, Electronic Notes in Theoretical Computer Science, vol. 113, Barcelona, Spain, Elsevier Science, Amsterdam, 2004. [Dru06] D. Drusinsky. On-line monitoring of metric temporal logic with time-series constraints using alternating finite automata. J. UCS, 12(5):482–498, 2006. [AM96] A. Montanari, Metric and layered temporal logic for time granularity, ILLC Dissertation Series 1996-02, University of Amsterdam (1996). [SK04] S. Konrad and B. H. C. Cheng. Real-time specification patterns. Technical Report MSU-CSE-04-37, Computer Science and Engineering, Michigan State University, East Lansing, Michigan, September 2004 [MP97] A. Montanari and A. Policriti. Executing metric temporal logic. In C. Brzoska and M. Fisher, editors, Proc. of the IJCAI’97 Workshop on Programming in Temporal and Non Classical Logics, 1997. [CB95] C. Brzoska. Temporal Logic Programming with Metric and Past Operators. In Executable Modal and Temporal Logics. Springer Verlag, 1995. [BMP+07] Domenico Bianculli, Angelo Morzenti, Matteo Pradella, Pierluigi San Pietro, and Paola Spoletini. Trio2Promela: A model checker for temporal metric specifications. In ICSE Companion, pages 61– 62, 2007. Project Schedule Start End Description Expected output 09/13 09/18 Choose the project topic Project topic 09/19 09/23 Preliminary reading and discussion Project plan 09/23 10/01 LTL, MTL and other TTL Part | of final project paper 10/01 10/15 MTL in other verification methods Part II of final project paper 10//16 11/16 Case Study Part ||| of final project paper 11/16 12/1 Make final paper and presentation Final paper and
View Full Document
Unlocking...