Abstract
Quantitative conformance testing of cyber-physical system (CPS) exploits time series of measurements, such as temperature or energy, for validating the correctness of deployed systems. This paper presents the foundations of segmented state space traversal in the setting of quantitative conformance testing of a CPS. It is demonstrated how this strategy together with domain-specific adaptations remedies state space explosion inherent to formal (state-based) verification. The presented contributions improve the scalability of quantitative conformance testing of a CPS and is demonstrated with a case study.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126, 183–235 (1994)
Alur, R., Madhusudan, P.: Decision problems for timed automata: A survey. In: Proc. of SFM 2004, pp. 1–24 (2004)
Behrmann, G., David, A., Larsen, K.G.: A tutorial on uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004)
Bengtsson, J.E., Yi, W.: Timed automata: Semantics, algorithms and tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) Lectures on Concurrency and Petri Nets. LNCS, vol. 3098, pp. 87–124. Springer, Heidelberg (2004)
Bensalem, S., Bozga, M., Krichen, M., Tripakis, S.: Testing conformance of real-time applications by automatic generation of observers. In: Runtime Verification (RV 2004), vol. 113, pp. 23–43 (2004)
Christensen, S., Kristensen, L., Mailund, T.: A sweep-line method for state space exploration. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 450–464. Springer, Heidelberg (2001)
Henzinger, T.A., Manna, Z., Pnueli, A.: What good are digital clocks? In: Kuich, W. (ed.) ICALP 1992. LNCS, vol. 623, pp. 545–558. Springer, Heidelberg (1992)
Larsen, B.N.K.G., Mikucionis, M.: Uppaal Tron User Manual. In: CISS, BRICS, Aalborg University, Aalborg, Denmark (2009)
Krichen, M., Tripakis, S.: Conformance testing for real-time systems. Formal Methods in System Design 34(3), 238–304 (2009)
Lim, R., Woehrle, M., Meier, A., Beutel, J.: Poster abstract: Harvester - energy savings through synchronized low-power listening. In: Adjunct Proc. EWSN 2009, pp. 29–30 (2009)
McMillan, K.L.: Lazy annotation for program testing and verification. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 104–118. Springer, Heidelberg (2010)
Woehrle, M., Lampka, K., Thiele, L.: Exploiting timed automata for conformance testing of power measurements. In: Ouaknine, J., Vaandrager, F.W. (eds.) FORMATS 2009. LNCS, vol. 5813, pp. 275–290. Springer, Heidelberg (2009)
Woehrle, M., Lampka, K., Thiele, L.: Conformance testing for cyber-physical systems. ACM Transactions on Embedded Computing Systems (2011)
Yovine, S.: Model checking timed automata. In: Europ. Educational Forum: School on Embedded Systems, pp. 114–152 (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Woehrle, M., Lampka, K., Thiele, L. (2011). Segmented State Space Traversal for Conformance Testing of Cyber-Physical Systems. In: Fahrenberg, U., Tripakis, S. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2011. Lecture Notes in Computer Science, vol 6919. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-24310-3_14
Download citation
DOI: https://doi.org/10.1007/978-3-642-24310-3_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-24309-7
Online ISBN: 978-3-642-24310-3
eBook Packages: Computer ScienceComputer Science (R0)