目录
摘要 1
一. 引言 1
二. 安全核心的基本原理 3
三. 交通灯的安全规定 4
四. 交通灯安全设备的必要条件 6
五. 核心规格 8
六. 安全核心的分析 11
七. 执行和应用 13
八. 核心的应用 15
九. 讨  论 16
十. 结  论 17
十一. 鸣  谢 17

摘要
    实施安全的果仁的成功已经导致提议用果仁实施安全。本文通过交通灯控制的应用为安全果仁提出一特殊的可行性示范的建议。文章为交通灯控制从安全特性开始详细说明保持安全特性的一颗果仁。埃达里给出了果仁实施的草图并讨论了使用方法。本文所主出的贡献就是证实了果仁在时间、安全关键的应用方面的软件的一种可行性和合乎需要的技术。文章也说明了用什么样的正规方法帮助软件工程师开发和使用这样的软件。

一.引言
    软件被用于控制的应用的次数渐增是非常安全的，它意味着某些失败和所谓的安全故障，有不可接受的费用。例如，认为损害、环境损害和财政损失等等。计算机控制，安全纠正系统确实也可能失败。并且在这些系统里对软件技术的改进有强烈的兴趣。虽然多种技术已经被发展。这些技术仍受到很多的限制，比如，实现什么功能，而且需要增加为软件安全纠正的发展提供一些可靠的方法。在本文中，我们朝着考虑果仁应用的目标去工作，在享有在安全地区的成功时取得安全。本文最特殊的贡献是Rushby关于果仁观念的可行性示范。交通灯的控制被选来为示范应用。
    安全纯粹是一个系统特性，软件本身是安全也是不安全的。然而，象在安全纠错系统中的任何一部分，软件都需要有被认为有包含安全的系统作用的某种特性。这些特性可以断定表示软件必须与它的输入、输出和当前的状态保持关联。例如，一个电抗线圈的安全特性系统可能被定义为如果电抗线圈过热则它就停止操作。为了使电抗线圈能够安全运行，用软件控制的电抗线圈必须使断定得到满意。电抗线圈传感器超出一临界值后电抗线圈就在一定时间间隔内发出一停止运行的命令。在这个例子中，安全设施被定义于与电抗线圈的毁坏有关，相关的安全设备。软件断定为调速控制器与传感器从输入到输出适时相关联。