Abstract
We describe a prototype extension of the real-time model checking tool Uppaal with symmetry reduction. The symmetric data type scalarset, which is also used in the Murϕ model checker, was added to Uppaal’s system description language to support the easy static detection of symmetries. Our prototype tool uses state swaps, described and proven sound earlier by Hendriks, to reduce the space and memory consumption of Uppaal. Moreover, the reduction strategy is canonical, which means that the symmetries are optimally used. For all examples that we experimented with (both academic toy examples and industrial cases), we obtained a drastic reduction of both computation time and memory usage, exponential in the size of the scalar sets used.
Supported by the European Community Project IST-2001-35304 (AMETIST), http://ametist.cs.utwente.nl.
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
Abadi, M., Lamport, L.: An old-fashioned recipe for real time. ACM Transactions on Programming Languages and Systems 16(5), 1543–1571 (1994)
Alur, R., Courcoubetis, C., Dill, D.L.: Model checking in dense real time. Information and Computation 104, 2–34 (1993)
Alur, R., Dill, D.L.: Automata for modeling real-time systems. In: 17th International Colloquium on Automata, Languages, and Programming, pp. 322–335 (1990)
Attiya, H., Dwork, C., Lynch, N., Stockmeyer, L.: Bounds on the time to reach agreement in the presence of timing uncertainty. Journal of the ACM 41(1), 122–152 (1994)
Bellman, R.: Dynamic Programming. Princeton University Press, Princeton (1957)
Bosnacki, D., Dams, D., Holenderski, L.: A heuristic for symmetry reductions with scalarsets. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol. 2021, pp. 518–533. Springer, Heidelberg (2001)
Clarke, E.M., Jha, S., Enders, R., Filkorn, T.: Exploiting symmetry in temporal logic model checking. Formal Methods in System Design 9(1/2), 77–104 (1996)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (2000)
Dill, D.: Timing assumptions and verification of finite-state concurrent systems. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 197–212. Springer, Heidelberg (1990)
Dill, D.L., Drexler, A.J., Hu, A.J., Han Yang, C.: Protocol verification as a hardware design aid. In: IEEE International Conference on Computer Design: VLSI in Computers and Processors, pp. 522–525. IEEE Computer Society, Los Alamitos (1992)
Elgaard, L.: The Symmetry Method for Coloured Petri Nets - Theory, Tools, and Practical Use. PhD thesis, Department of Computing Science, University of Aarhus, Denmark (July 2002)
Emerson, E.A., Sistla, A.P.: Symmetry and model checking. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, Springer, Heidelberg (1993)
Havelund, K., Skou, A., Larsen, K.G., Lund, K.: Formal modelling and analysis of an audio/video protocol: An industrial case study using uppaal. In: 18th IEEE Real-Time Systems Symposium, pp. 2–13 (1997)
Hendriks, M.: Enhancing uppaal by exploiting symmetry. Technical Report NIIIR0208, NIII, University of Nijmegen (October 2002)
Hendriks, M., Behrmann, G., Larsen, K.G., Niebert, P., Vaandrager, F.W.: Adding symmetry reduction to uppaal. Technical Report NIII-R03xx, NIII, University of Nijmegen (2003) (to appear)
Henzinger, T.A., Ho, P., Wong-Toi, H.: HyTech: A model checker for hybrid systems. Software Tools for Technology Transfer 1, 110–122 (1997)
Holzmann, G.J.: The spin model checker. IEEE Transactions on Software Engineering 23(5), 279–295 (1997)
Huber, P., Jensen, A.M., Jepsen, L.O., Jensen, K.: Reachability trees for high-level petri nets. Theoretical Computer Science 45(3), 261–292 (1986)
Ip, C.N., Dill, D.L.: Better verification through symmetry. In: Agnew, D., Claesen, L., Camposano, R. (eds.) Computer Hardware Description Languages and their Applications, Ottawa, Canada, pp. 87–100. Elsevier Science Publishers B.V., Amsterdam (1993); Journal version appeared in Formal Methods in System Design 9(1/2), 41–75, 1996
Jensen, K.: Condensed state spaces for symmetrical Coloured Petri Nets. Formal Methods in System Design 9(1/2), 7–40 (1996)
Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a nutshell. International Journal on Software Tools for Technology Transfer, 134–152 (1998)
McMillan, K.L.: Symbolic Model Checking. PhD thesis, Carnegie Mellon University, Pittsburgh (May 1992)
Starke, P.H.: Reachability analysis of petri nets using symmetries. Syst. Anal. Model. Simul./5 8(4), 293–303 (1991)
Tanenbaum, A.S.: Computer Networks. Prentice-Hall, Englewood Cliffs (1996)
Wang, F.: Efficient data structure for fully symbolic verification of real-time software systems. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 157–171. Springer, Heidelberg (2000)
Wang, F., Schmidt, K.: Symmetric symbolic safety-analysis of concurrent software with pointer data structures. In: Peled, D.A., Vardi, M.Y. (eds.) FORTE 2002. LNCS, vol. 2529, pp. 50–64. Springer, Heidelberg (2002)
Yovine, S.: Kronos: a verification tool for real-time systems. International Journal on Software Tools for Technology Transfer 1(2) (1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hendriks, M., Behrmann, G., Larsen, K., Niebert, P., Vaandrager, F. (2004). Adding Symmetry Reduction to Uppaal . In: Larsen, K.G., Niebert, P. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2003. Lecture Notes in Computer Science, vol 2791. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-40903-8_5
Download citation
DOI: https://doi.org/10.1007/978-3-540-40903-8_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21671-1
Online ISBN: 978-3-540-40903-8
eBook Packages: Springer Book Archive