Skip to main content
SpringerLink
Log in

Generation and Validation of Frame Conditions in Formal Models

  • Conference paper
  • First Online:
Book cover Model-Driven Engineering and Software Development (MODELSWARD 2018)

Part of the book series: Communications in Computer and Information Science ((CCIS,volume 991))

  • 552 Accesses

Abstract

Operation contracts are a popular description means in behavioral system modeling. Pre- and postconditions are used to describe the effects on model elements (such as attributes, links, etc.) that are enforced by an operation. However, it is usually not clearly stated what model elements may be affected by an operation call and what shall remain unchanged—although this information is essential in order to obtain a comprehensive description. A promising solution to this so-called frame problem is to define additional frame conditions. However, properly defining frame conditions which complete the model description in the intended way can be a non-trivial, tedious, and error-prone task. While in general there are several tools and methods for obtaining formal model descriptions and also a broad variety of approaches for the validation and verification of the generated models, corresponding methods for frame conditions have not received significant attention so far. In this work, we provide a comprehensive overview of recently proposed approaches that close this gap and support the designer in generating and validating frame conditions.

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

Notes

  1. 1.

    This chapter is an extension of the work previously published at [25].

  2. 2.

    Note that the postconditions might also refer to the pre-state of the operation (\(\sigma _1\)) using the suffix @pre as, e.g., for Turnstile::goThrough() in the running example.

  3. 3.

    Modifies only statements were originally introduced as invariability clauses by Kosiuczenko [19]. A variation of this idea is to specify the set of variable model elements within the postconditions using an OCL primitive modifiedOnly(Set) [5].

  4. 4.

    In addition to limiting the sequence length, all these approaches require further problem bounds in order to limit the search space, i.e., they need to be provided with a fixed number or at least a range of objects that shall be instantiated as well as a finite domain for all data types.

  5. 5.

    Note that, in the following, an abstract description is provided which is sufficient for the purposes of this work. For a more detailed treatment of the respective formulation, we refer to [30].

  6. 6.

    Note that the solver will always conclude at some point due to the finite search space.

