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

A formalization method of fault tolerant technique for transient faults

作　　者：朱丹丹 刘久富 陈柯 梁娟娟 

机构地区：[1]南航航空航天大学自动化学院,江苏南京210016

出　　处：《电子设计工程》2013年第5期20-23,共4页Electronic Design Engineering

基　　金：南京航空航天大学青年科学创新基金(NS2010069);国家自然科学基金(60674100)

摘　　要：软件发生瞬时故障时,可能会导致处理器状态改变,致使程序执行出现数据错误或者控制流错误。目前已有许多软件、硬件以及混合的解决方案,主要的方法是重复计算和检查副本的一致性。但是,生成正确的容错代码十分困难,而且几乎没有关于证明这些技术的正确性的研究。类型化汇编语言(TAL)是一种标准的程序安全性证明的方式。本文概述了一种面向瞬时故障的软硬结合的容错方法,以及对该方法的形式化方法,包括容错类型化汇编语言、类型系统和容错定理。形式化的目的是为了验证,只有通过验证的程序代码才是类型安全的。本文只简单介绍了程序的形式化方法。Whena transient fauhoccurs in software, it may cause the processor state changes. The program execution appears data error or control flow error. There are many software-based solutions, hardware-based solutions and hybrid solutions ,mainly using redundancy computingand checking the consistency of the copy method. But generating correct fault-tolerant code is very difficult, and almost none of these solutions provide rigorous proofs of their correctness. Typed assembly language （TAL） is a standardway proving program safety. This article has outlined a hybrid solution for transient faults and the formalization method of it, including fault-tolerant typed assembly language, type system and fault tolerant theorem. The purpose of formalization is to verify program code, and only after verification program code is type safe. We briefly introduce the programformalization method only.

关 键 词：瞬时故障 程序安全性 类型化汇编语言 类型系统 容错 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]