Show simple item record

dc.contributor.advisorD'Souza, Deepak
dc.contributor.authorDivakaran, Sumesh
dc.date.accessioned2018-06-21T17:12:01Z
dc.date.accessioned2018-07-31T04:39:17Z
dc.date.available2018-06-21T17:12:01Z
dc.date.available2018-07-31T04:39:17Z
dc.date.issued2018-06-21
dc.date.submitted2015
dc.identifier.urihttp://etd.iisc.ac.in/handle/2005/3744
dc.identifier.abstracthttp://etd.iisc.ac.in/static/etd/abstracts/4606/G26949-Abs.pdfen_US
dc.description.abstractThis 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.en_US
dc.language.isoen_USen_US
dc.relation.ispartofseriesG26949en_US
dc.subjectAbstract Data Typesen_US
dc.subjectData Structureen_US
dc.subjectData Abstractionen_US
dc.subjectFree RTOS-open-source Real-time Operating Systemen_US
dc.subjectRefinement (Computing)en_US
dc.subjectTheory of Refinementen_US
dc.subjectVirtual Collective Consiousness (VCC)en_US
dc.subjectModelling Languagesen_US
dc.subjectProgramming Languagesen_US
dc.subjectADT Transition Systemsen_US
dc.subjectFreeRTOSen_US
dc.subject.classificationComputer Scienceen_US
dc.titleA Refinement-Based Methodology for Verifying Abstract Data Type Implementationsen_US
dc.typeThesisen_US
dc.degree.namePhDen_US
dc.degree.levelDoctoralen_US
dc.degree.disciplineFaculty of Scienceen_US


Files in this item

This item appears in the following Collection(s)

Show simple item record