一种面向瞬时故障的容错技术的形式化方法

软件发生瞬时故障时,可能会导致处理器状态改变,致使程序执行出现数据错误或者控制流错误。目前已有许多软件、硬件以及混合的解决方案,主要的方法是重复计算和检查副本的一致性。但是,生成正确的容错代码十分困难,而且几乎没有关于证明这些技术的正确性的研究。类型化汇编语言(TAL)是一种标准的程序安全性证明的方式。本文概述了一种面向瞬时故障的软硬结合的容错方法,以及对该方法的形式化方法,包括容错类型化汇编语言、类型系统和容错定理。形式化的目的是为了验证,只有通过验证的程序代码才是类型安全的。本文只简单介绍了程序的形式化方法。

一种构造代码安全性证明的方法

提出一种构造代码安全性证明的新方法.这种方法的基本思想是,在基础逻辑中定义辅助递归函数来帮助构造证明.这种构造方法在不增加系统信任计算基础的情况下可以极大地减轻构造证明的工作量,并且减小安全性证明的规模同时介绍了该方法在一个FPCC系统中的应用.在这个系统中使用该方法使得代码的安全性证明可以自动产生.全部工作的细节已在证明辅助工具Coq中得以实现.