Abstract
Our increasing reliance on software systems requires reliable software. Mainstream software manufacture, however, is not rigorous and precise, and resulting software lacks the desired reliability. Formal methods take a rigorous and precise approach to software development, delivering reliable software, but they are widely recognised as being impractical. Although the situation is improving, the costs of achieving reliable software are still high and formal methods are only used when absolutely necessary.
This thesis investigates how reuse can contribute to improving the practicality of formal modelling methods, and how diagrammatic modelling notations and formal methods can be integrated for rigorous, but practical development of software systems.
The thesis proposes GeFoRME, an approach to building domain-specific frameworks based on templates that make a combined use of formal methods and diagrammatic modelling languages. To express templates, the thesis develops the language FTL, which generates sentences of some language upon instantiation and enables proof with templates of formal models.
The thesis then develops UML+Z a framework for object-oriented modelling for general purpose sequential systems that combines UML and Z. FTL is used to build UML+Z 's catalogue of templates and meta-theorems, which generates Z models and simplifies their proofs of consistency. The thesis also develops an approach to formal analysis with snapshot diagrams.
Full thesis : PDF 2MB