Skip to main content
SpringerLink
Log in

Embedded Software Analysis with MOTOR

  • Chapter
Formal Methods for the Design of Real-Time Systems (SFM-RT 2004)

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

Included in the following conference series:

Abstract

This paper surveys the language Modest, a Modelling and Description language for Stochastic and Timed systems, and its accompanying tool-environment MOTOR. The language and tool are aimed to support the modular description and analysis of reactive systems while covering both functional and non-functional system aspects such as hard and soft real-time, and quality-of-service aspects. As an illustrative example, the modeling and analysis of a device-absence detecting protocol in plug-and-play networks is described and is shown to exhibit some undesired behaviour.

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

Access this chapter

Log in via an institution
eBook
USD 16.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 16.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. Alur, R., Dill, D.L.: A theory of timed automata. Th. Comp. Sc. 126(2), 183–235 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  2. Amnell, T., Behrmann, G., Bengtsson, J., D’Argenio, P.R., David, A., Fehnker, A., Hune, T., Jeannet, B., Larsen, K.G., Möller, M.O., Pettersson, P., Weise, C., Yi, W.: Uppaal – Now, next, and future. In: Cassez, F., Jard, C., Rozoy, B., Dermot, M. (eds.) MOVEP 2000. LNCS, vol. 2067, pp. 99–124. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  3. Baier, C., Ciezinski, F., Groesser, M.: Probmela: a modeling language for communicating probabilistic processes. In: Int. Conf. on Formal Methods and Models for Codesign, ACM Press, New York (2004)

    Google Scholar 

  4. Belinfante, A., Feenstra, J., de Vries, R.G., Tretmans, J., Goga, N., Feijs, L., Mauw, S., Heerink, L.: Formal test automation: a simple experiment. In: Int. Workshop on Testing of Communicating Systems XII, pp. 179–196. Kluwer, Dordrecht (1999)

    Google Scholar 

  5. Ben-Ari, M.: Principles of Concurrent and Distributed Programming. Prentice-Hall, Englewood Cliffs (1990)

    MATH  Google Scholar 

  6. Berry, G.: Preemption and concurrency. In: Shyamasundar, R.K. (ed.) FSTTCS 1993. LNCS, vol. 761, pp. 72–93. Springer, Heidelberg (1993)

    Google Scholar 

  7. Bodlaender, M., Guidi, J., Heerink, L.: Enhancing discovery with liveness. In: IEEE Consumer Comm. and Networking Conf., IEEE CS Press, Los Alamitos (2004)

    Google Scholar 

  8. Bohnenkamp, H., Courtney, T., Daly, D., Derisavi, S., Hermanns, H., Katoen, J.-P., Lam, V., Sanders, W.H.: On integrating the Möbius and MoDeST modeling tools. In: Dependable Systems and Networks, pp. 671–672. IEEE CS Press, Los Alamitos (2003)

    Google Scholar 

  9. Bohnenkamp, H., D’Argenio, P.R., Hermanns, H., Katoen, J.-P., Klaren, J.: Modest: A compositional modeling formalism for real-time and stochastic systems (2004) (in preparation)

    Google Scholar 

  10. Bohnenkamp, H., Gorter, J., Guidi, J., Katoen, J.-P.: A simple and fair protocol to detect node absence in dynamic distributed systems (2004) (in preparation)

    Google Scholar 

  11. Bohnenkamp, H., Hermanns, H., Katoen, J.-P., Klaren, J.: The Modest modelling tool and its implementation. In: Kemper, P., Sanders, W.H. (eds.) TOOLS 2003. LNCS, vol. 2794, pp. 116–133. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  12. Bohnenkamp, H., Hermanns, H., Klaren, J., Mader, A., Usenko, Y.S.: Synthesis and stochastic assessment of schedules for lacquer production. In: Quantitative Evaluation of Systems, IEEE CS Press, Los Alamitos (2004) (to appear)

    Google Scholar 

  13. Bornot, S., Sifakis, J.: An algebraic framework for urgency. Inf. and Comp. 163, 172–202 (2001)

    Article  MathSciNet  Google Scholar 

  14. Special issue on embedded systems. IEEE Computer 33(9) (2000)

    Google Scholar 

  15. Bravetti, M., Gorrieri: The theory of interactive generalized semi-Markov processes. Th. Comp. Sc. 282(1), 5–32 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  16. D’Argenio, P.R., Hermanns, H., Katoen, J.-P., Klaren, J.: Modest: A modelling language for stochastic timed systems. In: de Luca, L., Gilmore, S. (eds.) PROBMIV 2001, PAPM-PROBMIV 2001, and PAPM 2001. LNCS, vol. 2165, pp. 87–104. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  17. D’Argenio, P.R., Katoen, J.-P., Ruys, T.C., Tretmans, G.: The bounded retransmission protocol must be on time! In: Brinksma, E. (ed.) TACAS 1997. LNCS, vol. 1217, pp. 416–431. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  18. Deavours, D., Clark, G., Courtney, T., Daly, D., Derasavi, S., Doyle, J., Sanders, W.H., Webster, P.: The Möbius framework and its implementation. IEEE Tr. on Softw. Eng. 28(10), 956–970 (2002)

    Article  Google Scholar 

  19. Fernandez, J.-C., Garavel, H., Mounier, L., Rasse, A., Rodriguez, C., Sifakis, J.: A tool box for the verification of LOTOS programs. In: 14th IEEE Int. Conf. on Softw. Eng. (1992)

    Google Scholar 

  20. Gafni, E., Mitzenmacher, M.: Analysis of timing-based mutual exclusion with random times. SIAM J. Comput. 31(3), 816–837 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  21. Garavel, H., Sighireanu, M.: On the introduction of exceptions in E-LOTOS. In: Formal Description Techniques IX, pp. 469–484. Kluwer, Dordrecht (1996)

    Google Scholar 

  22. Glynn, P.W.: A GSMP formalism for discrete event systems. Proc. of the IEEE 77(1), 14–23 (1989)

    Article  Google Scholar 

  23. Gorter, J.: Modeling and analysis of the liveness UPnP extension. Master’s thesis, Univ. of Twente (2004)

    Google Scholar 

  24. Hermanns, H.: Interactive Markov Chains – the Quest for Quantified Quality. In: Hermanns, H. (ed.) Interactive Markov Chains. LNCS, vol. 2428, p. 57. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  25. Hermanns, H., Katoen, J.-P., Meyer-Kayser, J., Siegle, M.: A tool for model checking Markov chains. J. on Software Tools for Technology Transfer 4(2), 153–172 (2003)

    Article  Google Scholar 

  26. Hillston, J.: A Compositional Approach to Performance Modelling. Cambr. Univ. Press, Cambridge (1996)

    Book  Google Scholar 

  27. Hoare, C.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)

    MATH  Google Scholar 

  28. Holzmann, G.J.: The Spin Model Checker. Addison-Wesley, Reading (2002)

    Google Scholar 

  29. Jansen, D.N., Hermanns, H., Usenko, Y.S.: From StoCharts to Modest: a comparative reliability analysis of train radio communications (2004) (submitted)

    Google Scholar 

  30. Jelasity, M., Kowalczyk, W., van Steen, M.: Newscast computing. Tech. Rep. IR-CS-006, Vrije Univ. Amsterdam (2003)

    Google Scholar 

  31. Kwiatkowska, M., Norman, G., Segala, R., Sproston, J.: Automatic verification of real-time systems with discrete probability distributions. Th. Comp. Sc. 282, 101–150 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  32. Lee, E.A.: Embedded software. In: Zelkowitz, M. (ed.) Advances in Computers, vol. 56, Academic Press, London (2002)

    Google Scholar 

  33. Meyer, J.F., Movaghar, A., Sanders, W.H.: Stochastic activity networks: structure, behavior and application. In: Int. Workshop on Timed Petri Nets, pp. 106–115 (1985)

    Google Scholar 

  34. Plotkin, G.D.: A structural approach to operational semantics. DAIMI FN-19, Aarhus University (1981)

    Google Scholar 

  35. Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. John Wiley & Sons, Chichester (1994)

    MATH  Google Scholar 

  36. Raynal, M., Tronel, F.: Group membership failure detection: a simple protocol and its probabilistic analysis. Distrib. Syst. Engng 6, 95–102 (1999)

    Article  Google Scholar 

  37. van Renesse, R., Minsky, Y., Hayden, M.: A gossip-style failure detection service. In: IFIP Conf. on Distributed Systems, Platforms, and Open Distributed Processing, pp. 55–70 (1998)

    Google Scholar 

  38. de Roever, W.-P., de Boer, F.S., Hannemann, U., Hooman, J., Lakhnech, Y., Poel, M., Zwiers, J.: Concurrency Verification: Introduction to Compositional and Noncompositional Methods. Cambridge Univ. Press, Cambridge (2001)

    MATH  Google Scholar 

  39. Sanders, W.H., Meyer, J.F.: Stochastic activity networks: formal definitions and concepts. In: Brinksma, E., Hermanns, H., Katoen, J.-P. (eds.) EEF School 2000 and FMPA 2000. LNCS, vol. 2090, pp. 315–344. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  40. Schneider, F.B., Bloom, B., Marzullo, K.: Putting time into proof outlines. In: Huizing, C., de Bakker, J.W., Rozenberg, G., de Roever, W.-P. (eds.) REX 1991. LNCS, vol. 600, pp. 618–639. Springer, Heidelberg (1992)

    Chapter  Google Scholar 

  41. Segala, R., Lynch, N.A.: Probabilistic simulations for probabilistic processes. Nordic J. of Computing 2(2), 250–273 (1995)

    MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Faculty of Electrical Engineering, Mathematics and Computer Science, University of Twente, The Netherlands

    Joost-Pieter Katoen, Henrik Bohnenkamp, Ric Klaren & Holger Hermanns

  2. Saarland University, D-66123, Saarbrücken, Germany

    Holger Hermanns

Authors
  1. Joost-Pieter Katoen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Henrik Bohnenkamp
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Ric Klaren
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Holger Hermanns
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Istituto di Scienze e Tecnologie dell’Informazione, Università di Urbino “Carlo Bo”, Italy

    Marco Bernardo

  2. Dipartimento di Matematica ed Informatica, University of Camerino, Via Madonna delle Carceri 9, 62032, Camerino, Italy

    Flavio Corradini

Rights and permissions

Reprints and permissions

Copyright information

© 2004 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Katoen, JP., Bohnenkamp, H., Klaren, R., Hermanns, H. (2004). Embedded Software Analysis with MOTOR. In: Bernardo, M., Corradini, F. (eds) Formal Methods for the Design of Real-Time Systems. SFM-RT 2004. Lecture Notes in Computer Science, vol 3185. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30080-9_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-30080-9_9

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-23068-7

  • Online ISBN: 978-3-540-30080-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation