Theory and methodology of object-oriented formal modelling

摘要

Although formal methods (FMs) are highly recommended by several International Standards for safety critical systems, almost all of the existing work on FMs focused on formal models which only have internal inconsistencies. How to guarantee the external consistency (or correctness) of a formal model, i.e., Satisfying the expectations of users, is a great challenge. In this paper, a strategy to improve the correctness of formal models is proposed by establishing, validating and verifying the function model and data structure separately, and fusing them finally, as the following steps. Firstly UML models are created to graphically express the system structure, and examine the structural completeness and reasonability. Secondly, hybrid automata are created to characterise system behaviours and analyse system action properties. Lastly, an object-oriented VDM++ model is established based on the transformation from hybrid automata to VDM++ functions, and from UML model to VDM++ data structure.