Publications

The purpose of this paper is to demonstrate how transformation can be used to derive a high integrity implementation of a train controller from an algorithmic specification. The paper begins with a general discussion of high consequence systems (e.g., software systems) and describes how rewrite-based transformation systems can be used in the development of such systems. The authors then discuss how such transformations can be used to derive a high assurance controller for the Bay Area Rapid Transit (BART) system from an algorithmic specification.

All systems, regardless of how carefully they have been constructed, suffer failures. This paper focuses on developing a formal understanding of failure with respect to system implementations. Furthermore, we would like the system design process to be able to leverage off of this understanding. It is important to deal with failures in a system context, rather than a priori limiting the solution to a particular technology, such as software alone. Our approach is limited to the class of systems that can be modeled by hybrid finite state machines (HFSMs) as described V.L. Winter. The purpose of this paper is to lay out a process, or framework, that can aid in identification and characterization of techniques for dealing with the different types of system threats. This framework leads naturally to a taxonomy of technologies and strategies for dealing with the various types of threats. In this process technologies are used to identify a priority list of technical capabilities for dealing with threats. The technologies are prioritized according to their analyzability and predictability. Strategies are then used to identify specific implementations that are best suited to dealing with the threat.

In this paper, the authors present a digital system requirements specification method that has demonstrated a potential for improving the completeness of requirements while reducing ambiguity. It assists with making proper digital system design decisions, including the defense against specific digital system failures modes. It also helps define the technical rationale for all of the component and interface requirements. This approach is a procedural method that abstracts key features that are expanded in a partitioning that identifies and characterizes hazards and safety system function requirements. The key system features are subjected to a hierarchy that progressively defines their detailed characteristics and components. This process produces a set of requirements specifications for the system and all of its components. Based on application to nuclear power plants, the approach described here uses two ordered domains: plant safety followed by safety system integrity. Plant safety refers to those systems defined to meet the safety goals for the protection of the public. Safety system integrity refers to systems defined to ensure that the system can meet the safety goals. Within each domain, a systematic process is used to identify hazards and define the corresponding means of defense and mitigation. In both domains, the approach and structure are focused on the completeness of information and eliminating ambiguities in the generation of safety system requirements that will achieve the plant safety goals.