Timed sequence diagrams and tool-based analysis: a case study
作者： Ursula Goltz , Thomas Gehrke , Michaela Huhn , Thomas Firley , Karsten Diethers
关键词: Software development 、 Communication diagram 、 Programming language 、 Formal verification 、 Unified Modeling Language 、 Software requirements specification 、 System sequence diagram 、 Embedded system 、 Computer science 、 Sequence diagram 、 Object-oriented programming 、 Protocol (object-oriented programming)
摘要: We use UML timed Sequence Diagrams to specify the realtime behaviour of a communication protocol audio/video components. The build requirements specification against which an implementation developed by Bang & Olufsen company is proven correct.To obtain complete specification, we have mark as optional or mandatory behaviour. Then Diagram interactions with their timing constraints and periods are transferred setting automata. Uppaal tool for verification. In particular, show that conforms concerning correct data transfer on bus.
springer.com
core.ac.uk
acm.org
ornl.gov 
sci-hub.st 参考文章(14)
Rajeev Alur, Gerard J. Holzmann, Doron Peled, An analyzer for message sequence charts tools and algorithms for construction and analysis of systems. pp. 35- 48 ,(1996) , 10.1007/3-540-61042-1_37
Bruce Powel Douglass, Real-time UML ,(1997)
Gerard J. Holzmann, Doron Peled, The State of SPIN computer aided verification. pp. 385- 389 ,(1996) , 10.1007/3-540-61474-5_85
Garth Gullekson, Bran Selic, Paul T. Ward, Real-time object-oriented modeling ,(1994)
Werner Damm, David Harel, LSCs: Breathing Life into Message Sequence Charts formal methods. ,vol. 19, pp. 45- 80 ,(2001) , 10.1023/A:1011227529550
J. Seemann, J. W. von Gudenberg, Extension of UML Sequence Diagrams for Real-Time Systems The Unified Modeling Language. «UML»’98: Beyond the Notation. pp. 240- 252 ,(1999) , 10.1007/978-3-540-48480-6_19
Kim G. Larsen, Paul Pettersson, Wang Yi, UPPAAL in a Nutshell International Journal on Software Tools for Technology Transfer. ,vol. 1, pp. 134- 152 ,(1997) , 10.1007/S100090050010
Rajeev Alur, David L. Dill, A theory of timed automata Theoretical Computer Science. ,vol. 126, pp. 183- 235 ,(1994) , 10.1016/0304-3975(94)90010-8
Doron Peled, Rajeev Alur, Gerard J. Holzmann, An Analyser for Mesage Sequence Charts tools and algorithms for construction and analysis of systems. pp. 35- 48 ,(1996)
Grady Booch, James Rumbaugh, Ivar Jacobson, The Unified Modeling Language User Guide ,(1999)