Meta-Modelling for Formal Software Development

AbstractFormal refinement shows how the specification of a program can be transformed by steps into an executable implementation. The method is sound and rigorous but is not suited to dealing with large and complex programs. Thus, the construction of large programs is often assumed to remain outside the scope of formal representation altogether and informal techniques, sometimes using diagrammatic notations, are used to go from requirements to programs.In this paper, we show how large programs can be defined in terms of different views that are instances of a single meta model. Each view represents one set of properties of the program and their composition defines the specification of the program. Transformations are used to convert views into program fragments that are composed together to build the whole program. The technique has been applied for the construction of many large systems that are in practical use