Abstract
In the context of run-time model checking, it could be desirable to prioritize and schedule the verification of system properties, so that the verification process, too, meets the time constraints of the underlying online experiment. In this paper, we introduce the Quantitative Metric Temporal Logic for Verification Time (QMTL-VT) to formally describe these constraints on verification time for properties formulated in a given temporal logic. Using QMTL-VT, we can query for satisfaction of time constraints (\(\mathcal {V}\)), the bounds of execution times (\(\mathcal {V}_{I}\)), and the probability of being checkable within these bounds (\(\mathcal {V}_{P}\)). Building up on that, we can execute queries under temporal conditions (\(\mathcal {V}_{C}\)), express their order (\(\mathcal {V}_{S}\)), and provide alternatives (\(\mathcal {V}_{A}\)) for the case of constraint violations. We apply a tool implementation of QMTL-VT to a set of UPPAAL sample models to demonstrate how to perform verification of given properties under real-time constraints, and discuss syntax and semantics in a medical case study on heart-motion tracking as an online real-time scenario.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsReferences
Rinast, J.: An online model-checking framework for timed automata. Ph.D. thesis, Technische Universität Hamburg (2015)
Dasarathy, B.: Timing constraints of real-time systems: constructs for expressing them, methods of validating them. IEEE Trans. Softw. Eng. SE–11(1), 80–86 (1985)
Wang, F.: Timing behavior analysis for real-time systems. In: Proceedings of Tenth Annual IEEE Symposium on Logic in Computer Science, pp. 112–122 (1995)
Xu, J., Parnas, D.L.: On satisfying timing constraints in hard-real-time systems. IEEE Trans. Softw. Eng. 19, 70–84 (1993)
Buttazzo, G.C.: Hard Real-Time Computing Systems: Predictable Scheduling Algorithms and Applications, vol. 24. Springer, Heidelberg (2011). https://doi.org/10.1007/978-1-4614-0676-1
Lisper, B., Nordlander, J.: A simple and flexible timing constraint logic. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012. LNCS, vol. 7610, pp. 80–95. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-34032-1_12
Pelánek, R.: Reduction and abstraction techniques for model checking. Ph.D. thesis, Masarykova univerzita, Fakulta informatiky (2006)
Grosu, R., Smolka, S.A.: Monte Carlo model checking. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 271–286. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-31980-1_18
Dershowitz, N., Hanna, Z., Katz, J.: Bounded model checking with QBF. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 408–414. Springer, Heidelberg (2005). https://doi.org/10.1007/11499107_32
Kumar, R., Mercer, E.G.: Load balancing parallel explicit state model checking. Electron. Notes Theor. Comput. Sci. 128(3), 19–34 (2005)
Ferdinand, C., Heckmann, R.: aiT: worst-case execution time prediction by static program analysis. In: Jacquart, R. (ed.) Building the Information Society. IIFIP, vol. 156, pp. 377–383. Springer, Boston (2004). https://doi.org/10.1007/978-1-4020-8157-6_29
Edgar, S., Burns, A.: Statistical analysis of WCET for scheduling. In: Proceedings of 22nd IEEE Real-Time Systems Symposium (RTSS 2001), pp. 215–224 (2001)
Kim, S., Patel, H.D., Edwards, S.A.: Using a Model Checker to Determine Worst-Case Execution Time. Computer Science Technical Report CUCS-038-09. Columbia University, New York (2009)
Al-Bataineh, O., Reynolds, M., French, T.: Accelerating worst case execution time analysis of timed automata models with cyclic behaviour. Formal Aspects Comput. 27, 917–949 (2015)
Li, T., Tan, F., Wang, Q., Bu, L., Cao, J.N., Liu, X.: From offline toward real time: a hybrid systems model checking and cps codesign approach for medical device plug-and-play collaborations. IEEE Trans. Parallel Distrib. Syst. 25, 642–652 (2014)
Filieri, A., Ghezzi, C., Tamburrelli, G.: Run-time efficient probabilistic model checking. In: Proceedings of the 33rd International Conference on Software Engineering (ICSE), pp. 341–350 (2011)
Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects Comput. 6, 512–535 (1994)
STS Institute, Website of the QMTL-VT tool implementation (2018). https://www.tuhh.de/sts/research/model-checking-abstract-interpretation/qmtl-vt.html
Chen, T., Diciolla, M., Kwiatkowska, M., Mereacre, A.: Quantitative verification of implantable cardiac pacemakers. In: 2012 IEEE 33rd Real-Time Systems Symposium (RTSS), pp. 263–272. IEEE (2012)
Antoni, S.T., et al.: Model checking for trigger loss detection during Doppler ultrasound-guided fetal cardiovascular MRI. Int. J. Comput. Assist. Radiol. Surg. 13, 1755–1766 (2018)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Lehmann, S., Antoni, ST., Schlaefer, A., Schupp, S. (2019). A Quantitative Metric Temporal Logic for Execution-Time Constrained Verification. In: Chamberlain, R., Taha, W., Törngren, M. (eds) Cyber Physical Systems. Model-Based Design. CyPhy WESE 2018 2018. Lecture Notes in Computer Science(), vol 11615. Springer, Cham. https://doi.org/10.1007/978-3-030-23703-5_9
Download citation
DOI: https://doi.org/10.1007/978-3-030-23703-5_9
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-23702-8
Online ISBN: 978-3-030-23703-5
eBook Packages: Computer ScienceComputer Science (R0)