Refinement Laws for Verifying Library Subroutine Adaptation

C. Fidge, P. Robinson, S. Dunne

Research output: Contribution to conferencePaper

125 Downloads (Pure)

Abstract

In Component-Based Software Engineering programs are constructed from pre-defined software library modules. However, if the library's subroutines do not exactly match the programmer's requirements, the subroutines' code must be adapted accordingly. For this process to be acceptable in safety or mission-critical applications, where all code must be proven correct, it must be possible to verify the correctness of the adaptations themselves. In this paper we show how refinement theory can be used to model typical adaptation steps and to define the conditions that must be proven to verify that a library subroutine has been adapted correctly.
Original languageEnglish
Pages224-232
DOIs
Publication statusPublished - 1 Apr 2005
EventThe Australian Software Engineering Conference 2005 - Brisbane, Australia
Duration: 29 Mar 20051 Apr 2005

Conference

ConferenceThe Australian Software Engineering Conference 2005
Abbreviated titleASWEC 2005
CountryAustralia
CityBrisbane
Period29/03/051/04/05

Bibliographical note

Author can archive publisher's version/PDF. For full details see http://www.sherpa.ac.uk/romeo/ [Accessed 30/03/2010]

Fingerprint Dive into the research topics of 'Refinement Laws for Verifying Library Subroutine Adaptation'. Together they form a unique fingerprint.

  • Cite this

    Fidge, C., Robinson, P., & Dunne, S. (2005). Refinement Laws for Verifying Library Subroutine Adaptation. 224-232. Paper presented at The Australian Software Engineering Conference 2005, Brisbane, Australia. https://doi.org/10.1109/ASWEC.2005.40