Formal proof from UML models

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