A framework for the development of a family of trustworthy systems

软件在我们的社会中扮演着主导的角色，通常不仅指导我们，而且迫使我们对特定的行为做出反应，从而带来回报和风险。智能医疗设备和在线医疗保健系统的软件就是最好的例子。它们带来了巨大的好处，但当它们发生故障或失效时，病人就处于危险之中。安全性、安全性和隐私性是决定此类应用程序信任的属性。在网上金融和电子商务领域，软件只有在安全、提供及时服务、履行义务和保护隐私的情况下才能被信任。在交通运输领域，飞机上安装了自动驾驶仪，自动驾驶仪一旦初始化，就会剥夺飞行员的控制，给飞行带来愉悦，偶尔也会发生严重的事故。安全性、安全性、可靠性和可用性都是确保对此类软件信任的基本属性。在能源领域，大型电网和核电站必须得到安全保护和保护。没有安全的直接证据，监视和管理这些系统的安全软件是不可信的。这些例子说明了不同行业风险的类型和严重程度。必须明确与软件交互的风险，以便客户在使用系统之前决定他们对系统的信任程度。特别是，对于隐私和安全关键领域的软件，可靠性论证必须采用直接证据的形式，可以由第三方（不需要是专家）审核。这个参数应该是一个表达式，它包括全局上下文信息、软件的关键属性、对其嵌入的假设、环境约束，以及满足指定属性的直接证据。本研究的目的是调查理论、方法和框架，以严格开发一系列可信系统。开发框架应该足够通用，以便在任何指定了合同的领域中开发可信的系统。正式构建直接证据链并在系统开发的所有阶段验证它是一项必要的活动。

Software plays a predominant role in our society, often not just guiding us but forcing us to respond to specific actions, bringing thus both rewards and risks. Software for smart medical devices and on-line health care systems are prime examples. They bring enormous benefits, but when they malfunction or fail the patients are in peril. Safety, security, and privacy are the attributes that determine trust in such applications. In the sector of on-line finance and E-commerce, software can be trusted only if it is secure, provides timely service, enforces obligations, and affords privacy. In transportation domain, aircrafts have autopilots installed in them, which once initialized will take away the control of a pilot, resulting in cruising pleasure and occasionally resulting in a severe accident. Safety, security, reliability, and availability are all essential attributes to ensure trust in such software. In the energy sector, large power grids and nuclear power plants should be safe-guarded and protected without fail. Without a direct evidence of safety and security software that monitors and manages these systems cannot be trusted. These examples illustrate the types and severity of risks that vary from one sector to another sector. The risk in interacting with software must be made explicit in order that clients may decide how well they want to trust the system before using it. In particular, for software in privacy and safety-critical domains the dependability argument must be in the form of direct evidence that can be audited by a third party who need not be an expert. This argument should be an expression that includes the global context information, the critical properties of the software, and assumptions on its embedding, its environmental constraints, and direct evidence that the specified properties are satisfied. The goal of this research is the investigation of theory, methods, and a framework for a rigorous development of a family of trustworthy systems. The development framework should be general enough to enable the development of a trustworthy system in any domain for which a contract is specified. Formally constructing a chain of direct evidence and validating it at all stages of system development is an essential activity.