Record Details

A Refinement-Based Methodology for Verifying Abstract Data Type Implementations

Electronic Theses of Indian Institute of Science

View Archive Info
 
 
Field Value
 
Title A Refinement-Based Methodology for Verifying Abstract Data Type Implementations
 
Creator Divakaran, Sumesh
 
Subject Abstract Data Types
Data Structure
Data Abstraction
Free RTOS-open-source Real-time Operating System
Refinement (Computing)
Theory of Refinement
Virtual Collective Consiousness (VCC)
Modelling Languages
Programming Languages
ADT Transition Systems
FreeRTOS
Computer Science
 
Description This thesis is about techniques for proving the functional correctness of Abstract Data Type (ADT) implementations. We provide a framework for proving the functional correctness of imperative language implementations of ADTs, using a theory of refinement. We develop a theory of refinement to reason about both declarative and imperative language implementations of ADTs. Our theory facilitates compositional reasoning about complex implementations that may use several layers of sub-ADTs.
Based on our theory of refinement, we propose a methodology for proving the functional correctness of an existing imperative language implementation of an ADT. We propose a mechanizable translation from an abstract model in the Z language to an abstract implementation in VCC’s ghost language. Then we present a technique to carry out the refinement checks completely within the VCC tool.
We apply our proposed methodology to prove the functional correctness of the scheduling-related functionality of FreeRTOS, a popular open-source real-time operating system. We focused on the scheduler-related functionality, found major deviations from the intended behavior, and did a machine-checked proof of the correctness of the fixed code.
We also present an efficient way to phrase the refinement conditions in VCC, which considerably improves VCC’s performance. We evaluated this technique on a simplified version of FreeRTOS which we constructed for this verification exercise. Using our efficient approach, VCC always terminates and leads to a reduction of over 90% in the total time taken by a naive check, when evaluated on this case-study.
 
Contributor D'Souza, Deepak
 
Date 2018-06-21T17:12:01Z
2018-06-21T17:12:01Z
2018-06-21
2015
 
Type Thesis
 
Identifier http://etd.iisc.ernet.in/2005/3744
http://etd.iisc.ernet.in/abstracts/4606/G26949-Abs.pdf
 
Language en_US
 
Relation G26949