A Compositional Re nement 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.