Facilitating the Maintenance of Safety-Critical Systems

As software is increasingly used to control safety-critical systems, correctness becomes paramount. Formal methods in software development provide many benefits in the forward engineering aspect of software development. Reverse Engineering is the process of constructing a high level representation of a system from existing lower level instantiations of that system. Reverse engineering of program code into formal specifications facilitates the utilization of the benefits of formal methods in projects where formal methods may not have previously been used, thus facilitating the maintenance of safety-critical systems. Keywords: formal methods, formal specifications, reverse engineering, maintenance, safetycritical systems 1 Introduction As software is increasingly used to control safety-critical systems, correctness becomes paramount. The demand for software correctness becomes more evident when accidents, sometimes fatal, are due to software errors. For example, recently it was repor..