Abstract
In the previous chapter, a method to prove the consistency of an abstract and a refined model has been proposed. However, this approach is only applicable if a formalized relation \(\text {Ref}\) between the two models is available. Without such a relation, verification of the refinement process is not possible. This scenario may arise when a developer has not documented the refinement process or when several models of the same specification are built independently of each other.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
This cardinality is chosen to keep the SMT instances as simple as possible.
- 2.
We omit these constraints here for the sake of brevity and readability.
References
Antoniol, G., Canfora, G., Casazza, G., Lucia, A.D., Merlo, E.: Recovering traceability links between code and documentation. Trans. Softw. Eng. 28, 970–983 (2002)
och Dag, J.N., Regnell, B., Carlshamre, P., Andersson, M., Karlsson, J.: A feasability study of automated natural language requirements analysis in market-driven development. Requir. Eng. 7, 20–33 (2002)
Hayes, J.H., Dekhtyar, A., Osborne, J.: Improving requirements tracing via information retrieval. In: Requirements Engineering Conference, pp. 138–147 (2003)
Pons, C., Kutsche, R.D.: Traceability across refinement steps in UML modeling. In: Workshop in Software Model Engineering (2004)
Egyed, A.: Consistent adaptation and evolution of class diagrams during refinement. In: Fundamental Approaches to Software Engineering (2004)
Briand, L.C., Labiche, Y., Yue, T.: Automated traceability analysis for UML model refinements. Inf. Softw. Technol. 51, 512–527 (2009)
Doche, M., Gravell, A.: Extraction of abstraction invariants for data refinement. In: Formal Specification and Development in Z and B (2002)
Butler, M.: csp2B: a practical approach to combining CSP and B. In: Formal Methods (1999)
Derrick, J., Smith, G.: Using model checking to automatically find retrieve relations. Electron. Notes Theor. Comput. Sci. 201, 155–175 (2008)
Robinson, N.J.: Finding abstraction relations for data refinement. Technical report, Software Verification Research Center, The University of Queensland (2003)
Robinson, N.J.: Incremental derivation of abstraction relations for data refinement. In: Formal Methods and Software Engineering, pp. 246–265 (2003)
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
Copyright information
© 2017 The Author(s)
About this chapter
Cite this chapter
Seiter, J., Wille, R., Drechsler, R. (2017). Extraction of a Relation for 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_5
Download citation
DOI: https://doi.org/10.1007/978-3-319-41480-5_5
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-41479-9
Online ISBN: 978-3-319-41480-5
eBook Packages: EngineeringEngineering (R0)