Abstract
On-line model checking is a recent technique to overcome limitations of model checking if accurate system models are not available. At certain times during on-line model checking it is necessary to adjust the current model state to the real-world state and to do so in an efficient way. This paper presents a general, graph-based transformation reduction and applies it to reduce the length of transformation sequences needed to reach particular states in the model checker UPPAAL. Our evaluation shows that, generally, for the length of those sequences upper bounds exist independently from the elapsed time in the system. It follows that our proposed method is capable of fulfilling the real-time requirements imposed by on-line model checking.
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.
Similar content being viewed by others
References
Alur, R., Courcoubetis, C., Halbwachs, N., Dill, D., Wong-Toi, H.: Minimization of Timed Transition Systems. In: Cleaveland, W.R. (ed.) CONCUR 1992. LNCS, vol. 630, pp. 340–354. Springer, Heidelberg (1992)
Alur, R., La Torre, S., Pappas, G.J.: Optimal Paths in Weighted Timed Automata. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A. (eds.) HSCC 2001. LNCS, vol. 2034, pp. 49–62. Springer, Heidelberg (2001)
Asarin, E., Maler, O.: As Soon as Possible: Time Optimal Control for Timed Automata. In: Vaandrager, F.W., van Schuppen, J.H. (eds.) HSCC 1999. LNCS, vol. 1569, pp. 19–30. Springer, Heidelberg (1999)
Behrmann, G., Bengtsson, J., David, A., Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL Implementation Secrets. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol. 2469, pp. 3–22. Springer, Heidelberg (2002)
Bengtsson, J.: Clocks, DBMs and States in Timed Systems. Ph.D. thesis, Uppsala University (2002)
Bengtsson, J., Jonsson, B., Lilius, J., Yi, W.: Partial Order Reductions for Timed Systems. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 485–500. Springer, Heidelberg (1998)
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)
Bulychev, P., David, A., Larsen, K., Mikučionis, M., Bøgsted Poulsen, D., Legay, A., Wang, Z.: UPPAAL-SMC: Statistical Model Checking for Priced Timed Automata. In: Wiklicky, H., Massink, M. (eds.) QAPL 2012. EPTCS, vol. 85, pp. 1–16 (2012)
Janowska, A., Penczek, W.: Path Compression in Timed Automata. Fundamenta Informaticae 79(3-4), 379–399 (2007)
Jensen, H., Larsen, K., Skou, A.: Modelling and Analysis of a Collision Avoidance Protocol using SPIN and UPPAAL. BRICS (1996)
Larsen, K.G., Behrmann, G., Brinksma, E., Fehnker, A., Hune, T., Pettersson, P., Romijn, J.: As Cheap as Possible: Efficient Cost-Optimal Reachability for Priced Timed Automata. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 493–505. Springer, Heidelberg (2001)
Larsen, K., Larsson, F., Pettersson, P., Yi, W.: Compact Data Structures and State-Space Reduction for Model-Checking Real-Time Systems. Real-Time Systems 25(2-3), 255–275 (2003)
Larsen, K., Pettersson, P., Yi, W.: Model-Checking for Real-Time Systems. In: Reichel, H. (ed.) FCT 1995. LNCS, vol. 965, pp. 62–88. Springer, Heidelberg (1995)
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 Co-design Approach for Medical Device Plug-and-Play (MDPnP). In: ICCPS 2012, pp. 13–22. IEEE (2012)
Li, T., Wang, Q., Tan, F., Bu, L., Cao, J.N., Liu, X., Wang, Y., Zheng, R.: From Offline Long-Run to Online Short-Run: Exploring A New Approach of Hybrid Systems Model Checking for MDPnP. In: HCMDSS-MDPnP 2011 (2011)
Lönn, H., Pettersson, P.: Formal Verification of a TDMA Protocol Start-Up Mechanism. In: PRFTS 1997, pp. 235–242. IEEE (1997)
Vaandrager, F., de Groot, A.: Analysis of a biphase mark protocol with UPPAAL and PVS. Formal Aspects of Computing 18(4), 433–458 (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Rinast, J., Schupp, S., Gollmann, D. (2014). A Graph-Based Transformation Reduction to Reach UPPAAL States Faster. In: Jones, C., Pihlajasaari, P., Sun, J. (eds) FM 2014: Formal Methods. FM 2014. Lecture Notes in Computer Science, vol 8442. Springer, Cham. https://doi.org/10.1007/978-3-319-06410-9_37
Download citation
DOI: https://doi.org/10.1007/978-3-319-06410-9_37
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-06409-3
Online ISBN: 978-3-319-06410-9
eBook Packages: Computer ScienceComputer Science (R0)