Abstract
In this paper we present the continuous and on-going development of datastructures and algorithms underlying the verification engine of the tool UppaaL. In particular, we review the datastructures of Difference Bounded Matrices, Minimal Constraint Representation and Clock Difference Diagrams used in symbolic state-space representation and -analysis for real-time systems.
In addition we report on distributed versions of the tool, and outline the design and experimental results for new internal datastructures to be used in the next generation of UppaaL.
Finally, we mention work on complementing methods involving acceleration, abstraction and compositionality.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Tobias Amnell, Gerd Behrmann, Johan Bengtsson, Pedro R. D’Argenio, Alexandre David, Ansgar Fehnker, Thomas Hune, Bertrand Jeannet, Kim G. Larsen, M. Oliver Möller, Paul Pettersson, Carsten Weise, and Wang Yi. Uppaal-Now, Next, and Future. In F. Cassez, C. Jard, B. Rozoy, and M. Ryan, editors, Modelling and Verification of Parallel Processes, number 2067 in Lecture Notes in Computer Science, pages 100–125. Springer-Verlag, 2001.
Luca Aceto, Augusto Burgueno, and Kim G. Larsen. Model checking via reachability testing for timed automata. In Bernhard Steffen, editor, Proc. 4th Int. Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’98), volume 1384 of Lecture Notes in Computer Science, pages 263–280. Springer, 1998.
Marius Bozga, Conrado Daws, Oded Maler, Alfredo Olivero, Stavros Tripakis, and Sergio Yovine. Kronos: A model-Checking Tool for Real-Time Systems. In Proc. of the 10th Int. Conf. on Computer Aided Verification, number 1427 in Lecture Notes in Computer Science, pages 546–550. Springer-Verlag, 1998.
Gerd Behrmann. A performance study of distributed timed automata reachability analysis. Submitted.
Richard Bellman. Dynamic Programming. Princeton University Press, 1957.
Johan Bengtsson. Clocks, DBMs and STates in Timed Systems. PhD thesis, Faculty of Science and Technology, Uppsala University, 2002.
Gerd Behrmann, Ansgar Fehnker, Thomas S. Hune, Kim Larsen, Paul Petterson, and Judi Romijn. Efficient guiding towards cost-optimality in uppaal. In Proc. of TACAS’2001, Lecture Notes in Computer Science. Springer-Verlag, 2001.
Johan Bengtsson, W.O. David Griffioen, Kåre J. Kristoffersen, Kim G. Larsen, Fredrik Larsson, Paul Pettersson, and Wang Yi. Verification of an Audio Protocol with Bus Collision Using Uppaal. In Rajeev Alur and Thomas A. Henzinger, editors, Proc. of the 8th Int. Conf. on Computer Aided Verification, number 1102 in Lecture Notes in Computer Science, pages 244–256. Springer-Verlag, July 1996.
Gerd Behrmann, Thomas Hune, and Frits Vaandrager. Distributed timed model checking-How the search order matters. In Proc. of 12th International Conference on Computer Aided Verification, Lecture Notes in Computer Science, Chicago, Juli 2000. Springer-Verlag.
Johan Bengtsson, Kim G. Larsen, Fredrik Larsson, Paul Pettersson, and Wang Yi. Uppaal in 1995. In Proc. of the 2nd Workshop on Tools and Algorithms for the Construction and Analysis of Systems, number 1055 in Lecture Notes in Computer Science, pages 431–434. Springer-Verlag, March 1996.
Gerd Behrmann, Kim G. Larsen, Justin Pearson, Carsten Weise, and Wang Yi. Efficient Timed Reachability Analysis Using Clock Difference Diagrams. In Proc. of the 11th Int. Conf. on Computer Aided Verification, number 1633 in Lecture Notes in Computer Science. Springer-Verlag, 1999.
Randal E. Bryant. Graph-Based Algorithms for Boolean Function Manipulation. IEEE Trans. on Computers, 1986.
K.M. Chandy and J. Misra. Parallel Program Design: A Foundation. Addison Wesley, 1988.
Alexandre David, Gerd Behrmann, Kim G. Larsen, and Wang Yi. The next generation of uppaal. Submitted.
H. Dierks. Specification and Verification of Polling Real-Time Systems. PhD thesis, Carl von Ossietzky Universität Oldenburg, July 1999.
David Dill. Timing Assumptions and Verification of Finite-State Concurrent Systems. In J. Sifakis, editor, Proc. of Automatic Verification Methods for Finite State Systems, number 407 in Lecture Notes in Computer Science, pages 197–212. Springer-Verlag, 1989.
Conrado Daws and Stavros Tripakis. Model checking of real-time reachability properties using abstractions. In Bernard Steffen, editor, Proc. of the 4th Workshop on Tools and Algorithms for the Construction and Analysis of Systems, number 1384 in Lecture Notes in Computer Science, pages 313–329. Springer-Verlag, 1998.
C. Daws and S. Yovine. Two examples of verification of multirate timed automata with Kronos. In Proc. of the 16th IEEE Real-Time Systems Symposium, pages 66–75. IEEE Computer Society Press, December 1995.
Martijn Hendriks. Devlopment of reactive programs using uppaal. Master’s thesis, KUN, Nijmegen University, 2002.
Martin Hndriks and Kim G. Larsen. Exact acceleration of real-time model checking. In Theory and Practice of Timed Systems, volume 65 of Electronic Notes in Theoretical Computer Science. Elsevier Science Publishers, 2002.
Klaus Havelund, Kim G. Larsen, and Arne Skou. Formal verification of a power controller using the real-time model checker Uppaal. In Proceedings of AMST 1999, volume 1601 of Lecture Notes in Computer Science, pages 277–298, 1999.
C.A.R. Hoare. Communicating Sequential Processes. Communications of the ACM, 21(8):666–677, 1978.
Gerard J. Holzmann. On limits and possibilities of automated protocol analysis. In Proc. 7th IFIP WG 6.1 Int. Workshop on Protocol Specification, Testing, and Verification, pages 137–161, 1987.
Thomas S. Hune. Modeling a language for embedded systems in timed automata. Technical Report RS-00-17, BRICS, Basic Research in computer Science, August 2000. 26 pp. Earlier version entitled Modelling a Real-Time Language appeared in FMICS99, pages 259–282.
Torsten K. Iversen, Kåre J. Kristoffersen, Kim G. Larsen, Morten Laursen, Rune G. Madsen, Steffen K. Mortensen, Paul Pettersson, and Chris B. Thomasen. Model-Checking Real-Time Control Programs —Verifying LEGO Mindstorms Systems Using Uppaal. In Proc. of 12th Euromicro Conference on Real-Time Systems, pages 147–155. IEEE Computer Society Press, June 2000.
Henrik Ejersbo Jensen, Kim G. Larsen, and Arne Skou. Scaling up Uppaal-automatic verification of real-time systems using compositionality and abstraction. In Proceedings of FTRTFT 2000, volume 1926 of Lecture Notes in Computer Science, pages 19–30, 2000.
C. Jones. Tentative steps toward a development method for interfering programs. ACM Transactions on Programming Languages and Systems, 5(4):596–620, 1983.
Leslie Lamport. A Fast Mutual Exclusion Algorithm. ACM Trans. on Computer Systems, 5(1):1–11, February 1987. Also appeared as SRC Research Report 7.
Kim G. Larsen, Fredrik Larsson, Paul Pettersson, and Wang Yi. Efficient Verification of Real-Time Systems: Compact Data Structures and State-Space Reduction. In Proc. of the 18th IEEE Real-Time Systems Symposium, pages 14–24. IEEE Computer Society Press, December 1997.
Kim G. Larsen, Fredrik Larsson, Paul Pettersson, and Wang Yi. Compact data structure and state-space reduction for model-checking real-time systems. Real-Time Systems-the International Journal of Time-Critical Computing Systems, 2002. To appear-accepted for publication.
Henrik Lönn and Paul Pettersson. Formal Verification of a TDMA Protocol Startup Mechanism. In Proc. of the Pacific Rim Int. Symp. on Fault-Tolerant Systems, pages 235–242, December 1997.
Kim G. Larsen, Paul Pettersson, and Wang Yi. Compositional and Symbolic Model-Checking of Real-Time Systems. In Proc. of the 16th IEEE Real-Time Systems Symposium, pages 76–87. IEEE Computer Society Press, December 1995.
Kim G. Larsen, Paul Pettersson, and Wang Yi. Uppaal in a Nutshell. Int. Journal on Software Tools for Technology Transfer, 1(1-2):134–152, October 1997.
Kim G. Larsen, Carsten Weise, Wang Yi, and Justin Pearson. Clock Difference Diagrams. Nordic Journal of Computing, 6(3):271–298, 1999.
R. Milner. Communication and Concurrency. Prentice Hall, Englewood Cliffs, 1989.
J. Møller, J. Lichtenberg, H. R. Andersen, and H. Hulgaard. Difference decision diagrams. In Proceedings 13th International Conference on Computer Science Logic, volume 1683 of Lecture Notes in Computer Science, pages 111–125, Madrid, Spain, September 1999.
J. Møller, J. Lichtenberg, H. R. Andersen, and H. Hulgaard. Fully symbolic model checking of timed systems using difference decision diagrams. In Proceedings First International Workshop on Symbolic Model Checking, volume 23-2 of Electronic Notes in Theoretical Computer Science, Trento, Italy, July 1999.
S. Owicki and D. Gries. An Axiomatic Proof Technique for Parallel Programs I. Acta Informatica, 6(4):319–340, 1976.
Paul Pettersson. Modelling and Analysis of Real-Time Systems Using Timed Automata: Theory and Practice. PhD thesis, Department of Computer Systems, Uppsala University, February 1999.
Wolfgang J. Paul and Janos Simon. Decision Trees and Random Access Machines. In Logic and Algorithmic, volume 30 of Monographie de L’Enseignement Mathématique, pages 331–340. L’Enseignement Mathématique, Université de Genève, 1980.
Tomas Gerhard Rokicki. Representing and Modeling Digital Circuits. PhD thesis, Stanford University, 1993.
D.P.L. Simons and M.I.A. Stoelinga. Mechanical verification of the IEEE 1394a root contention protocol using Uppaal2k. Springer International Journal of Software Tools for Technology Transfer, 2001.
Karsten Strehl and Lothar Thiele. Symbolic Model Checking of Process Networks Using Interval Diagram Techniques. In Proceedings of the IEEE/ACM International Conference on Computer-Aided Design (ICCAD-98), pages 686–692, 1998.
Howard Wong-Toi. Symbolic Approximations for Verifying Real-Time Systems. PhD thesis, Standford University, 1995.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Behrmann, G., Bengtsson, J., David, A., Larsen, K.G., Pettersson, P., Yi, W. (2002). UppaaL Implementation Secrets. In: Damm, W., Olderog, E.R. (eds) Formal Techniques in Real-Time and Fault-Tolerant Systems. FTRTFT 2002. Lecture Notes in Computer Science, vol 2469. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45739-9_1
Download citation
DOI: https://doi.org/10.1007/3-540-45739-9_1
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-44165-6
Online ISBN: 978-3-540-45739-8
eBook Packages: Springer Book Archive