The Dependable Intrusion Tolerance (DIT) architecture is a flexible, adaptive, and intrusion-tolerant server design. We briefly discuss its prototype implementation and validation, and demonstrate how it resists sample attacks.

SDTP is an architecture for secure distributed transaction processing. It is based upon X/Open's standard architecture for distributed transaction processing. In addition to the ACID (atomicity, consistency, isolation, and durability) properties provided by X/Open's architecture, SDTP guarantees that the Simple Security Property and the *-Property of the Bell-LaPadula model are satisfied. We have built a reference implementation of SDTP, formally proven the security properties of the implementation using novel verification techniques, and constructed two prototype applications of the architecture. The first application is a law enforcement tracking system, inspired by the FBI's Field Office Information Management System. The second application is an intrusion detection correlation system.

A sound theory of real-time scheduling is necessary to support the engineering of real-time software applications. Developing scheduling results using formal methods helps provide the high level of assurance required in safety-critical domains. We propose a formalization methodology relying on state-machine models and on a library of commonly applicable properties. A case study has shown that rigorous and a detailed verification of nontrivial scheduling results can be performed within reasonable time limits, using modern theorem-proving tools such as PVS. It is still necessary to develop and extend such verification efforts to the increasingly complex scheduling algorithms that may one day be used in safety-critical applications. Other aspects relevant to the avionics domain remain insufficiently explored by the formal methods community. For example, little has been done in the analysis of distributed real-time systems, where difficult problems mixing communication, processing, fault tolerance must be addressed. Formal methods are especially valuable in such complex settings, where informal proofs guided by intuition are insufficient and where other validation approaches such as testing are incomplete. Formal methods should become an essential tool for validating the most critical aspects of real-time systems, such as the partitioning mechanisms required for fault isolation in integrated avionics. Real-time scheduling problems are an ideal application area for formal methods since they are subtle and complex, must be certified to the highest degrees of assurance for supporting critical applications, and thus require very precise, detailed, and rigorous verification.

The objective of this tutorial is to introduce current and emerging standards that address computer system and software safety. We consider relevant available standards and identify their strengths and weaknesses, we explore how to evaluate standards and we consider their application in practice. We address in depth IEC 61508 and Def Stan 00-56, two important standards. In addition, we will discuss current safety standards activity within the IEEE Software Engineering Standards Committee and we will touch upon the thorny issue of introducing standards into an organization. The tutorial will be practical and will address the application - not just the theory of safety standards. The tutorial is aimed at managers, project managers, safety engineers and software engineers with system or safety responsibility during the lifecycle of safety critical systems.

We describe a software-testing standardization proposal that is currently under consideration by the UK Ministry of Defense (MOD) Procurement Executive. The need for the proposal was borne out of the recognition that current MOD procurement policy does not deal adequately with software testing requirements, thus hampering both MOD managers and MOD contractors. Here we propose a testing standardization framework to cover all aspects and phases of software testing. Wherever possible, the framework makes use of established, internationally agreed standards in line with MOD standardization policy. Since integration testing is not adequately dealt with by existing standards, we put forward an outline proposal for dealing with the integration phase.

This paper describes the process of implementing an architecture for secure distributed transaction processing, the process of verifying that it has the desired security properties, and the implementation that resulted. The implementation and verification processes provided us with valuable experience relevant to answering several questions posed by our research on transformational development of architectures. To what extent can implementation-level architectural descriptions be derived from abstract description via application of transformations that preserve a broad class of properties, which includes satisfaction of various access control policies? To what extent can a formal derivation of a non-secure implementation-level distributed transaction processing architecture be reused in derivation of a secure architecture? Are the transformation verification techniques that we have developed sufficient for verifying a collection of transformations adequate for implementing complex secure architecture? Do our architecture hierarchies effectively fill the gap between abstract, intellectually manageable models of a complex architecture and the actual implementation? Exploring the answers to these questions resulted in a reference implementation of an architecture for secure distributed transaction processing, and an independently interesting demonstration instance of the reference implementation.

This article is concerned with systems integration and its impact on software intensive projects. It contains a review and a taxonomy of integration concepts as applied to software intensive systems. We identify pertinent technical integration issues and review and classify integration models, strategies, mechanisms and architectures. We argue that integration is part of the design activity and propose existing best integration practice for project management and engineering of large software intensive systems.

