Refinement Laws for Verifying Library Subroutine Adaptation

C. Fidge; P. Robinson; S. Dunne

doi:10.1109/ASWEC.2005.40

Refinement Laws for Verifying Library Subroutine Adaptation

C. Fidge, P. Robinson, S. Dunne

School of Social Sciences, Humanities & Law

Research output: Contribution to conference › Paper › peer-review

144 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 language	English
Pages	224-232
DOIs	https://doi.org/10.1109/ASWEC.2005.40
Publication status	Published - 1 Apr 2005
Event	The Australian Software Engineering Conference 2005 - Brisbane, Australia Duration: 29 Mar 2005 → 1 Apr 2005

Conference

Conference	The Australian Software Engineering Conference 2005
Abbreviated title	ASWEC 2005
Country/Territory	Australia
City	Brisbane
Period	29/03/05 → 1/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]

Access to Document

10.1109/ASWEC.2005.40

Accepted manuscriptAccepted author manuscript, 120 KBLicence: CC BY-NC-ND

http://ieeexplore.ieee.org/document/1402017/

Cite this

@conference{495b2402f11e460b8899e6808577c334,

title = "Refinement Laws for Verifying Library Subroutine Adaptation",

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.",

author = "C. Fidge and P. Robinson and S. Dunne",

note = " Author can archive publisher's version/PDF. For full details see http://www.sherpa.ac.uk/romeo/ [Accessed 30/03/2010]; The Australian Software Engineering Conference 2005, ASWEC 2005 ; Conference date: 29-03-2005 Through 01-04-2005",

year = "2005",

month = apr,

day = "1",

doi = "10.1109/ASWEC.2005.40",

language = "English",

pages = "224--232",

}

TY - CONF

T1 - Refinement Laws for Verifying Library Subroutine Adaptation

AU - Fidge, C.

AU - Robinson, P.

AU - Dunne, S.

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

PY - 2005/4/1

Y1 - 2005/4/1

N2 - 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.

AB - 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.

U2 - 10.1109/ASWEC.2005.40

DO - 10.1109/ASWEC.2005.40

M3 - Paper

SP - 224

EP - 232

T2 - The Australian Software Engineering Conference 2005

Y2 - 29 March 2005 through 1 April 2005

ER -

Refinement Laws for Verifying Library Subroutine Adaptation

Abstract

Conference

Bibliographical note

Access to Document

Fingerprint

Cite this