Theory and methodology of object-oriented formal modelling Online publication date: Mon, 26-Jan-2015
by Guo Xie; Ding Liu; Xinhong Hei; Tianhua Xu
International Journal of Sensor Networks (IJSNET), Vol. 16, No. 4, 2014
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.
Existing subscribers:
Go to Inderscience Online Journals to access the Full Text of this article.
If you are not a subscriber and you just want to read the full contents of this article, buy online access here.Complimentary Subscribers, Editors or Members of the Editorial Board of the International Journal of Sensor Networks (IJSNET):
Login with your Inderscience username and password:
Want to subscribe?
A subscription gives you complete access to all articles in the current issue, as well as to all articles in the previous three years (where applicable). See our Orders page to subscribe.
If you still need assistance, please email subs@inderscience.com
Our Blog 
Follow us on Twitter 
Visit us on Facebook