Verifiable Fault-Tolerant Transformation of a Real-Time Legacy System
DJ Owen, PD Ezhilchelvan · 2002
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.