This paper describes the process of implementing an architecture for secure distributed transaction processing, the process of verifying that it has the desired security properties, and the implementation that resulted. The implementation and verification processes provided us with valuable experience relevant to answering several questions posed by our research on transformational development of architectures. To what extent can implementation-level architectural descriptions be derived from abstract description via application of transformations that preserve a broad class of properties, which includes satisfaction of various access control policies? To what extent can a formal derivation of a non-secure implementation-level distributed transaction processing architecture be reused in derivation of a secure architecture? Are the transformation verification techniques that we have developed sufficient for verifying a collection of transformations adequate for implementing complex secure architecture? Do our architecture hierarchies effectively fill the gap between abstract, intellectually manageable models of a complex architecture and the actual implementation? Exploring the answers to these questions resulted in a reference implementation of an architecture for secure distributed transaction processing, and an independently interesting demonstration instance of the reference implementation.

The application of formal methods offers an opportunity to enhance the integrity of software standards through several distinct roles. During the development of standards, the final representation of the standard, and testing of implementations claiming conformance to the standard, formal methods can be applied to achieve more precise and testable standards.

These paper presents an approach for integrating UML with an ADL. The integration would encompass the advantages of both languages. It would give formal semantics to UML constructs and thus would provide UML with a theoretical foundation for architecture modeling. Furthermore, the integration would provide benefits for both ADL and UML users: it will enable ADL users to utilize general-purpose UML tools, and will enable UML users to utilize ADL validation capabilities. The result would be a rigorous software development process that is currently lacking.

Software for safety critical systems must deal with the hazards identified by safety analysis. This paper investigates, how the results of one safety analysis technique, fault trees, are interpreted as software safety requirements to be used in the program design process. We propose that fault tree analysis and program development use the same system model. This model is formalized in a real-time, interval logic, based on a conventional dynamic systems model with state evolving over time. Fault trees are interpreted as temporal formulas, and it is shown how such formulas can be used for deriving safety requirements for software components.

We report on a formal requirements analysis experiment involving an avionics control system. We describe a method for specifying and verifying real-time systems with PVS. The experiment involves the formalization of the functional and safety requirements of the avionics system as well as its multilevel verification. First level verification demonstrates the consistency of the specifications whilst the second level shows that certain system safety properties are satisfied by the specification. We critically analyze methodological issues of large scale verification and propose some practical ways of structuring Verification activities for optimizing the benefits.

By describing several industrial-scale applications of formal methods, we demonstrate that formal methods for software development and safety analysis are being increasingly adopted in the safety-critical systems sector. The benefits and limitations of formal methods are described, and the problems in developing software for safety-critical systems are analyzed.

Formal methods are increasingly used for system development and their potential advantages for dependability assurance have been recognized. However, there has so far been no hard evidence to either support or refute the efficacy of formal methods in this respect. This paper discusses how the dependability of systems can be affected by the tree of formal methods in two respects. First, how and why formal methods can help ensure the dependability of systems, and second what uncertainties can affect their effectiveness in achieving dependability. Issues related to the assessment of formal methods such as assessment criteria an assessment model and the establishment of evaluation experiments are discussed.<>

Standards concerned with the development of safety-critical systems, and the software in such systems in particular, abound today as the software crisis increasingly affects the world of embedded computer-based systems. The use of formal methods is often advocated as a way of increasing confidence in such systems. This paper examines the industrial use of these techniques, the recommendations concerning formal methods in a number of current and draft standards, and comments on the applicability and problems of using formal methods for the development of safety-critical systems on an industrial scale. Some possible future directions are suggested.

We elaborate on an integrated hardware specification, simulation and verification environment. We expand upon two major components of this environment, namely the hardware description language FUNNEL and the 2OBJ theorem proving system. We motivate the design of these and demonstrate their use through a simple specification and verification example.

We present the approach to development of provablycorrect safety critical software emerging through the case studies activity of the ProCoS project. We envisage the development of a safety critical system through six major stages; Control objectives and safety criteria will be be captured in requirements capture languages (RLs) (formal mathematical models of the problem domain) supporting the notions of durations, events and states. A specification expressed in a specification language(SL) satisfying the requirements is derived via requirements transformations.The specification is refined and finally transformed into a programming language (PL) program which is refined and mapped by a verified PL compiler onto the instruction set of an abstract hardware machine (AHM) and is executed via an ABM computer supported by a trusted kernel operating system. The aim of this paper is to show how the coordinated development activities fit together once an informal specification of the desired system behaviour has been delivered.