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.