In: Gianfranco Ciardo, Philippe Darondeau (Eds.): Lecture Notes in Computer Science, Vol. 3536: Applications and Theory of Petri Nets 2005: 26th International Conference, ICATPN 2005, Miami, USA, June 20-25, 2005., pages 403-422. Springer Verlag, June 2005.
Abstract: Safety-critical systems are systems that can cause undesired loss or damage to life, property, or the environment. Standards for developing safety-critical software often recommend that semi-formal or formal methods should be used to specify, analyze, and verify the behavior of safety-critical software. This paper presents results from a project in which Coloured Petri Nets were used to specify and analyze software safety requirements of a frequency converter being developed by Danfoss Drives. Frequency converters are used to control the speed of motors. The analysis of the model revealed behavior which could lead to hazardous situations or unnecessary failures. Prototype tool support was developed for validating the behavior of an Java-based executable software architecture prototype against the CP-net that specified the desired behavior of the software.