A Compositional Renement Technique for Verifying
Abstract Data Type Implementations
Sumesh Divakaran,
Deepak D'Souza
Anirudh Kushwah
, Prahladavaradan
Sampath
, Nigamanth Sridhar
, and Jim Woodcock
We propose a methodology for verifying the functional
correctness of an imperative language implementation of a system that
can be modelled as Abstract Data Type (ADT). The
methodology is based on a novel theory of refinement that allows us to
treat both declarative and imperative implementations of ADT's on a
common ground. The theory facilitates compositional reasoning about
complex implementations that may use several layers of sub-ADT's.
We apply this technique to carry out a full machine-checked proof of
functional correctness of the scheduler-related functionality of
FreeRTOS, a popular open-source embedded operating system.
pdf