Abstract
Danfoss is a Danish manufacturer of refrigeration, motion, heating, and water controls. This paper describes the main results of a project on the modelling and analysis of a Danfoss flowmeter system using Coloured Petri Nets (CP-nets or CPNs). A modern flowmeter system consists of a number of communicating processes, cooperating to make various measurements on, e.g., the flow of water through a pipe. The purpose of the project was to investigate the application of CP-nets for validation of the communication protocols used in the flowmeter system. Analysis by means of state spaces successfully identified problems in the proposed communication protocols. An alternative design was analysed using state spaces reduced by taking advantage of the inherent symmetries in the system. Exploiting the symmetries made it possible to analyse configurations of the flowmeter system approaching the size of typical flowmeter systems.
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
M. Awad, J. Kuusela, and J. Ziegler. Object-Oriented Technology for Real-Time Systems: A Practical Approach using OMT and Fusion. Prentice-Hall, 1996.
ITU (CCITT). Recommendation Z.120: MSC. Technical report, International Telecommunication Union, 1992.
A. Cheng, S. Christensen, and K.H. Mortensen. Model Checking Coloured Petri Nets Exploiting Strongly Connected Components. In M.P. Spathopoulos, R. Smedinga, and P. Kozák, editors, Proceedings WODES’ 96. Institution of Electrical Engineers, Computing and Control Division, Edinburgh, UK, 1996.
S. Christensen. Message Sequence Charts. User’s Manual, January 1997. Available from http://www.daimi.au.dk/designCPN/.
S. Christensen and J.B. Jørgensen. Analysis of Bang and Olufsen’s BeoLink Audio/Video System Using Coloured Petri Nets. In P. Azéma and G. Balbo, editors, Proceedings of ICATPN’97, volume 1248 of Lecture Notes in Computer Science, pages 387–406. Springer-Verlag, 1997.
E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic Verification of Finite State Concurrent Systems using Temporal Logic. ACM Transactions on Programming Languages and Systems, 8(2):244–263, 1986.
E.M. Clarke, R. Enders, T. Filkorn, and S. Jha. Exploiting Symmetries in Temporal Model Logic Model Checking. Formal Methods in System Design, 9, 1996.
J.D. Day and H. Zimmermann. The OSI Reference Model. Proceedings of the IEEE, 71, December 1983.
E.A. Emerson and A. Prasad Sistla. Symmetry and Model Checking. Formal Methods in System Design, 9, 1996.
D.J. Floreani, J. Billington, and A. Dadej. Designing and Verifying a Communications Gateway Using Coloured Petri Nets and Design/CPN. In J. Billington and W. Reisig, editors, Proceedings of ICATPN’96, volume 1091 of Lecture Notes in Computer Science, pages 153–171. Springer-Verlag, 1996.
K. Jensen. Coloured Petri Nets. Basic Concepts, Analysis Methods and Practical Use. Volume 1, Basic Concepts. Monographs in Theoretical Computer Science. Springer-Verlag, 1992.
K. Jensen. Coloured Petri Nets. Basic Concepts, Analysis Methods and Practical Use. Volume 2, Analysis Methods. Monographs in Theoretical Computer Science. Springer-Verlag, 1994.
K. Jensen. Condensed State Spaces for Symmetrical Coloured Petri Nets. Formal Methods in System Design, 9, 1996.
L.M. Kristensen, S. Christensen, and K. Jensen. The Practitioner’s Guide to Coloured Petri Nets. International Journal on Software Tools for Technology Transfer, 2(2):98–132, December 1998.
W. Lawrenz. CAN Contoller Area Network, Grundlagen und Praxis. Hüttig Buch Verlag, Heidelberg, 1994.
Design/CPN Online. http://www.daimi.au.dk/designCPN/.
A. Valmari. Error Detection by Reduced Reachability Graph Generation. In Proceedings of the 9th European Workshop on Application and Theory of Petri Nets, pages 95–112, 1988.
A. Valmari. Stubborn Sets of Coloured Petri Nets. In G. Rozenberg, editor, Proceedings of ICATPN’91, pages 102–121, 1991.
J. Xu and J. Kuusela. Analyzing the Execution Architecture of Mobile Phone Software with Colored Petri Nets. Software Tools for Technology Transfer, 2(2):133–143, December 1998.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lorentsen, L., Kristensen, L.M. (2000). Modelling and Analysis of a DANFOSS Flowmeter System Using Coloured Petri Nets. In: Nielsen, M., Simpson, D. (eds) Application and Theory of Petri Nets 2000. ICATPN 2000. Lecture Notes in Computer Science, vol 1825. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44988-4_20
Download citation
DOI: https://doi.org/10.1007/3-540-44988-4_20
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67693-5
Online ISBN: 978-3-540-44988-1
eBook Packages: Springer Book Archive