Verified Emulation of Legacy Mission Computer Systems

对于军用飞机和其他关键应用的长寿命计算机控制系统来说，处理器陈旧是一个严重的维护问题。一个有希望的解决方案是在原始的“遗留”软件和替换处理器之间插入一个仿真程序。不幸的是，没有技术可以准确地验证这个过程是否保留了原始系统的功能和定时行为。一个特别的挑战是处理器仿真涉及到用不同编程语言编写的遗留代码和新的子例程。该项目将通过设计基于程序细化理论的多语言建模和推理形式来验证安全和关键任务仿真系统。

Processor obsolescence is a serious maintenance problem for long-lived computer control systems in military aircraft and other critical applications. A promising solution is to interpose an emulator program between the original "legacy" software and a replacement processor. Unfortunately, no techniques exist for accurately verifying that this procedure preserves the original system's functional and timing behaviour. A particular challenge is that processor emulations involve both legacy code and new subroutines, written in different programming languages. This project will enable verification of safety and mission-critical emulated systems by devising a multilingual modelling and reasoning formalism, based on program refinement theory.