×

HRELTL: a temporal logic for hybrid systems. (English) Zbl 1332.68139

Summary: Hybrid traces are useful to describe behaviors of dynamic systems where continuous and discrete evolutions are combined. The ability to represent sets of traces by means of formulas in temporal logic has recently found important applications in various fields, such as requirements analysis, compositional verification, and contract-based design. In this paper we present HRELTL, a temporal logic to characterize hybrid traces. The logic is highly expressive: it allows the description of continuous behaviors, by expressing mathematical constraints over derivatives, and discrete behaviors, by constraining values of variables across instantaneous transitions. HRELTL combines the power of temporal operators and regular expressions, and enjoys important properties such as sampling invariance.
We demonstrate that the satisfiability problem for a fragment of HRELTL allows for a satisfiability-preserving reduction to RELTL(RA), a logic over discrete traces with atoms in non-linear Real Arithmetic for which automated reasoning procedures are being developed.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
03B44 Temporal logic

Software:

VIS; nuXmv; NuSMV; OCRA; HyTech; PHAVer
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abadi, M.; Lamport, L., Conjoining specifications, ACM Trans. Program. Lang. Syst., 17, 3, 507-534 (1995)
[2] Alur, R.; Courcoubetis, C.; Henzinger, T. A.; Ho, P.-H., Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems, (Hybrid Systems (1992)), 209-229
[3] Alur, R.; Feder, T.; Henzinger, T. A., The benefits of relaxing punctuality, J. ACM, 43, 1, 116-146 (1996) · Zbl 0882.68021
[4] Alur, R.; Henzinger, T. A., Logics and models of real time: a survey, (Rex Workshop (1991)), 74-106
[5] Alur, R.; Henzinger, T. A., Real-time logics: complexity and expressiveness, Inf. Comput., 104, 1, 35-77 (1993) · Zbl 0791.68103
[6] Barrett, C. W.; Sebastiani, R.; Seshia, S. A.; Tinelli, C., Satisfiability modulo theories, (Handbook of Satisfiability (2009)), 825-885
[7] Bauer, S. S.; David, A.; Hennicker, R.; Larsen, K. G.; Legay, A.; Nyman, U.; Wasowski, A., Moving from specifications to contracts in component-based design, (Fase (2012)), 43-58
[8] Benveniste, A.; Caillaud, B.; Ferrari, A.; Mangeruca, L.; Passerone, R.; Sofronis, C., Multiple viewpoint contract-based specification and design, (Fmco (2007)), 200-225 · Zbl 1209.68120
[9] Biere, A.; Heljanko, K.; Junttila, T. A.; Latvala, T.; Schuppan, V., Linear encodings of bounded ltl model checking, Log. Methods Comput. Sci., 2, 5 (2006) · Zbl 1127.68057
[10] Bloem, R.; Cavada, R.; Pill, I.; Roveri, M.; Tchaltsev, A., RAT: a tool for the formal analysis of requirements, (Cav (2007)), 263-267
[11] Bradley, A. R., Sat-based model checking without unrolling, (Vmcai (2011)), 70-87 · Zbl 1317.68109
[12] Brayton, R. K.; Hachtel, G. D.; Sangiovanni-Vincentelli, A. L.; Somenzi, F.; Aziz, A.; Cheng, S.; Edwards, S. A.; Khatri, S. P.; Kukimoto, Y.; Pardo, A.; Qadeer, S.; Ranjan, R. K.; Sarwary, S.; Shiple, T. R.; Swamy, G.; Villa, T., Vis: a system for verification and synthesis, (Cav (1996)), 428-432
[13] Bresolin, D., HyLTL: a temporal logic for model checking hybrid systems, (Has (2013)), 73-84
[14] Bustan, D.; Flaisher, A.; Grumberg, O.; Kupferman, O.; Vardi, M. Y., Regular vacuity, (Charme (2005)), 191-206 · Zbl 1159.68311
[15] Cavada, R.; Cimatti, A.; Dorigatti, M.; Mariotti, A.; Micheli, A.; Mover, S.; Griggio, A.; Roveri, M.; Tonetta, S., The nuXmv symbolic model checker (2014), Fondazione Bruno Kessler
[16] Chaochen, Z.; Hoare, C. A.R.; Ravn, A. P., A calculus of durations, Inf. Process. Lett., 40, 5, 269-276 (1991) · Zbl 0743.68097
[17] Chaochen, Z.; Ravn, A. P.; Hansen, M. R., An extended duration calculus for hybrid real-time systems, (Hybrid Systems (1992)), 36-59
[18] Chiappini, A.; Cimatti, A.; Macchi, L.; Rebollo, O.; Roveri, M.; Susi, A.; Tonetta, S.; Vittorini, B., Formalization and validation of a subset of the European train control system, (Icse (2) (2010)), 109-118
[19] Cimatti, A.; Clarke, E. M.; Giunchiglia, E.; Giunchiglia, F.; Pistore, M.; Roveri, M.; Sebastiani, R.; Tacchella, A., NuSMV 2: an OpenSource tool for symbolic model checking, (Cav (2002)), 359-364 · Zbl 1010.68766
[20] Cimatti, A.; Dorigatti, M.; Tonetta, S., OCRA: a tool for checking the refinement of temporal contracts, (Ase (2013), IEEE), 702-705
[21] Cimatti, A.; Griggio, A.; Mover, S.; Tonetta, S., IC3 modulo theories via implicit predicate abstraction, (Tacas (2014))
[22] Cimatti, A.; Griggio, A.; Mover, S.; Tonetta, S., Verifying LTL properties of hybrid systems with K-liveness, (Computer Aided Verification - Proceedings of the 26th International Conference. Computer Aided Verification - Proceedings of the 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22 (2014)), 424-440
[23] Cimatti, A.; Mover, S.; Tonetta, S., A quantifier-free SMT encoding of non-linear hybrid automata, (Fmcad (2012)), 187-195
[24] Cimatti, A.; Roveri, M.; Susi, A.; Tonetta, S., Object models with temporal constraints, (Sefm 2008 (2008), IEEE Press), 249-258
[25] Cimatti, A.; Roveri, M.; Susi, A.; Tonetta, S., Validation of requirements for hybrid systems: a formal approach, ACM Trans. Softw. Eng. Methodol., 21, 4, 22 (2012)
[26] Cimatti, A.; Roveri, M.; Tonetta, S., Symbolic compilation of PSL, IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst., 27, 10, 1737-1750 (2008)
[27] Cimatti, A.; Roveri, M.; Tonetta, S., Requirements validation for hybrid systems, (Cav (2009)), 188-203 · Zbl 1242.68156
[28] Cimatti, A.; Tonetta, S., A property-based proof system for contract-based design, (Seaa (2012))
[29] Claessen, K., A coverage analysis for safety property lists, (Fmcad (2007), IEEE), 139-145
[30] Claessen, K.; Sörensson, N., A liveness checking algorithm that counts, (Fmcad (2012)), 52-59
[31] Clarke, E. M.; Grumberg, O.; Hamaguchi, K., Another look at LTL model checking, Form. Methods Syst. Des., 10, 1, 47-71 (1997)
[32] de Alfaro, L.; Manna, Z., Verification in continuous time by discrete reasoning, (Amast (1995)), 292-306 · Zbl 1496.68189
[33] Eisner, C.; Fisman, D., A Practical Introduction to Psl (Series on Integrated Circuits and Systems) (2006), Springer-Verlag New York, Inc.
[34] European railway agency
[35] European space agency
[36] ERTMS/ETCS — baseline 3: system requirements specifications. SUBSET-026-1, i3.0.0 (2008)
[38] Feasibility study for the formal specification of ETCS functions (2007), Call for tender
[39] Eveking, H.; Braun, M.; Schickel, M.; Schweikert, M.; Nimbler, V., Multi-level assertion-based design, (Memocode (2007), IEEE), 85-86
[40] Faber, J.; Meyer, R., Model checking data-dependent real-time properties of the European train control system, (Fmcad (2006)), 76-77
[42] Frehse, G., PHAVer: algorithmic verification of hybrid systems past HyTech, (Hscc (2005)), 258-273 · Zbl 1078.93533
[43] Furia, C. A.; Pradella, M.; Rossi, M., Automated verification of dense-time MTL specifications via discrete-time approximation, (Fm (2008)), 132-147
[44] Heitmeyer, C. L., Requirements specifications for hybrid systems, (Hybrid Systems (1995)), 304-314
[45] Henzinger, T. A., The theory of hybrid automata, (Lics (1996)), 278-292
[46] Henzinger, T. A.; Manna, Z.; Pnueli, A., Towards refining temporal specifications into hybrid systems, (Hybrid Systems (1992)), 60-76
[47] Henzinger, T. A.; Manna, Z.; Pnueli, A., What good are digital clocks?, (Icalp (1992)), 545-558 · Zbl 1425.68255
[48] Kapur, A., Interval and point-based approaches to hybrid system verification (1998), Stanford University: Stanford University Stanford, CA, USA, Ph.D. thesis
[49] Kupferman, O.; Vardi, M. Y., Vacuity detection in temporal model checking, Int. J. Softw. Tools Technol. Transf., 4, 2, 224-233 (2003)
[50] Lutz, R. R.; Mikulski, I. C., Requirements discovery during the testing of safety-critical software, (Icse (2003)), 578-585
[51] Lutz, R. R.; Mikulski, I. C., Resolving requirements discovery in testing and operations, (Re (2003), IEEE Computer Society), 33
[52] Maler, O.; Manna, Z.; Pnueli, A., From timed to hybrid systems, (Rex Workshop (1991)), 447-484
[53] Maler, O.; Nickovic, D.; Pnueli, A., Checking temporal properties of discrete, timed and continuous behaviors, (Pillars of Computer Science (2008)), 475-505 · Zbl 1133.68378
[54] Manna, Z.; Pnueli, A., The Temporal Logic of Reactive and Concurrent Systems: Specification (1992), Springer-Verlag
[55] Manna, Z.; Pnueli, A., Verifying hybrid systems, (Hybrid Systems (1992)), 4-35
[56] McMillan, K. L., Interpolation and SAT-based model checking, (Cav (2003)), 1-13 · Zbl 1278.68184
[57] McMillan, K. L., Circular compositional reasoning about liveness, (Charme (1999)), 342-345
[58] Meyer, B., Applying “Design by contract”, Computer, 25, 10, 40-51 (1992)
[59] Mover, S.; Cimatti, A.; Tiwari, A.; Tonetta, S., Time-aware relational abstractions for hybrid systems, (Emsoft (2013), IEEE), 1-10
[60] Pill, I.; Semprini, S.; Cavada, R.; Roveri, M.; Bloem, R.; Cimatti, A., Formal analysis of hardware requirements, (Dac (2006)), 821-826 · Zbl 1160.68401
[61] Platzer, A., Differential dynamic logic for verifying parametric hybrid systems, (Tableaux (2007)), 216-232 · Zbl 1132.68478
[62] Pnueli, A., The temporal logic of programs, (Proceedings of 18th IEEE Symp. on Foundation of Computer Science (1977)), 46-57
[63] The PROSYD project on property-based system design (2007)
[64] Rabinovich, A. M., On the decidability of continuous time specification formalisms, J. Log. Comput., 8, 5, 669-678 (1998) · Zbl 0913.03018
[65] SafeCer project
[66] Sheeran, M.; Singh, S.; Stålmarck, G., Checking safety properties using induction and a sat-solver, (Fmcad (2000)), 108-125
[67] Tiwari, A., Abstractions for hybrid systems, Form. Methods Syst. Des., 32, 1, 57-83 (2008) · Zbl 1133.68368
[68] Vijayaraghavan, S.; Ramanathan, M., A Practical Guide for SystemVerilog Assertions (2005), Springer
[69] Vizel, Y.; Grumberg, O., Interpolation-sequence based model checking, (Fmcad (2009), IEEE), 1-8
[70] Wang, F., Time-progress evaluation for dense-time automata with concave path conditions, (Atva (2008)), 258-273 · Zbl 1183.68384
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.