Deriving Specifications for Systems That Are Connected to the Physical World
Deriving Specifications for Systems That Are Connected to the Physical World
复制标题
导出连接到物理世界的系统的规范
DOI：
--
复制
发表时间：
2007
期刊：
影响因子：
--
通讯作者：
M. A. Jackson
中科院分区：
文献类型：
--
作者：
Cliff B. Jones;I. Hayes;M. A. Jackson
从形式规格说明开发程序的方法已经有了很好的理解。这样的方法不仅提供了一个精确的检查，从他们的规范的某些种类的偏差是不存在的实现，但他们也可以提高开发过程的生产力，通过仔细使用抽象层和细化设计。然而，这些方法都以一个规范为前提，从这个规范开始开始开发。对于完全用机器内的符号值描述的任务，发明一个规范并不困难，但对程序与外部物理世界交互的系统的需求越来越大。在这里，确定“硅封装”的规格的任务可能比开发本身更具挑战性。这些应用包括控制程序，这些程序试图通过致动器改变物理世界，并通过传感器测量外部（硅封装）世界的事物。此外，大多数这类系统必须容忍计算机外部物理组件的故障：这样就更难保证规范是适当的。本文提供了一种系统的方法来推导控制程序的规格。此外，我们的方法导致记录关于物理世界的假设。我们还讨论了分离的检测和管理故障的系统操作中没有故障。这一讨论与“正常”和“激进”设计之间的区别有关。
Well understood methods exist for developing programs from formal specifications. Not only do such methods offer a precise check that certain sorts of deviations from their specifications are absent from implementations but they can also increase the productivity of the development process by careful use of layers of abstraction and refinement in design. These methods, however, presuppose a specification from which to begin the development. For tasks that are fully described in terms of the symbolic values within a machine, inventing a specification is not difficult but there is an increasing demand for systems in which programs interact with an external physical world. Here, the task of fixing the specification for the "silicon package" can be more challenging than the development itself. Such applications include control programs that attempt to bring about changes in the physical world via actuators and measure things in that external (to the silicon package) world via sensors. Furthermore, most systems of this class must tolerate failures in the physical components outside the computer: it then becomes even harder to achieve confidence that the specification is appropriate. This paper offers a systematic way to derive the specification of a control program. Furthermore, our approach leads to recording assumptions about the physical world. We also discuss separating the detection and management of faults from system operation in the absence of faults. This discussion is linked to the distinction between "normal" and "radical" design.