Proof-based verification approaches for dynamic properties: application to the information system domain

This paper proposes a formal approach for generating necessary and sufficient proof obligations to demonstrate a set of dynamic properties using the B method. In particular, we consider reachability, non-interference and absence properties. Also, we show that these properties permit a wide range of...

Full description

Saved in:
Bibliographic Details
Published in:Formal aspects of computing 2015-03, Vol.27 (2), p.335-374
Main Authors: Mammar, Amel, Frappier, Marc
Format: Article
Language:English
Subjects:
Computation
Computer Science
Dynamic mechanical properties
Dynamical systems
Dynamics
Information systems
Math Applications in Computer Science
Original Article
Proving
Symbolic Computation
Theory of Computation
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:This paper proposes a formal approach for generating necessary and sufficient proof obligations to demonstrate a set of dynamic properties using the B method. In particular, we consider reachability, non-interference and absence properties. Also, we show that these properties permit a wide range of property patterns introduced by Dwyer to be expressed. An overview of a tool supporting these approaches is also provided.
ISSN:0934-5043
1433-299X
DOI:10.1007/s00165-014-0323-x