We use UML timed Sequence Diagrams to specify the real-time behaviour of a communication protocol of audio/video components. The Sequence Diagrams build the requirements specification against which an implementation of the protocol developed by the Bang & Olufsen company is proven correct. To obtain a complete requirements specification, we have to mark the UML Sequence Diagrams as optional or mandatory behaviour. Then the Sequence Diagram interactions with their timing constraints and periods are transferred to a setting of timed automata. We use the Uppaal tool for verification. In particular, we show that the implementation of the protocol conforms to the Sequence Diagram specification concerning the correct data transfer on the bus.
CITATION STYLE
Firley, T., Huhn, M., Diethers, K., Gehrke, T., & Goltz, U. (1999). Timed sequence diagrams and tool-based analysis— A case study. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1723, pp. 645–660). Springer Verlag. https://doi.org/10.1007/3-540-46852-8_45
Mendeley helps you to discover research relevant for your work.