Title: Theory and methodology of object-oriented formal modelling

Authors: Guo Xie; Ding Liu; Xinhong Hei; Tianhua Xu

Addresses: Xi'an University of Technology, Shaanxi, Xi'an 710048, China ' Xi'an University of Technology, Shaanxi, Xi'an 710048, China ' Xi'an University of Technology, Shaanxi, Xi'an 710048, China ' State Key Laboratory of Rail Traffic Control and Safety, Beijing Jiaotong University, 100044 China

Abstract: 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.

Keywords: formal modelling; reliability; correctness; object-oriented modelling; safety critical systems; UML; model validation; model verification; function model; data structure.

DOI: 10.1504/IJSNET.2014.067099

International Journal of Sensor Networks, 2014 Vol.16 No.4, pp.252 - 260

Received: 23 Jun 2014
Accepted: 24 Jun 2014
Published online: 26 Jan 2015 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article