Abstract
uppaalport is a new tool for component-based design and analysis of embedded systems. It operates on the hierarchically structured continuous time component modeling language SaveCCM and provides efficient model-checking by using partial-order reduction techniques that exploits the structure and the component behavior of the model. uppaalport is implemented as an extension of the verification engine in the uppaal tool. The tool can be used as back-end in to the Eclipse based SaveCCM integrated development environment, which supports user friendly editing, simulation, and verification of models.
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.
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 subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Åkerholm, M., Carlson, J., Fredriksson, J., Hansson, H., Håkansson, J., Möller, A., Pettersson, P., Tivoli, M.: The SAVE approach to component-based development of vehicular systems. Journal of Systems and Software 80(5), 655–667 (2007)
Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)
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)
Bortnik, E., Trčka, N., Wijs, A.J., Luttik, S.P., van de Mortel-Fronczak, J.M., Baeten, J.C.M., Fokkink, W.J., Rooda, J.E.: Analyzing a χ model of a turntable system using Spin, CADP and Uppaal. Journal of Logic and Algebraic Programming 65(2), 51–104 (2005)
Bouyer, P., Haddad, S., Reynier, P.-A.: Timed unfoldings for networks of timed automata. In: Graf, S., Zhang, W. (eds.) ATVA 2006. LNCS, vol. 4218, pp. 292–306. Springer, Heidelberg (2006)
Carlson, J., Håkansson, J., Pettersson, P.: SaveCCM: An analysable component model for real-time systems. In: Proc. of the 2nd Workshop on Formal Aspects of Components Software (FACS 2005). Electronic Notes in Theoretical Computer Science. Elsevier, Amsterdam (2005)
Cassez, F., Chatain, T., Jard, C.: Symbolic unfoldings for networks of timed automata. In: Graf, S., Zhang, W. (eds.) ATVA 2006. LNCS, vol. 4218, pp. 307–321. Springer, Heidelberg (2006)
David, A., Behrmann, G., Larsen, K.G., Yi, W.: A tool architecture for the next generation of UPPAAL. In: Aichernig, B.K., Maibaum, T.S.E. (eds.) Formal Methods at the Crossroads. From Panacea to Foundational Support. LNCS, vol. 2757, pp. 352–366. Springer, Heidelberg (2003)
Gössler, G., Sifakis, J.: Composition for component-based modelling. Science of Computer Programming 55(1-3), 161–183 (2005)
Håkansson, J., Pettersson, P.: Partial order reduction for verification of real-time components. In: Proc. of 1st International Workshop on Formal Modeling and Analysis of Timed Systems. LNCS. Springer, Heidelberg (2007)
Lugiez, D., Niebert, P., Zennou, S.: A partial order semantics approach to the clock explosion problem of timed automata. Theoretical Computer Science 345(1), 27–59 (2005)
Minea, M.: Partial order reduction for model checking of timed automata. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 431–446. Springer, Heidelberg (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Håkansson, J., Carlson, J., Monot, A., Pettersson, P., Slutej, D. (2008). Component-Based Design and Analysis of Embedded Systems with UPPAAL PORT. In: Cha, S.(., Choi, JY., Kim, M., Lee, I., Viswanathan, M. (eds) Automated Technology for Verification and Analysis. ATVA 2008. Lecture Notes in Computer Science, vol 5311. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-88387-6_23
Download citation
DOI: https://doi.org/10.1007/978-3-540-88387-6_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-88386-9
Online ISBN: 978-3-540-88387-6
eBook Packages: Computer ScienceComputer Science (R0)