Skip to main content
SpringerLink
Log in

Timed Sequence Diagrams and Tool-Based Analysis — A Case Study

  • Conference paper
  • First Online:
Book cover «UML»’99 — The Unified Modeling Language (UML 1999)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1723))

Included in the following conference series:

Abstract

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.

This author was supported by the DFG project EREAS

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Rajeev Alur and David L. Dill. A theory of timed automata. Theoretical Computer Science, 126:183–235, 1994.

    Article  MATH  MathSciNet  Google Scholar 

  2. Rajeev Alur, Gerard J. Holzmann, and Doron Peled. An analyzer for Message Sequence Charts. In Tiziana Margaria and Bernhard Steffen, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS’96), volume 1055 of LNCS, pages 35–48. Springer-Verlag, 1996.

    Google Scholar 

  3. Grady Booch, james Rumbaugh, and Ivar Jacobson. The Unified Modeling Language User Guide. Addison-Wesley, 1999.

    Google Scholar 

  4. Werner Damm and David Harel. LSCs: Breathing life into Message Sequence Charts. In 3rd IFIP Int. Conference on Formal Methods for Open Object-Based Distributed Systems, (FMOODS’99), pages 293–312. Kluwer Academic Publishers, 1999.

    Google Scholar 

  5. Bruce P. Douglass. Real-Time UML. Addison-Wesley, 1998.

    Google Scholar 

  6. Vincent Encontre. Modeling and implementing correct, scalable and efficient real-time applications with ObjectGEODE. 1rst Quarter Edition of Real-Time Magazine, 1996.

    Google Scholar 

  7. Gerard J. Holzmann and Doron Peled. The state of SPIN. In 8th International Conference on Computer Aided Verification, volume 1102 of LNCS, pages 385–389, New Brunswick, NJ, USA, 1996. Springer Verlag.

    Google Scholar 

  8. Klaus Havelund, Arne Skou, Kim G. Larsen, and Kristian Lund. Formal modelling and analysis of an audio/video protocol: An industrial case study using UPPAAL. In Proceedings of the 18th IEEE Real-Time Systems Symposium, pages 2–13, 1997.

    Google Scholar 

  9. Agnès Lanusse, Sébastian Gérard, and Francois Terrier. Real-time modelling with UML: The ACCORD approach. In UML’ 98, volume 1618 of LNCS, pages 287–296. Springer-Verlag, 1998.

    Google Scholar 

  10. Stefan Leue and Gerard Holzmann. v-Promela: A visual, object-oriented language for SPIN. In Proc. of the 2nd IEEE Intern. Symp. on Object-Oriented Real-Time Distributed Computing. IEEE Computer Society Press, 1999.

    Google Scholar 

  11. Kim G. Larsen, Paul Pettersson, and Wang Yi. Diagnostic model-checking for real-time systems. In Proc. of the 4th DIMACS Workshop on Verification and Control of Hybrid Systems, volume 1066 of LNCS, pages 575–586. Springer-Verlag, 1995.

    Google Scholar 

  12. Kim G. Larsen, Paul Pettersson, and Wang Yi. UPPAAL in a nutshell. Intern. Journal on Software Tools for Technology Transfer, 1(1+2), 1997.

    Google Scholar 

  13. Bran Selic, Garth Gullekson, and Paul T. Ward. Real-Time Object-Oriented Modeling. John Wiley & Sons, 1994.

    Google Scholar 

  14. J. Seemann and J. Wolff von Gudenberg. Extension of UML Sequence Diagrams for real-time systems. In UML’ 98, volume 1618 of LNCS, pages 225–233. Springer-Verlag, 1998.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut für Software, Abteilung Programmierung, Technische Universität Braunschweig, Braunschweig

    Thomas Firley, Michaela Huhn, Karsten Diethers, Thomas Gehrke & Ursula Goltz

Authors
  1. Thomas Firley
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Michaela Huhn
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Karsten Diethers
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Thomas Gehrke
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Ursula Goltz
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, Colorado State University, Fort Collins, CO, 80523-1873, USA

    Robert France

  2. Institut für Informatik, Technische Universität München, D-80290, München, Germany

    Bernhard Rumpe

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Firley, T., Huhn, M., Diethers, K., Gehrke, T., Goltz, U. (1999). Timed Sequence Diagrams and Tool-Based Analysis — A Case Study. In: France, R., Rumpe, B. (eds) «UML»’99 — The Unified Modeling Language. UML 1999. Lecture Notes in Computer Science, vol 1723. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46852-8_45

Download citation

  • DOI: https://doi.org/10.1007/3-540-46852-8_45

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-66712-4

  • Online ISBN: 978-3-540-46852-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation