Publications

To date most validation techniques are highly biased towards calculations involving symbolic representations of problems. These calculations are either formal (in the case of consistency and completeness checks), or informal in the case of code inspections. The authors believe that an essential type of evidence of the correctness of the formalization process must be provided by (i.e., must originate from) human-based calculation. They further believe that human calculation can by significantly amplified by shifting from symbolic representations to graphical representations. This paper describes their preliminary efforts in realizing such a representational shift.

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.

A key step in the construction of high consequence software is its specification in a formal framework. In order to minimize the difficulty and potential for error, a specification should be expressed in a domain language supporting operators and structures that are intrinsic to the class of algorithms one wishes to specify. In this paper the authors describe a language that is suitable for the algorithmic specification of software controllers for a class of reactive systems of which the Bay Area Rapid Transit (BART) system is an instance. The authors then specify an abstract controller for a subset of BART using this language.

The purpose of this panel is to present different perspectives and opinions regarding the issues surrounding why software should or shouldn't be entrusted with critical (high consequence) functionality.

In this paper we present an approach that facilitates the validation of high consequence system requirements. This approach consists of automatically generating a graphical representation from an informal document. Our choice of a graphical notation is statecharts. We proceed in two steps: we first extract a hierarchical decomposition tree from a textual description, then we draw a graph that models the statechart in a hierarchical fashion. The resulting drawing is an effective requirements assessment tool that allows the end user to easily pinpoint inconsistencies and incompleteness.

HATS is a general purpose syntax derivation tree based transformation system in which transformation sequences are described in special purpose language. A powerful feature of this language is that unification is an explicit operation. By making unification explicit, an elegant framework arises in which to express complex application conditions which in turn enables refined control strategies to be realized. This paper gives an overview of HATS, focusing especially on the framework provided by the transformation language and its potential with respect to control and general purpose transformation.

This paper describes a modeling technique for single-agent reactive systems, that is influenced by the modeling paradigm of Parnas as well as by the synchronous paradigms of LUSTRE and ESTEREL. In this paradigm, single-agent reactive systems are modeled in a universe having a discrete clock. This discretization of time greatly reduces the temporal complexity of the model. He believes that the advantage of this reduction in temporal complexity is that the resulting model is in many ways better suited to automated software construction and analysis techniques (e.g., deductive synthesis, transformation, and verification) than models that are based on continuous representations of time.

Transformations that are based on syntax directed rewriting systems can have a significant impact on the construction of high assurance systems. However, in order for a transformational approach to be useful to a particular problem domain, a (general) transformation system must be adapted to the notation of that particular domain. A transformation system that can be easily adapted to various domain notations has the potential of having a wide range of applicability. In this paper we dissus why transforrmtion is attractive horn a high assurance perspective, as well as some issues surrounding automated transformation within specific problem domains. We then give an overview of a language independent High Assurance Transformation System (HATS) that is being developed at Sandia National Laboratories.

When designing a high consequence system, considerable care should be taken to ensure that the system can not easily be placed into a high consequence failure state. A formal system design process should include a model that explicitly shows the complete state space of the system (including failure states) as well as those events (e.g., abnormal environmental conditions, component failures, etc.) that can cause a system to enter a failure state. In this paper the authors present such a model and formally develop a notion of risk-based refinement with respect to the model.

The software construction process consists of a mixture of informal and formal steps. By their very nature, informal steps cannot be formally verified. Empirical evidence suggests that a majority of software errors originate in the informal steps of the software development process. For this reason, when constructing high assurance software, it is essential that a significant effort be made to increase one`s confidence (i.e., to validate) that the informal steps have been made correctly. Visualization and animation can be used to provide an `intuitive proof` that the informal steps in the software construction process are correct. In addition, the formal portion of software construction often permits/demands artistic (informal) decisions to be made (e.g., design decisions). Such decisions often have unexpected/unforeseen consequences that are only discovered later in the development process. Visualization and animation techniques can be brought to bear on this aspect of the software construction process by providing a better intuitive understanding of the impact of the informal decisions that are made in program development. This increases the likelihood that undesirable decisions can be avoided or at least detected earlier in the development process.

The construction of a high-assurance system requires some evidence, ideally a proof, that the system as implemented will behave as required. Direct proofs of implementations do not scale up well as systems become more complex and therefore are of limited value. In recent years, refinement-based approaches have been investigated as a means to manage the complexity inherent in the verification process. In a refinement-based approach, a high-level specification is converted into an implementation through a number of refinement steps. The hope is that the proofs of the individual refinement steps will be easier than a direct proof of the implementation. However, if stepwise refinement is performed manually, the number of steps is severely limited, implying that the size of each step is large. If refinement steps are large, then proofs of their correctness will not be much easier than a direct proof of the implementation. The authors describe an approach to refinement-based software development that is based on automatic application of refinements, expressed as program transformations. This automation has the desirable effect that the refinement steps can be extremely small and, thus, easy to prove correct. They give an overview of the TAMPR transformation system that the use for automated refinement. They then focus on some aspects of the semantic framework that they have been developing to enable proofs that TAMPR transformations are correctness preserving. With this framework, proofs of correctness for transformations can be obtained with the assistance of an automated reasoning system.

TAMPR is a fully automatic transformation system based on syntactic rewrites. Our approach in a correctness proof is to map the transformation into an axiomatized mathematical domain where formal (and automated) reasoning can be performed. This mapping is accomplished via an extended denotational semantic paradigm. In this approach, the abstract notion of a program state is distributed between an environment function and a store function. Such a distribution introduces properties that go beyond the abstract state that is being modeled. The reasoning framework needs to be aware of these properties in order to successfully complete a correctness proof. This paper discusses some of our experiences in proving the correctness of TAMPR transformations.