Abstract
We present a practical approach to a formal analysis of UML-based models. This is achieved by an underlying formal representation in Z, which allows us to pose and discharge conjectures to analyse models. We show how our approach allows us to consistency-check UML models, and model analysis by simply drawing snapshot diagrams.
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
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Saaltink, M.: The Z/EVES system. In: Till, D., P. Bowen, J., Hinchey, M.G. (eds.) ZUM 1997. LNCS, vol. 1212. Springer, Heidelberg (1997)
Amálio, N., Polack, F., Stepney, S.: A sound modelling framework for sequential systems I: Modelling. Technical Report YCS-2004, Department of Computer Science, University of York (2004)
Amálio, N., Stepney, S., Polack, F.: Modular UML semantics: Interpretations in Z based on templates and generics. In: Van, H.D., Liu, Z. (eds.) FACS 2003: Formal Aspects of Component Software, Int. Workshop, Pisa, Italy, vol. 284, pp. 81–100. UNU/IIST Technical Report (2003)
D’Sousa, D., Wills, A.C.: Object Components and Frameworks with UML: the Catalysis approach. Addison-Wesley, Reading (1998)
Amálio, N., Polack, F.: Comparison of formalisation approaches of UML class constructs in Z and Object-Z. In: Bert, et al. (eds.) [9], pp. 339–358
Jackson, D.: Structuring Z specifications with views. ACM Transactions on Software Engineering and Methodology (TOSEM) 4(4), 365–389 (1995)
Stepney, S., Polack, F., Toyn, I.: Patterns to guide practical refactoring: examples targetting promotion in Z. In: Bert, et al. (eds.) [9], pp. 20–39
Jackson, D.: Alloy: A lightweight object modelling notation. ACM Transactions on Software Engineering and Methodology 11(2), 256–290 (2002)
Bert, D., P. Bowen, J., King, S. (eds.): ZB 2003. LNCS, vol. 2651. Springer, Heidelberg (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Amálio, N., Stepney, S., Polack, F. (2004). Formal Proof from UML Models. In: Davies, J., Schulte, W., Barnett, M. (eds) Formal Methods and Software Engineering. ICFEM 2004. Lecture Notes in Computer Science, vol 3308. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30482-1_35
Download citation
DOI: https://doi.org/10.1007/978-3-540-30482-1_35
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23841-6
Online ISBN: 978-3-540-30482-1
eBook Packages: Springer Book Archive