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

摘要

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 low level language called the real-time network specification language (RTN-SL). We have addressed two issues: (1) expressing the low-level design specification in a suitably abstract form that simplifies fault-tolerant transformations; and (2) formulation of rules for incorporating known fault-tolerant techniques in a machine verifiable manner. The former is achieved by the use of a context-sensitive graph grammar and the verification of transformation by utilizing the IFAD VDM-SL Toolbox. Our experience in applying these fault-tolerant transformations 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.