Skip to main content
SpringerLink
Log in

A Note on Refinement in Hierarchical Transition Systems

  • Conference paper
  • First Online:
Formal Methods for Industrial Critical Systems (FMICS 2018)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 11119))

Abstract

Software engineers frequently employ notations and tools based on transition systems, such as UML state machines and Statecharts, for specifying and reasoning about reactive behaviour. While these notations are typically supported by an operational semantics, they lack a formal underpinning of the incremental refinement practices of engineers who, e.g., place state machines inside states or add outer transitions to states during design. This note sketches how modal transition systems may be applied to formally capture such refinements along state hierarchies, using a hierarchical extension of labelled transition systems that permits engineers to explicitly allow or disallow state refinement and transition extension at each state. A small example testifies to the utility of this framework for hierarchically refining reactive systems.

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 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.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

References

  1. de Alfaro, L., Henzinger, T.A.: Interface automata. In: ESEC/FSE, pp. 109–120. ACM (2001)

    Google Scholar 

  2. Basu, A., Bensalem, S., Bozga, M., Bourgos, P., Sifakis, J.: Rigorous system design: the BIP approach. In: Kotásek, Z., Bouda, J., Černá, I., Sekanina, L., Vojnar, T., Antoš, D. (eds.) MEMICS 2011. LNCS, vol. 7119, pp. 1–19. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-25929-6_1

    Chapter  Google Scholar 

  3. Bauer, S.S., Mayer, P., Schroeder, A., Hennicker, R.: On weak modal compatibility, refinement, and the MIO workbench. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 175–189. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-12002-2_15

    Chapter  MATH  Google Scholar 

  4. Benveniste, A., et al.: Contracts for system design. Found. Trends Electron. Des. Autom. 12(2–3), 124–400 (2018)

    Article  Google Scholar 

  5. Bujtor, F., Fendrich, S., Lüttgen, G., Vogler, W.: Nondeterministic modal interfaces. Theoret. Comput. Sci. 642(C), 24–53 (2016)

    Article  MathSciNet  Google Scholar 

  6. Drusinsky, D.: Modeling and Verification Using UML Statecharts. Newnes (2006)

    Google Scholar 

  7. Eshuis, R.: Reconciling statechart semantics. Sci. Comput. Program. 74(3), 65–99 (2009)

    Article  MathSciNet  Google Scholar 

  8. Fendrich, S., Lüttgen, G.: A generalised theory of interface automata, component compatibility and error. Acta Inf. (2018). https://doi.org/10.1007/s00236-018-0319-8

  9. Garavel, H., Lang, F., Mounier, L.: Compositional verification in action. In: Howar, F., Barnat, J. (eds.) FMICS 2018. LNCS, vol. 11119, pp. 189–210. Springer, Cham (2018)

    Google Scholar 

  10. Glabbeek, R.J.: The linear time - branching time spectrum. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 278–297. Springer, Heidelberg (1990). https://doi.org/10.1007/BFb0039066

    Chapter  Google Scholar 

  11. Graf, S., Quinton, S.: Contracts for BIP: hierarchical interaction models for compositional verification. In: Derrick, J., Vain, J. (eds.) FORTE 2007. LNCS, vol. 4574, pp. 1–18. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73196-2_1

    Chapter  MATH  Google Scholar 

  12. Graf, S., Steffen, B., Lüttgen, G.: Compositional minimisation of finite state systems using interface specifications. Formal Asp. Comput. 8(5), 607–616 (1996)

    Article  Google Scholar 

  13. Ben-Hafaiedh, I., Graf, S., Quinton, S.: Reasoning about safety and progress using contracts. In: Dong, J.S., Zhu, H. (eds.) ICFEM 2010. LNCS, vol. 6447, pp. 436–451. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-16901-4_29

    Chapter  Google Scholar 

  14. Hamon, G., Rushby, J.M.: An operational semantics for Stateflow. STTT 9(5–6), 447–456 (2007)

    Article  Google Scholar 

  15. Harbird, L.: Patterns and Model Transformation Tools for Designing Contractual State Machines. Ph.D thesis, Univ. York, UK (2011)

    Google Scholar 

  16. Harel, D.: Statecharts: a visual formalism for complex systems. Sci. Comput. Program. 8, 231–274 (1987)

    Article  MathSciNet  Google Scholar 

  17. Harel, D., Naamad, A.: The STATEMATE semantics of Statecharts. ACM Trans. Softw. Eng. Methodol. 5(4), 293–333 (1996)

    Article  Google Scholar 

  18. Larsen, K.G.: Modal specifications. In: Sifakis, J. (ed.) Computer Aided Verification. LNCS, vol. 407, pp. 232–246. Springer, Heidelberg (1990). https://doi.org/10.1007/3-540-52148-8_19

    Chapter  Google Scholar 

  19. Lüttgen, G., von der Beeck, M., Cleaveland, R.: A compositional approach to Statecharts semantics. In: FSE, ACM Software Engineering Notes, vol. 25(6), pp. 120–129. ACM (2000)

    Google Scholar 

  20. Mikk, E., Lakhnechi, Y., Siegel, M.: Hierarchical automata as model for Statecharts. In: Shyamasundar, R.K., Ueda, K. (eds.) ASIAN 1997. LNCS, vol. 1345, pp. 181–196. Springer, Heidelberg (1997). https://doi.org/10.1007/3-540-63875-X_52

    Chapter  Google Scholar 

  21. Pnueli, A., Shalev, M.: What is in a step: on the semantics of Statecharts. In: Ito, T., Meyer, A.R. (eds.) TACS 1991. LNCS, vol. 526, pp. 244–264. Springer, Heidelberg (1991). https://doi.org/10.1007/3-540-54415-1_49

    Chapter  Google Scholar 

  22. Quinton, S., Graf, S.: Contract-based verification of hierarchical systems of components. In: SEFM, pp. 377–381. IEEE (2008)

    Google Scholar 

  23. de Roever, W.-P., Lüttgen, G., Mendler, M.: What Is in a step: new perspectives on a classical question. In: Manna, Z., Peled, D.A. (eds.) Time for Verification. LNCS, vol. 6200, pp. 370–399. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-13754-9_15

    Chapter  Google Scholar 

  24. Schmidt, H.: On the Role of Nondeterminism and Refinement in Model-Driven Top-Down Development of Software Systems. Ph.D thesis, Univ. Kiel, Germany (2009)

    Google Scholar 

  25. Steffen, B., Murtovi, A.: M3C: modal meta model checking. In: Howar, F., Barnat, J. (eds.) FMICS 2018. LNCS, vol. 11119, pp. 223–241. Springer, Cham (2018)

    Google Scholar 

Download references

Acknowledgements

Research support was provided by the German Research Foundation (DFG) under grant no. LU 1748/3-2. The author thanks Johannes Gareis for his helpful comments on drafts of this note and for carefully drawing the example figures.

Author information

Authors and Affiliations

  1. Software Technologies Research Group, University of Bamberg, Bamberg, Germany

    Gerald Lüttgen

Authors
  1. Gerald Lüttgen
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Gerald Lüttgen .

Editor information

Editors and Affiliations

  1. Technical University of Dortmund, Dortmund, Germany

    Falk Howar

  2. Masaryk University, Brno, Czech Republic

    Jiří Barnat

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Lüttgen, G. (2018). A Note on Refinement in Hierarchical Transition Systems. In: Howar, F., Barnat, J. (eds) Formal Methods for Industrial Critical Systems. FMICS 2018. Lecture Notes in Computer Science(), vol 11119. Springer, Cham. https://doi.org/10.1007/978-3-030-00244-2_14

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-00244-2_14

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-00243-5

  • Online ISBN: 978-3-030-00244-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation