Toggle Main Menu Toggle Search

Open Access padlockePrints

Verifiable Fault-Tolerant Transformation of a Real-Time Legacy System

Lookup NU author(s): Daniel Owen, Dr Paul Ezhilchelvan

Downloads


Abstract

Transforming a non-fault-tolerant legacy system into a fault-tolerant one requires, among other things, a convincing proof or argument that the transformed system is functionally equivalent. In addition, one should be able to assess whether the new system is capable of meeting the timeliness guarantees of the original system, since the fault-tolerance support activities typically impose a performance overhead. This paper describes the approach and methods we have adopted to transform an industrial-strength real-time system specified in a lowlevel language called the real-time network specification language (RTN-SL).We have addressed two issues: (i) expressing the low-level design specification in a suitably abstract form that simplifies fault-tolerant transformations, and (ii) formulation of rules for incorporating known fault-tolerant techniques in a machineverifiable manner. The former is achieved by the use of a context-sensitive graph grammar and the verification of transformation by utilising the IFAD VDM-SL Toolbox. Our experience in applying these fault-tolerant transformation on an industrial-strength legacy system exposes a general problem encountered, merits of utilizing existing industrial tools, and the kinds of tools that need to be developed.


Publication metadata

Author(s): Owen DJ, Ezhilchelvan PD

Publication type: Report

Publication status: Published

Series Title: School of Computing Science Technical Report Series

Year: 2002

Pages: 22

Print publication date: 01/11/2002

Source Publication Date: November 2002

Report Number: 785

Institution: School of Computing Science, University of Newcastle upon Tyne

Place Published: Newcastle upon Tyne

URL: http://www.cs.ncl.ac.uk/publications/trs/papers/785.pdf


Share