References

  1. Ahrendt, W., et al.: The KeY tool. Softw. Syst. Model. 4(1), 32–54 (2005)

    Article  Google Scholar 

  2. Anastasakis, K., Bordbar, B., Georg, G., Ray, I.: UML2Alloy: a challenging model transformation. In: Engels, G., Opdyke, B., Schmidt, D.C., Weil, F. (eds.) MODELS 2007. LNCS, vol. 4735, pp. 436–450. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-75209-7_30

    Chapter  Google Scholar 

  3. Beckert, B., Schmitt, P.H.: Program verification using change information. In: SEFM, p. 91 (2003)

    Google Scholar 

  4. Borgida, A., Mylopoulos, J., Reiter, R.: On the frame problem in procedure specifications. IEEE Trans. Softw. Eng. 21, 785–798 (1995)

    Article  Google Scholar 

  5. Brucker, A.D., Tuong, F., Wolff, B.: Featherweight OCL: a proposal for a machine-checked formal semantics for OCL 2.5. Archive of Formal Proofs (2014)

    Google Scholar 

  6. Brucker, A.D., Wolff, B.: HOL-OCL: a formal proof environment for uml/ocl. In: Fiadeiro, J.L., Inverardi, P. (eds.) FASE 2008. LNCS, vol. 4961, pp. 97–100. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78743-3_8

    Chapter  Google Scholar 

  7. Cabot, J.: Ambiguity issues in OCL postconditions. In: OCL Workshop, pp. 194–204 (2006)

    Google Scholar 

  8. Cabot, J.: From declarative to imperative UML/OCL operation specifications. In: Parent, C., Schewe, K.-D., Storey, V.C., Thalheim, B. (eds.) ER 2007. LNCS, vol. 4801, pp. 198–213. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-75563-0_15

    Chapter  Google Scholar 

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

    Google Scholar 

  10. Cabot, J., Clarisó, R., Riera, D.: Verifying UML/OCL operation contracts. In: Leuschel, M., Wehrheim, H. (eds.) IFM 2009. LNCS, vol. 5423, pp. 40–55. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-00255-7_4

    Chapter  Google Scholar 

  11. Choppy, C., Klai, K., Zidani, H.: Formal verification of UML state diagrams: a Petri net based approach. Softw. Eng. Notes 36(1), 1–8 (2011)

    Article  Google Scholar 

  12. de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24

    Chapter  Google Scholar 

  13. Demuth, B., Wilke, C.: Model and object verification by using dresden OCL. In: IIT-TP, p. 81. Technical University (2009)

    Google Scholar 

  14. de Dios, M.A.G., Dania, C., Basin, D., Clavel, M.: Model-driven development of a secure ehealth application. In: Heisel, M., Joosen, W., Lopez, J., Martinelli, F. (eds.) Engineering Secure Future Internet Services and Systems. LNCS, vol. 8431, pp. 97–118. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-07452-8_4

    Chapter  Google Scholar 

  15. Gogolla, M., Büttner, F., Richters, M.: USE: a UML-based specification environment for validating UML and OCL. Sci. Comput. Program. 69(1–3), 27–34 (2007)

    Article  MathSciNet  Google Scholar 

  16. Gogolla, M., Hamann, L., Hilken, F., Kuhlmann, M., France, R.B.: From application models to filmstrip models: an approach to automatic validation of model dynamics. In: Modellierung, pp. 273–288 (2014)

    Google Scholar 

  17. Gogolla, M., Kuhlmann, M., Hamann, L.: Consistency, independence and consequences in UML and OCL models. In: Dubois, C. (ed.) TAP 2009. LNCS, vol. 5668, pp. 90–104. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02949-3_8

    Chapter  Google Scholar 

  18. Hilken, F., Niemann, P., Gogolla, M., Wille, R.: Filmstripping and unrolling: a comparison of verification approaches for UML and OCL behavioral models. In: Seidl, M., Tillmann, N. (eds.) TAP 2014. LNCS, vol. 8570, pp. 99–116. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-09099-3_8

    Chapter  Google Scholar 

  19. Kosiuczenko, P.: Specification of invariability in OCL. In: Nierstrasz, O., Whittle, J., Harel, D., Reggio, G. (eds.) MODELS 2006. LNCS, vol. 4199, pp. 676–691. Springer, Heidelberg (2006). https://doi.org/10.1007/11880240_47

    Chapter  Google Scholar 

  20. Kosiuczenko, P.: Specification of invariability in OCL - specifying invariable system parts and views. Softw. Syst. Model. 12(2), 415–434 (2013)

    Article  MathSciNet  Google Scholar 

  21. Leino, K.R.M.: This is Boogie 2. Technical report (2008). http://research.microsoft.com/apps/pubs/default.aspx?id=147643

  22. Meyer, B.: Applying design by contract. IEEE Comput. 25(10), 40–51 (1992)

    Article  Google Scholar 

  23. Niemann, P., Hilken, F., Gogolla, M., Wille, R.: Assisted generation of frame conditions for formal models. In: DATE, pp. 309–312 (2015)

    Google Scholar 

  24. Niemann, P., Hilken, F., Gogolla, M., Wille, R.: Extracting frame conditions from operation contracts. In: MoDELS, pp. 266–275 (2015)

    Google Scholar 

  25. Niemann, P., Przigoda, N., Wille, R., Drechsler, R.: Analyzing frame conditions in UML/OCL models - consistency equivalence and independence. In: MODELSWARD, pp. 139–151 (2018)

    Google Scholar 

  26. OMG - Object Management Group: Object Constraint Language (2014). http://www.omg.org/spec/OCL/2.4. Version 2.4, February 2014

  27. Przigoda, N., Filho, J.G., Niemann, P., Wille, R., Drechsler, R.: Frame conditions in symbolic representations of UML/OCL models. In: MEMOCODE, pp. 65–70 (2016)

    Google Scholar 

  28. Przigoda, N., Hilken, C., Wille, R., Peleska, J., Drechsler, R.: Checking concurrent behavior in UML/OCL models. In: MoDELS, pp. 176–185 (2015)

    Google Scholar 

  29. Przigoda, N., Niemann, P., Filho, J.G., Wille, R., Drechsler, R.: Frame conditions in the automatic validation and verification of UML/OCL models: a symbolic formulation of modifies only statements. Comput. Lang. Syst. Struct. (2017). https://doi.org/10.1016/j.cl.2017.11.002

    Article  Google Scholar 

  30. Przigoda, N., Soeken, M., Wille, R., Drechsler, R.: Verifying the structure and behavior in UML/OCL models using satisfiability solvers. IET Cyber-Phys. Syst.: Theory Appl. 1(1), 49–59 (2016). https://doi.org/10.1049/iet-cps.2016.0022

    Article  Google Scholar 

  31. Przigoda, N., Stoppe, J., Seiter, J., Wille, R., Drechsler, R.: Verification-driven design across abstraction levels: a case study. In: DSD, pp. 375–382. IEEE Computer Society (2015)

    Google Scholar 

  32. Przigoda, N., Wille, R., Drechsler, R.: Ground setting properties for an efficient translation of OCL in SMT-based model finding. In: MoDELS, pp. 261–271 (2016)

    Google Scholar 

  33. Rumbaugh, J., Jacobson, I., Booch, G. (eds.): The Unified Modeling Language Reference Manual. Addison-Wesley Longman Ltd., Essex (1999)

    Google Scholar 

  34. Soeken, M., Wille, R., Drechsler, R.: Verifying dynamic aspects of UML models. In: DATE, pp. 1077–1082 (2011)

    Google Scholar 

  35. Soeken, M., Wille, R., Kuhlmann, M., Gogolla, M., Drechsler, R.: Verifying UML/OCL models using Boolean satisfiability. In: DATE, pp. 1341–1344 (2010)

    Google Scholar 

