Verification of safety requirements for program code using data abstraction

Authors

  • Frank Stappers
  • Michel Reniers

DOI:

https://doi.org/10.14279/tuj.eceasst.23.311

Abstract

Large systems in modern development consist of many concurrent processes. To prove safety properties formal modelling techniques are needed. When source code is the only available documentation for deriving the system's behaviour, it is a difficult task to create a suitable model. Implementations of a system usually describe behaviour in too much detail for a formal verification. Therefore automated methods are needed that directly abstract from the implementation, but maintain enough information for a formal system analysis. This paper describes and illustrates a method by which systems with a high degree of parallelism can be verified. The method consists of creating an over-approximation of the behaviour by abstracting from the values of program variables. The derived model, consisting of interface calls between processes, is checked for various safety properties with the mCRL2 tool set.

Downloads

Published

2009-12-17

How to Cite

[1]
F. Stappers and M. Reniers, “Verification of safety requirements for program code using data abstraction”, eceasst, vol. 23, Dec. 2009.