Toward a backward model checking Online publication date: Thu, 30-Jan-2014
by Aleb Nassima; Tamen Zahia; Kamel Nadjet
International Journal of Computer Aided Engineering and Technology (IJCAET), Vol. 5, No. 1, 2013
Abstract: This paper presents a new method of program verification, backward incremental model checking (BIMC). BIMC is a backward compositional technique to check, statically safety properties of C programs. A program is a hierarchy of blocks. Blocks are analysed in reverse order until we prove or disprove property. To our knowledge, it is the first work dealing with program model checking in a backward way. We define a new method: ASMA for program modelling. ASMA allows separating a program into two components: the data model and the control model. This approach allows an easy program manipulation. BIMC starts the verification with a minimal set P0 which is then incrementally extended each time needed. The weakest precondition concept is applied on the two models in an adequate and incremental way. BIMC allows handling programs containing function calls and pointers. All the techniques described in this paper are illustrated by clarifying examples.
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 Computer Aided Engineering and Technology (IJCAET):
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