Download references

Acknowledgments

This work was supported by the German Federal Ministry of Education and Research (BMBF) within the project SELFIE under grant no. 01IW16001 and the Deutsche Forschungsgemeinschaft (German Research Foundation, DFG) within the Reinhart Koselleck project under grant no. DR287/23-1.

Author information

Authors and Affiliations

  1. Group for Computer Architecture, University of Bremen, Bremen, Germany

    Philipp Niemann & Rolf Drechsler

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

    Philipp Niemann, Robert Wille & Rolf Drechsler

  3. Siemens Mobility GmbH, Braunschweig, Germany

    Nils Przigoda

  4. Institute for Integrated Circuits, Johannes Kepler University Linz, Linz, Austria

    Robert Wille

Authors
  1. Philipp Niemann
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Nils Przigoda
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Robert Wille
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Rolf Drechsler
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Philipp Niemann .

Editor information

Editors and Affiliations

  1. Université d’Angers/ESEO, Angers, France

    Slimane Hammoudi

  2. University of Twente, Enschede, The Netherlands

    LuĂ­s Ferreira Pires

  3. Malina Software Corp., Nepean, ON, Canada

    Bran Selic

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Niemann, P., Przigoda, N., Wille, R., Drechsler, R. (2019). Generation and Validation of Frame Conditions in Formal Models. In: Hammoudi, S., Pires, L., Selic, B. (eds) Model-Driven Engineering and Software Development. MODELSWARD 2018. Communications in Computer and Information Science, vol 991. Springer, Cham. https://doi.org/10.1007/978-3-030-11030-7_12

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-11030-7_12

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-11029-1

  • Online ISBN: 978-3-030-11030-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation