In: Azéma, P.; Balbo, G.: Lecture Notes in Computer Science, Vol. 1248: 18th International Conference on Application and Theory of Petri Nets, Toulouse, France, June 1997, pages 387-406. Berlin, Germany: Springer-Verlag, June 1997.
Abstract: Bang & Olufsen A/S (B&O) is a renowned manufacturer of audio and video products. Their BeoLink system distributes sound and vision throughout a home via a network. In this way, e.g., while doing the cooking in the kitchen, a person can remotely select and listen to a track from a CD loaded in the CD player situated in the living room. To resolve conflicts, synchronisation between various actions is needed, and is indeed taken care of by appropriate communication protocols. The purpose of the project described in this paper was to test Coloured Petri Nets (CP-nets or CPN) as a way to improve B&O's methods for specification, validation, and verification of protocols. In the main experiment, an engineer from B&O used the Design/CPN tool to build a CPN model of vital parts of BeoLink, to validate its behaviour using simulations with a familiar graphical feedback, and to formally verify crucial properties using occurrence graphs (also known as state spaces and reachability graphs/trees). The latter activity demonstrated the applicability of occurrence graphs for timed CP-nets. Moreover, CPN was used to examine important aspects of a possible future revision of BeoLink, and to check compatibility between the new and the old version. Based on the experiments reported in this paper, CPN has been included in the set of methods for specification, validation, and verification of future protocols at B&O.
Keywords: System design and verification using nets; higher-level net models; computer tools for nets; experience with using nets, case studies; application of nets to protocols and embedded systems.