Skip to main content
SpringerLink
Log in

Verification of Vertical Refinement

  • Chapter
  • First Online:
Automatic Methods for the Refinement of System Models

Part of the book series: SpringerBriefs in Electrical and Computer Engineering ((BRIEFSELECTRIC))

  • 337 Accesses

Abstract

In this chapter, we discuss solutions to the challenges presented in Sect. 3.2.

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 EPUB and 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

Notes

  1. 1.

    For the sake of clarity, the distinction between abstract and refined model is omitted in this section. We will refer to the refined model by m.

References

  1. Huzar, Z., Kuzniarz, L., Reggio, G., Sourrouille, J.L.: Consistency problems in UML-based software development. In: UML2004 Satellite Activities (2005)

    Google Scholar 

  2. Seiter, J., Wille, R., Kühne, U., Drechsler, R.: Automatic refinement checking for formal system models. In: Forum on specification and Design Languages (2014)

    Google Scholar 

  3. Seiter, J., Wille, R., Kühne, U., Drechsler, R.: Languages, design methods, and tools for electronic systems design: selected contributions from FDL 2014, chap. In: Automatic Refinement Checking for Formal System Models. Springer, Berlin (2015)

    Google Scholar 

  4. Seiter, J., Wille, R., Soeken, M., Drechsler, R.: Determining relevant model elements for the verification of UML/OCL specifications. In: Design, Automation and Test in Europe, pp. 1189–1192 (2013)

    Google Scholar 

  5. Wirth, N.: Program development by stepwise refinement. Commun. ACM 14, 221–227 (1971)

    Article  MATH  Google Scholar 

  6. Back, R.J.: A calculus of refinements for program derivations. Acta Inf. 25, 593–624 (1988)

    Article  MathSciNet  MATH  Google Scholar 

  7. Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, New York (1996)

    Book  MATH  Google Scholar 

  8. Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, New York (2010)

    Book  MATH  Google Scholar 

  9. Woodcock, J., Davies, J.: Using Z: Specification, Refinement, and Proof. Prentice-Hall, Englewood Cliffs (1996)

    MATH  Google Scholar 

  10. Snook, C., Butler, M.: UML-B: Formal Modeling and Design Aided by UML. Softw. Eng. Method. 15, 92–122 (2006)

    Article  Google Scholar 

  11. Ben Ammar, B., Bhiri, M.T., Souquières, J.: Incremental development of UML specifications using operation refinements. Innov. Syst. Softw. Eng. 4, 259–266 (2008). doi:10.1007/s11334-008-0056-1

    Article  Google Scholar 

  12. Biere, A., Cimatti, A., Clarke, E.M., Strichmann, O., Zhu, Y.: Bounded model checking. Adv. Comput. 58, 117–148 (2003)

    Article  Google Scholar 

  13. Glabbeek, R.J.V.: The linear time - branching time spectrum. Concur ’90 Theories Of Concurrency: Unification And Extension, vol. 458, pp. 278–297. Springer, Berlin (1990)

    Chapter  Google Scholar 

  14. Loiseaux, C., Graf, S., Sifakis, J., Bouajjani, A., Bensalem, S., Probst, D.: Property preserving abstractions for the verification of concurrent systems. Form. Methods Syst. Des. 6, 11–44 (1995)

    Article  MATH  Google Scholar 

  15. Nejati, S., Gurfinkel, A., Chechik, M.: Stuttering abstraction for model checking. In: Software Engineering and Formal Methods, p. 311–320 (2005)

    Google Scholar 

  16. Braunstein, C., Encrenaz, E.: CTL-property transformations along an incremental design process. Softw. Tools Technol. Transf. 9, 77–88 (2006). doi:10.1007/s10009-006-0007-9

    Article  MATH  Google Scholar 

  17. Bulychev, P., Konnov, I.V., Zakharov, V.A.: Computing (bi)simulation relations preserving \(CTL^*_X\) for ordinary and fair kripke structures. In: Mathemathical Methods and Algorithms, ISP RAS, pp. 59–76 (2006)

    Google Scholar 

  18. Ranzato, F., Tapparo, F.: Computing stuttering simulations. Concurrency Theory, pp. 542–556. Springer, Berlin (2009)

    Google Scholar 

  19. Leuschel, M., Butler, M.: Automatic refinement checking for B. In: Formal Engineering Methods (2005)

    Google Scholar 

  20. Cabot, J., Clarisó, R., Riera, D.: Verification of UML/OCL class diagrams using constraint programming. In: Software Testing, Verification and Validation, pp. 73–80 (2008)

    Google Scholar 

  21. Cadoli, M., Calvanese, D., Giacomo, G.D., Mancini, T.: Finite model reasoning on UML class diagrams via constraint programming. In: AI*IA, pp. 36–47 (2007)

    Google Scholar 

  22. Anastasakis, K., Bordbar, B., Georg, G., Ray, I.: UML2Alloy: a challenging model transformation. In: Model Driven Engineering Languages and Systems, pp. 436–450. Springer, Berlin (2007)

    Google Scholar 

  23. Soeken, M., Wille, R., Kuhlmann, M., Gogolla, M., Drechsler, R.: Verifying UML/OCL models using boolean satisfiability. In: Design, Automation and Test in Europe, pp. 1341–1344 (2010)

    Google Scholar 

  24. Soeken, M., Wille, R., Drechsler, R.: Verifying dynamic aspects of UML models. In: Design, Automation and Test in Europe, pp. 1077–1082 (2011)

    Google Scholar 

  25. Boiten, E.A.: Introducing extra operations in refinement. Form. Asp. Comput. 26, 305–317 (2012)

    Article  MathSciNet  Google Scholar 

  26. Weiser, M.: Program slicing. In: Software Engineering, pp. 439–449 (1981)

    Google Scholar 

  27. Wille, R., Soeken, M., Drechsler, R.: Debugging of inconsistent UML/OCL models. In: Design, Automation and Test in Europe, pp. 1078–1083 (2012)

    Google Scholar 

  28. Shaikh, A., Clarisó, R., Wiil, U.K., Memon, N.: Verification-driven slicing of UML/OCL models. In: Automated Software Engineering, pp. 185–194 (2010)

    Google Scholar 

  29. Lano, K., Rahimi, S.K.: Slicing of UML models. In: Software and Data Technologies, pp. 259–262 (2010)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Verden, Germany

    Julia Seiter

  2. Johannes Kepler University Linz, Linz, Austria

    Robert Wille

  3. AG Rechnerarchitektur, University of Bremen, Bremen, Germany

    Rolf Drechsler

  4. Cyber-Physical Systems, DFKI GmbH, Bremen, Germany

    Rolf Drechsler

Authors
  1. Julia Seiter
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Robert Wille
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Rolf Drechsler
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Julia Seiter .

Rights and permissions

Reprints and permissions

Copyright information

© 2017 The Author(s)

About this chapter

Cite this chapter

Seiter, J., Wille, R., Drechsler, R. (2017). Verification of Vertical Refinement. In: Automatic Methods for the Refinement of System Models. SpringerBriefs in Electrical and Computer Engineering. Springer, Cham. https://doi.org/10.1007/978-3-319-41480-5_4

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-41480-5_4

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-41479-9

  • Online ISBN: 978-3-319-41480-5

  • eBook Packages: EngineeringEngineering (R0)

Publish with us

Policies and ethics

Search

Navigation