Abstract:

The engineering of systems that are acceptably correct is a hard problem. On the one hand, semi-formal modelling approaches that are used in practical, large-scale system development, such as the UML, are not amenable to formal analysis and consistency checking. On the other hand, formal modelling and analysis requires a level of competence and expertise that is not common in commercial development communities, and formal approaches are not well integrated with the rest of the development process. This paper advocates an approach to building engineering environments (or frameworks) for rigorous model-driven development (MDD) that is based on combining semi-formal notations with formal modelling languages. To support the approach, there is a formal language of templates, which captures patterns of formal development and enables an approach to proof with templates. This allows the construction of catalogues of patterns (represented as templates) and meta-theorems for frameworks. The paper presents and illustrates a framework for sequential systems that combines UML and the formal language Z.