NRL Resources
Publications
| 2009 | 2008 | 2007 | 2006 | 2005 | 2004 | 2003 | 2002 | 2001 | 2000 | 1999 | 1998 | 1997 | 1996 | 1995 | 1994 | 1993 |
View Abstract
This paper describes how formal methods were used to produce evidence in a certification, based on the Common Criteria, of a security-critical software system. The evidence included a top level specification (TLS) of the security-relevant software behavior, a formal statement of the required security properties, proofs that the specification satisfied the properties, and a demonstration that the source code, which had been annotated with preconditions and postconditions, was a refinement of the TLS. The paper also describes those aspects of our approach which were most effective and research that could significantly increase the effectiveness of formal methods in software certification.
View Abstract
It is widely agreed that building correct fault-tolerant systems is very difficult. To address this problem, this paper introduces a new model-based approach for developing masking fault-tolerant systems. As in component-based software development, two (or more) component specifications are developed, one implementing the required normal behavior and the other(s) the required fault-handling behavior. The specification of the required normal behavior is verified to satisfy system properties, whereas each specification of the required faulthandling behavior is shown to satisfy both system properties, typically weakened, and fault-tolerance properties, both of which can then be inferred of the composed fault-tolerant system. The paper presents the formal foundations of our approach, including a new notion of partial refinement and two compositional proof rules. To demonstrate and validate the approach, the paper applies it to a real-world avionics example.
View Abstract
Although it is most often applied to finite state models, in recent years, symbolic model checking has been extended to infinite state models using symbolic representations that encode infinite sets. This paper investigates the application of an infinite state symbolic model checker called Action Language Verifier (ALV) to formal requirements specifications of safety-critical systems represented in the SCR (Software Cost Reduction) tabular notation. After reviewing the SCR method and tools, the Action Language for representing state machine models, and the ALV infinite state model checker, the paper presents experimental results of formally analyzing two SCR specifications using ALV. The application of ALV to verify or falsify (by generating counterexample behaviors) the state and transition invariants of SCR specifications and to check Disjointness and Coverage properties is described. The results of formal analysis with ALV are then compared with the results of formal analysis using techniques that have been integrated into the SCR toolset. Based on the experimental results, strengths and weaknesses of infinite state model checking with respect to other formal analysis approaches such as explicit and finite state model checking and theorem proving are discussed.
View Abstract
A major problem in verifying the security of code is that the code's large size makes it much too costly to verify in its entirety. This article describes a novel and practical approach to verifying the security of code which substantially reduces the cost of verification. In this approach, a compact security model containing only information needed to reason about the security properties of interest is constructed, and the security properties are represented formally in terms of the model. To reduce the cost of verification, the code to be verified is partitioned into three categories: Only the first category, less than 10% of the code in our application, requires formal verification; the proof of the other two categories is relatively trivial. Our approach was developed to support a Common Criteria evaluation of the separation kernel of an embedded software system. This article describes 1) our techniques and theory for verifying the kernel code and 2) the artifacts produced: a Top Level Specification (TLS), a formal statement of the security property,a mechanized proof that the TLS satisfies the property, the partitioning of the code, and a demonstration that the code conforms to the TLS. The article also presents the formal basis for the argument that the kernel code conforms to the TLS and consequently satisfies the security property.
View Abstract
Based on our recent experience in four projects, each focused on either security-critical or safety-critical software, this paper evaluates several notions, widely held by RE researchers, for their utility in practical software development. It describes four notions which in our view work in practice and five others which do not.
View Abstract
This paper describes the specification, validation and verification of system and software requirements using the SCR tabular method and tools. An example is presented to illustrate the SCR tabular notation, and an overview of each of the ten tools in the SCR toolset is presented.
View Abstract
Recently, a formal requirements method called SCR (Software Cost Reduction) was used to specify software requirements of mission-critical components of three NASA systems. The components included a fault protection engine, which determines how a spacecraft should respond to a detected fault; a fault detection, isolation and recovery component, which, in response to an undesirable event, outputs a failure notification and raises one or more alarms; and a display system, which allows a space crew to monitor and control on-orbit scientific experiments. This paper demonstrates how significant and complex requirements of one of the components can be translated into an SCR specification and describes the errors detected when the authors formulated the requirements in SCR. It also discusses lessons learned in using formal methods to document the software requirements of the three components. Based on the authors' experiences, the paper presents several recommendations for improving the quality of requirements specifications of safety-critical aerospace software.
View Abstract
A general purpose theorem prover can be thought of as an extremely flexible modeling environment in which one can define and analyze almost any kind of model. A disadvantage to the full flexibility of a general purpose theorem prover is the lack of any guidance on how to construct a model and how then to apply the theorem prover to analyzing the model. In the general environment supplied by the prover, much time can be consumed in deciding how to specify a model and in interacting with and understanding feedback from the prover. However, specification templates, together with proof strategies whose design follows certain principles, can be used in many general purpose provers to create specialized modeling environments that address these difficulties. A specialized modeling environment created in this way can be further extended and/or further specialized in a straightforward way by drawing on the underlying theorem prover for additional capabilities. Moreover, a specialized modeling environment derived from a general purpose theorem prover provides a means of integrating powerful theorem proving capabilities into existing software development environments by way of appropriate translation schemes. This paper uses TAME (Timed Automata Modeling Environment) to illustrate the creation, extension, and specialization of a modeling environment based on PVS, and its integration into several software development environments.
View Abstract
Timed I/O Automata (TIOA) is a mathematical framework for modeling and verification of distributed systems that involve discrete and continuous dynamics. TIOA can be used for example, to model a real-time software component controlling a physical process. The TIOA model is sufficiently general to subsume other models in use for timed systems. The TIOA toolkit, currently under development, is aimed at supporting system development based on TIOA specifications. The TIOA toolkit is an extension of the IOA toolkit, which provides a specification simulator, a code generator, and both model checking and theorem proving support for analyzing specifications. This paper focuses on modeling of timed systems with TIOA and the TAME-based theorem proving support provided in the toolkit for proving system properties, including timing properties. Several examples are provided by way of illustration.
View Abstract
Using a theorem prover to establish that a body of code correctly implements an algorithm is a task seldom undertaken because the effort required tends to be prohibitive. Direct reasoning about code in a particular programming language requires that some version of the language's semantics---e.g., axiomatic, operational, denotational---be used to determine the program correctness assertions to establish with the theorem prover. Any scheme for generating correctness assertions will be language-specific, and for languages with complex constructs, can be complex to implement and use. Direct reasoning about algorithms using a theorem prover can be not just difficult, but impossible, if the algorithms are (as is typical) specified using informal pseudocode. This paper outlines a scheme that falls short of full program verification yet provides high confidence in the correctness of an algorithm's implementation. The scheme uses formal pseudocode specifications, in a restricted language of "while" programs with (possibly recursive) procedure calls, to bridge from algorithm specifications to implementations in code. Each block of formal pseudocode is verified in the theorem prover PVS by translating it into a state machine model and proving a set of state invariants. High confidence in implementation correctness is achieved by combining verification of the pseudocode with traceability arguments relating the algorithm specification to the pseudocode representation and the pseudocode representation to the actual code.
View Abstract
This paper investigates the application of infinite state model checking to the formal analysis of requirements specifications in the SCR (Software Cost Reduction) tabular notation using Action Language Verifier (ALV). After reviewing the SCR method and tools and the Action Language, experimental results are presented of formally analyzing two SCR specifications using ALV. The application of ALV to verify or falsify (by generating counterexamples) the state and transition invariants of SCR specifications and to check Disjointness and Coverage properties is described. ALV is compared with the verification techniques that have been integrated into the SCR toolset.
View Abstract
Although many algorithms, hardware designs, and security protocols have been formally verified, formal verification of the security of software is still rare. This is due in large part to the large size of software, which results in huge costs for verification. This paper describes a novel and practical approach to formally establishing the security of code. The approach begins with a well-defined set of security properties and, based on the properties, constructs a compact security model containing only information needed to reason about the properties. Our approach was formulated to provide evidence for a Common Criteria evaluation of an embedded software system which uses a separation kernel to enforce data separation. The paper describes 1) our approach to verifying the kernel code and 2) the artifacts used in the evaluation: a Top Level Specification (TLS) of the kernel behavior, a formal definition of data separation, a mechanized proof that the TLS enforces data separation, code annotated with pre- and postconditions and partitioned into three categories, and a formal demonstration that each category of code enforces data separation. Also presented is the formal argument that the code satisfies the TLS.
View Abstract
A promising trend in software development is the increasing adoption of model-driven design. In this approach, a developer first constructs an abstract model of the required program behavior in a language, such as Statecharts or Stateflow, and then uses a code generator to automatically transform the model into an executable program. This approach has many advantages---typically, a model is not only more concise than code and hence more understandable, it is also more amenable to mechanized analysis. Moreover, automatic generation of code from a model usually produces code with fewer errors than hand-crafted code.
One serious problem, however, is that a code generator may produce inefficient code. To address this problem, this paper describes a method for generating efficient code from SCR (Software Cost Reduction) specifications. While the SCR tabular notation and tools have been used successfully to specify, simulate, and verify numerous embedded systems, until now SCR has lacked an automated method for generating optimized code. This paper describes an efficient method for automatic code generation from SCR specifications, together with an implementation and an experimental evaluation. The method first synthesizes an execution-flow graph from the specification, then applies three optimizations to the graph, namely, input slicing, simplification, and output slicing, and then automatically generates code from the optimized graph. Experiments on seven benchmarks demonstrate that the method produces significant performance improvements in code generated from large spec
View Abstract
In presenting specifications and specification properties to a theorem prover, there is a tension between convenience for the user and convenience for the theorem prover. A choice of specification formulation that is most natural to a user may not be the ideal formulation for reasoning about that specification in a theorem prover. However, when the theorem prover is being integrated into a system development framework, a desirable goal of the integration is to make use of the theorem prover as easy as possible for the user. In such a context, it is possible to have the best of both worlds: specifications that are natural for a system developer to write in the language of the development framework, and representations of these specifications that are well matched to the reasoning techniques provided in the prover. In a tactic-based prover, these reasoning techniques include the use of tactics (or strategies) that can rely on certain structural elements in the theorem prover's representation of specifications. This paper illustrates how translation techniques used in integrating PVS into the TIOA (Timed Input/Output Automata) system development framework produce PVS specifications structured to support development of PVS strategies that implement reasoning steps appropriate for proving TIOA specification properties.
View Abstract
While human effort is critical to creating requirements specifications and human inspection can detect many specification errors, software tools find errors inspections miss and also find certain classes of errors more cheaply. This paper describes a set of tools for constructing and analyzing requirements specifications in the SCR (Software Cost Reduction) tabular notation. The tools include a specification editor, a consistency checker, a simulator, and tools for verifying application properties - including a model checker, a verifier, a property checker based on decision procedures, and an invariant generator. This paper also describes the practical systems to which the tools are being applied as well as some new tools recently added to the toolset - e.g., a tool that constructs a sound and complete abstraction from a property and a specification. To illustrate the tools, the paper describes their use in developing a requirements specification for an automobile cruise control system.
View Abstract
This extended abstract describes a general technique for organizing an automaton model of a system (or protocol) that is useful in the context of theorem proving, which we call the reference variable method. In this technique, a (usually complex) reference variable is used to capture the state. In cases when reasoning about the reference variable directly is complicated, auxiliary, shadow variables with provable relationships to the reference variable are used in formalizing properties of the automaton. The shadow variables are updated simultaneously with the reference variable when state transitions occur, and invariants are used to establish the relationships maintained. Proofs of properties relating shadow variables can often be done in an abstraction that omits the reference variable. This technique produces a natural specification in which the connection of the system model to the actual system is clear, and can be useful even when shadow variables are not used. Particularly when shadow variables are used, the technique provides the advantage that different abstractions can be related easily to ensure that they are abstractions of the same system. To illustrate the potential usefulness of the technique, we describe how we applied it in three examples.
View Abstract
UDDI is not suitable for handling semantic markups for Web services due to its flat data model and limited search capabilities. In this paper, we introduce an approach to allow for support of semantic service descriptions and queries using registries that conforms to UDDI V3 specification. Specifically, we discuss how to store complex semantic markups in the UDDI data model and use that information to perform semantic query processing. Our approach does not require any modification to the existing UDDI registries. The add-on modules reside only on clients who wish to take advantage of semantic capabilities. This approach is completely backward compatible and can integrate seamlessly into existing infrastructure.
View Abstract
Abstractions are important in specifying and proving properties of complex systems. To prove that a given automaton implements an abstract specification automaton, one must first find the correct abstraction relation between the states of the automata, and then show that this relation is preserved by all corresponding action sequences of the two automata. This paper describes tool support based on the PVS theorem prover that can help users accomplish the second task, in other words, in proving a candidate abstraction relation correct. This tool support relies on a clean and uniform technique for defining abstraction properties relating automata that uses library theories for defining abstraction relations and templates for specifying automata and abstraction theorems. The paper then describes how the templates and theories allow development of generic, high level PVS strategies that aid in the mechanization of abstraction proofs. These strategies first set up the standard subgoals for the abstraction proofs and then execute the standard initial proof steps for these subgoals, thus making the process of proving abstraction properties in PVS more automated. With suitable supplementary strategies to implement the "natural" proof steps needed to complete the proofs of any of the standard subgoals remaining to be proved, the abstraction proof strategies can form part of a set of mechanized proof steps that can be used interactively to translate high level proof sketches into PVS proofs. Using timed I/O automata examples taken from the literature, this paper illustrates use of th
View Abstract
James Robertson of the Atlantic Systems Guild argues that requirements analysts must also be inventors. "When it comes to the software that we build for clients, we must invent some of it," states Robertson. Connie Heitmeyer of NRL counters that designers, not analysts, should design. She argues that "The requirements analyst's task is largely one of discovery: By studying existing documentation, eliciting requirements from customers and domain experts, and analyzing the documented requirements for flaws, the analyst discovers (rather than invents) the new system's requirements."
View Abstract
Architectural patterns, analogous to design patterns, are a means to develop mechanisms for adding non-functional requirements, such as fault-tolerance, during the integration of hardware and software components. A synchronous language, the Secure Operations Language (SOL), was developed as a verifiable language for development of components (agents) to be ntegrated into high assurance systems. Agents written in SOL execute in a distributed nfrastructure allowing creation, deployment, migration, communication, etc. of these agents. his research addresses the generic extension f SOL to support architectural patterns. The architectural pattern, Hot Standby, which provides backup computational capability in case of failure of the primary resource, is exemplified. It is shown that formal properties, associated with such architectural patterns written in extended SOL are amenable to formal proof.
View Abstract
Formal specifications of required system behavior can be analyzed, verified, and validated, giving high confidence that the specification captures the desired behavior. Transferring this confidence to the system implementation depends on a formal link between requirements and implementation. The automatic generation of provably correct code provides just such a link. While optimization is usually performed on code to achieve efficiency, we propose to optimize the formal specification before generating code, thus providing optimization independent of the particular code generation method. This paper investigates the use of invariants in optimizing code generated from formal specifications in the Software Cost Reduction (SCR) tabular notation. We show that invariants (1) provide the basis for simplifying expressions that otherwise cannot be improved using traditional compiler optimization techniques, and (2) allow detection and elimination of parts of the specification that would lead to unreachable code.
View Abstract
Over the past two decades, formal methods researchers have produced a number of powerful software tools designed to detect errors in, and to verify properties of, hardware designs, software systems, and software system artifacts. Mostly used in the past to debug hardware designs, in future years, these tools should help developers improve the quality of software systems. They should be especially useful in developing "high assurance software systems," where compelling evidence is required that the system satisfies critical properties, such as safety and security. This paper describes the different roles that formally based software tools can play in improving the correctness of software and software artifacts. Such tools can help developers manage complexity by automatically exposing certain classes of software errors and by producing evidence (e.g., mechanically checked proofs, results of executing automatically generated test cases, etc.) that a software system satisfies its requirements. In addition, the tools allow practitioners to focus on development tasks best performed by people--e.g., obtaining and validating requirements and constructing a high-quality requirements specification.
View Abstract
Recent modifications to PVS support a new technique for defining abstraction properties relating automata in a clean and uniform way. This definition technique employs specification templates that can support development of generic high level PVS strategies that set up the standard subgoals of these abstraction proofs and then execute the standard initial proof steps for these subgoals. In this paper, we describe an abstraction specification technique and associated abstraction proof strategies we are developing for I/O automata. The new strategies can be used together with existing strategies in the TAME (Timed Automata Modeling Environment) interface to PVS; thus, our new templates and strategies provide an extension to TAME for proofs of abstraction. We illustrate how the extended set of TAME templates and strategies can be used to prove example I/O automata abstraction properties taken from the literature.
View Abstract
This tutorial provides an overview of the PVS strategy language, and explains how to define new PVS strategies and load them into PVS, and how to create a strategy package. It then discusses several useful techniques that can be used in developing user strategies, and provides examples that illustrate many of these techniques.
View Abstract
NSA's Security-Enhanced (SE) Linux enhances Linux by providing a specification language for security policies and a Flask-like architecture with a security server for enforcing policies defined in the language. While the security server refers to an internal form of the policy compiled form the policy specification, the description of the policy most understandable to the user is its ``source'' specification in the policy language. It is natural for users to expect to be able to analyze the properties of the policy from this source specification. But the policy language is very low level, making the high level properties of a policy difficult to deduce by inspection. For this reason, tools to help users with the analysis are necessary. The NRL project on analyzing SE Linux policies aims first to use mechanized support to analyze an example policy specification and then to customize this support for use by practitioners in the open source software community. This paper describes how we model policies in the analysis tool TAME, the kinds of analysis we can support, and prototype mechanical support to enable others to model example policies in TAME. The paper concludes with some general observations on desirable properties for a policy language. This paper summarizes the research described in our full paper that is to appear in the proceedings of the IEEE 4th International Workshop on Policies for Distributed Systems and Networks (POLICY 2003), Lake Como, Italy, June 4-6, 2003. The longer paper is also available as NRL Memorandum Report NRL/MR/5540--03-8659.
View Abstract
Security-Enhanced (SE) Linux is a modification of Linux initially released by NSA in January 2001 that provides a language for specifying Linux security policies and, as in the Flask architecture, a security server for enforcing policies defined in the language. To determine whether user requests to the operating system should be granted, the security server refers to an internal form of the policy compiled from the policy specification. Since the most convenient description of the policy for user understanding is its ``source'' specification in the policy language, it is natural for users to expect to be able to analyze the properties of the policy from this source specification. However, though specifications in the SE Linux policy language avoid implementation details, the policy language is very low-level, making the high level properties of a policy difficult to deduce by inspection. For this reason, tools to help users with the analysis are necessary. The goal of the NRL project on analyzing SE Linux security policies is to first use mechanized support to analyze the specification of an example policy, and then to customize this support for use by practitioners in the open source software community. This paper describes how we have modeled an example security policy in the analysis tool TAME, the kinds of analysis we can support, and prototype mechanical support to enable others to model example security policies in TAME. The paper concludes with some general observations on desirable properties for a policy language.
View Abstract
There is an increasing need within the Navy and Marine Corps for building distributed situation-aware applications that are rapidly reconfigurable and survivable in the face of attacks and changing mission needs. For the Navy's vision of Network Centric Warfare and the Total Ship Computing Environment to succeed, there is an urgent need for a secure, robust, and survivable network infrastructure for disseminating mission-critical information in a timely manner. It is widely believed that intelligent software agents provide the ability to build robust, agile, and efficient distributed applications. We outline how Secure Infrastructure for Networked Systems (SINS) being developed at the Naval Research Laboratory will provide commanders and warfighters the necessary middleware for constructing situation-aware Command and Control (C2) and combat applications. We pay particular attention to the correctness, survivability, and efficiency of the underlying middleware architecture, and develop a middleware definition language Secure Operations Language (SOL) that enables C2 and Combat applications to use this infrastructure in a seamless and scalable manner.
View Abstract
We explore the idea of faking a rational design process, a la Parnas and Clements, by the application of the extended SCR Method of Heitmeyer and Bharadwaj. We argue that the formal artefacts created as a result serve as the basis for determining the work products associated with each step of the process, and whose quality assessment is aided by the application of tools in the SCR Toolset. Further, since the products associated with each step have a consistent formal denotation, the approach opens the possibility of significantly automating many process steps.
View Abstract
In this paper we present an integrated formal framework for the specification and analysis of Multi-Agent Systems (MAS). Agents are specified in a synchronous programming language called Secure Operations Language (SOL) which supports the modular development of secure agents. Multi-agent systems are constructed from individual agent modules by using the composition operator of SOL, the semantics of which are guaranteed to preserve certain individual agent properties. The formal semantics and the underlying framework of SOL also serve as the basis for analysis and transformation techniques such as abstraction, consistency checking, verification by model checking or theorem proving, and automatic synthesis of agent code. Based on this framework, we are currently developing a suite of analysis and transformation tools for the formal specification, analysis, and synthesis of multi-agent systems.
View Abstract
This paper describes a compositional proof strategy for verifying properties of requirements specifications. The proof strategy, which may be applied using either a model checker or a theorem prover, uses known state invariants to prove state and transition invariants. Two proof rules are presented: a standard incremental proof rule analogous to Manna and Pnueli's incremental proof rule and a compositional proof rule. The advantage of applying the compositional rule is that it decomposes a large verification problem into smaller problems which often can be solved more efficiently than the larger problem. The steps needed to implement the compositional rule are described, and the results of applying the proof strategy to two examples, a simple cruise control system and a real-world Navy system, are presented. In the Navy example, compositional verification using either theorem proving or model checking was three times faster than verification based on the standard incremental (noncompositional) rule. In addition to the two above rules for proving invariants, a new compositional proof rule is presented for circular assume-guarantee proofs of invariants. While in principle the strategy and rules described for proving invariants may be applied to any state-based specification with parallel composition of components, the specifications in the paper are expressed in the SCR (Software Cost Reduction) tabular notation, the auxiliary invariants used in the proofs are automatically generated invariants, and the verification is supported by the SCR tools.
View Abstract
Model checking is a technique that has been successfully applied for the validat ion and verification of hardware specifications and communication protocols. In mission-critical syst ems of NASA and the DoD, various mobile devices generate information dynamically, and their state ch anges with time. Most often, a situation serves as a trigger for a new situation. Therefore, it is nec essary to extend existing model checking methods and tools in order to apply them for the validat ion and verification of situation-aware, mission-critical applications such as DoD command and contro l systems or the Navy s Total Ship Computing Environment. However, there are several problems to be ov ercome before these techniques become practical, such as overcoming the state explosion problem and adapting the V&V systems and algorithms to this application area. In this paper, we propose a new technique, founded on combining existing techniques in theorem proving and model checking to extend the application area of existing pure model checking methods. This paper also introduces state space reduction methods based on abstraction that ameliorate the state explosion problem. Future distrib uted real-time and embedded system must necessarily be highly adaptable, secure, and reliable. Exis ting system development techniques therefore need to be extended so that future systems have the capability to meet these new system requirements.
View Abstract
Formal specifications of software systems are extremely useful because they can be rigorously analyzed, verified, and validated, giving high confidence that the specification captures the desired behavior. To transfer this confidence to the actual source code implementation, a formal link is needed between the specification and the implementation. Generating the implementation directly from the specification provides one such link. A program transformation system such as Paige's APTS can be useful in developing a source code generator. This paper describes a case study in which APTS was used to produce code generators that construct C source code from a requirements specification in the SCR (Software Cost Reduction) tabular notation. In the study, two different code generation strategies were explored. The first strategy uses rewrite rules to transform the parse tree of an SCR specification into a parse tree for the corresponding C code. The second strategy associates a relation with each node of the specification parse tree. Each member of this relation acts as an attribute, holding the C code corresponding to the tree at the associated node; the root of the tree has the entire C program as its member of the relation. This paper describes the two code generators supported by APTS, how each was used to synthesize code for two example SCR requirements specifications, and what was learned about APTS from these implementations.
View Abstract
In this paper we discuss how we intend to develop a specialized theorem proving environment for the Hybrid I/O Automata (HIOA) framework over the PVS theorem prover, and some of the issues involved. In particular, we describe approaches to using PVS that allow and encourage the development of useful proof strategies, and note some desired PVS features that would further help us to do so for our HIOA environment.
View Abstract
There is an increasing need, within organizations such as the Department of Defense and NASA, for building distributed applications that are rapidly re-con gurable and survivable in the face of attacks and changing mission needs. Existing methods and tools are inadequate to deal with the multitude of challenges posed by application development for systems that may be distributed over multiple physical nodes separated by vast geographical distances. The problem is exacerbated in a hostile and unforgiving environment such as space where, in addition, systems are vulnerable to failures. It is widely believed that intelligent software agents are central to the development of agile, efficient, and robust distributed applications. This paper presents details of agent-based middleware that could be the basis for developing such applications. We pay particular attention to the correctness, survivability, and efficiency of the underlying middleware architecture, and develop a middleware definition language that permits applications to use this infrastructure in a scalable and seamless manner.
View Abstract
Security-Enhanced (SE) Linux, released by NSA in January, 2001, is a version of Linux that adds security features by superimposing the Flask architecture on its kernel. In this architecture, a security server decides whether to grant particular subjects (i.e., processes) permissions to particular objects. The decisions are based on a combination of type enforcement (TE), role-based access control (RBAC), and multilevel security (MLS) rules. SE Linux includes a policy language for defining these parts of the security policy. Because the policy language forces detailed specification of which access permissions may be granted, the relation of a policy definition to high level security goals is not obvious. The length and complexity of policy definitions (thousands of rules is typical) precludes proving a high level security property by inspection. For policy analysis, tool support is clearly needed. To be effective in practice, this tool support needs to be usable by members of the open source software community. This paper reports progress made towards adapting the theorem proving tool TAME to the analysis of SE Linux security policies, and making it usable to open source developers.
View Abstract
This paper describes a specialized interface to PVS called TAME (Timed Automata Modeling Environment) which provides automated support for proving properties of I/O automata. A major goal of TAME is to allow a software developer to use PVS to specify and prove properties of an I/O automaton efficiently and without first becoming a PVS expert. To accomplish this goal, TAME provides a template that the user completes to specify an I/O automaton and a set of proof steps natural for humans to use for proving properties of automata. Each proof step is implemented by a PVS strategy and possibly some auxiliary theories that support that strategy. We have used the results of two recent formal methods studies as a basis for two case studies to evaluate TAME. In the first formal methods study, Romijn used I/O automata to specify and verify memory and remote procedure call components of a concurrent system. In the second formal methods study, Devillers et al. specified a tree identify protocol (TIP), part of the IEEE 1394 bus protocol, and provided hand proofs of TIP properties. Devillers also used PVS to specify TIP and to check proofs of TIP properties. In our first case study, the third author, a new TAME user with no previous PVS experience, used TAME to create PVS specifications of the I/O automata formulated by Romijn and Devillers et al. and to check their hand proofs. In our second case study, the TAME approach to verification was compared with an alternate approach by Devillers which uses PVS directly.
View Abstract
The TESLA multicast stream authentication protocol is distinguished from other types of cryptographic protocols in both its key management scheme and its use of timing. It takes advantage of the stream being broadcast to periodically commit to and later reveal keys used by a receiver to verify that packets are authentic, and it uses both inductive reasoning and time arithmetic to allow the receiver to determine that an adversary cannot have prior knowledge of a key that has just been revealed. While an informal argument for the correctness of TESLA has been published, no mechanized proof appears to have previously been done for TESLA or any other protocol of the same variety. This paper reports on a mechanized correctness proof of the basic TESLA protocol based on establishing a sequence of invariants for the protocol using the tool TAME, an interface to PVS specialized for proving properties of automata. It discusses the organization and process used in the proof, and the possibilities for reusing these techniques in correctness proofs of similar protocols, starting with more sophisticated versions of TESLA.
View Abstract
Recently, there has been a great deal of interest in the application of formal methods, in particular precise formal notations and automatic analysis tools, for the creation and analysis of artifacts of requirements engineering. In this paper we discuss the role of formal methods in requirements engineering (RE), emphasizing that in contrast to their more conventional application in RE for the creation and analysis of requirements specifications, formal methods may be applied in a cost-effective way to answer specific questions about the domain by the construction and automated analysis of "domain models".
View Abstract
Building trusted applications is hard, especially in a distributed or mobile setting. Existing methods and tools are inadequate to deal with the multitude of challenges posed by distributed application development. The problem is exacerbated in a hostile environment such as the Internet where, in addition, applications are vulnerable to malicious attacks. It is widely acknowledged that intelligent software agents provide the right paradigm for developing agile, re-configurable, and efficient distributed applications. Distributed processing in general carries with it risks such as denial of service, Trojan horses, information leaks, and malicious code. Agent technology, by introducing autonomy and code mobility, may exacerbate some of these problems. In particular, a malicious agent could do serious damage to an unprotected host, and malicious hosts could damage agents or corrupt agent data.
Secure Infrastructure for Networked Systems (SINS) being developed at the Naval Research Laboratory is a middleware for secure agents intended to provide the required degree of trust for mobile agents, in addition to ensuring their compliance with a set of enforceable security policies. An infrastructure such as SINS is central to the successful deployment and transfer of distributed agent technology to Industry because security is a necessary prerequisite for distributed computing.
View Abstract
SOL (Secure Operations Language) is a synchronous programming language for implementing reactive systems. The utility of SOL hinges upon the fact that it is a secure language, i.e., most programs in SOL are amenable to fully automated static analysis techniques, such as automatic theorem proving using decision procedures or model checking. Among the unique features of SOL is the ability to express a wide class of enforceable safety and security policies (including the temporal aspects of software component interfaces) in the language itself, thereby opening up the possibility of eliminating runaway computations and malicious code, such as worms and viruses.
View Abstract
Building distributed agents is difficult. It is therefore not surprising that truly distributed applications for the Internet are few and far between. In this position paper, we argue that intelligent software agents are central to the development of the capabilities required to write robust, re-configurable, and survivable distributed applications.
View Abstract
There is an increasing need, within organizations such as the Department of Defense and NASA, for building distributed applications that are rapidly re-configurable and survivable in the face of attacks and changing mission needs. Existing methods and tools are inadequate to deal with the multitude of challenges posed by application development for systems that may be distributed over multiple physical nodes separated by vast geographical distances. The problem is exacerbated in a hostile and unforgiving environment such as space where, in addition, systems are vulnerable to failures. It is widely believed that intelligent software agents are central to the development of agile, efficient, and robust distributed applications. This paper presents details of agent-based middleware that could be the basis for developing such applications. We pay particular attention to the correctness, survivability, and efficiency of the underlying middleware architecture, and develop a middleware definition language that permits applications to use this infrastructure in a scalable and seamless manner.
View Abstract
This article reviews Software Cost Reduction (SCR), a set of techniques for designing software based on software engineering principles. The article focuses on the SCR techniques for constructing and evaluating the requirements document, the work product built during the requirements stage of software development, and the aspect of SCR that has been the topic of significant research. It also briefly describes, and gives pointers to, the SCR approach to software design, focusing on the design and documentation of the module structure, the module interfaces, and the uses hierarchy.
View Abstract
Maintaining consistency between requirements and the design developed to satisfy them is both important and difficult. Maintaining consistency is important to satisfying stakeholders' desires, which the requirements express. Much of the difficulty of maintaining consistency stems from having redundant descriptions of requirements decisions -- one in the requirements document and a second in the design document -- typically recorded in widely divergent languages. To ameliorate this problem, we write requirements and design in such a way that requirements decisions and their expression in the requirements document are incorporated directly into the design document, which organizes the decisions and includes additional design decisions.
View Abstract
TAME (Timed Automata Modeling Environment), an interface to the theorem proving system PVS, is designed for proving properties of three classes of automata: I/O automata, Lynch-Vaandrager timed automata, and SCR automata. TAME provides templates for specifying these automata, a set of auxiliary theories, and a set of specialized PVS strategies that rely on these theories and on the structure of automata specifications using the templates. Use of the TAME strategies simplifies the process of proving automaton properties, particularly state and transition invariants. TAME provides two types of strategies: strategies for ``automatic'' proof and strategies designed to implement ``natural'' proof steps, i.e., proof steps that mimic the high-level steps in typical natural language proofs. TAME's ``natural'' proof steps can be used both to mechanically check hand proofs in a straightforward way and to create proof scripts that can be understood without executing them in the PVS proof checker. Several new PVS features can be used to obtain better control and efficiency in user-defined strategies such as those used in TAME. This paper describes the TAME strategies, their use, and how their implementation exploits the structure of specifications and various PVS features. It also describes several features, currently unsupported in PVS, that would either allow additional ``natural'' proof steps in TAME or allow existing TAME proof steps to be improved. Lessons learned from TAME relevant to the development of similar specialized interfaces to PVS or other theorem provers are discussed.
View Abstract
The SCR (Software Cost Reduction) toolset contains tools for specifying, debugging, and verifying system and software requirements. The utility of the SCR tools in detecting specification errors, many involving safety properties, has been demonstrated recently in projects involving practical systems, such as the International Space Station, a flight guidance system, and a U.S. weapons system. This paper briefly describes our experience in applying the tools in the development of two secure systems: a communications device and a biometrics standard for user authentication.
View Abstract
In earlier work, we developed a fixpoint algorithm for automatically generating state invariants, properties that hold in each reachable state of a state machine model, from state-based requirements specifications. Such invariants are useful both in validating requirements specifications and as auxiliary lemmas in proofs that a requirements specification satisfies other invariant properties. This paper describes a new related algorithm that strengthens state invariants generated by our initial algorithm and demonstrates the new algorithm on a simplified version of an automobile cruise control system. The paper concludes by describing how the two algorithms were used to generate state invariants from a requirements specification of a cryptographic device and how the invariants in conjunction with a theorem prover were used to prove formally that the device satisfies a set of critical security properties.
View Abstract
TAME is a special-purpose interface to PVS designed to support developers of software systems in proving properties of automata models. One of TAME's major goals is to allow a software developer who has basic knowledge of standard logic, and can do hand proofs, to use PVS to represent and to prove properties about an automaton model without first becoming a PVS expert. A second goal is for a human to be able to read and understand the content of saved TAME proofs without running them through the PVS proof checker. A third goal is to make proving properties of automata with TAME less costly in human time than proving such properties using PVS directly. Recent work by Romijn and Devillers et al., based on the I/O automata model, has provided the basis for two case studies on how well TAME achieves these goals. Romijn specified the RPC-Memory Problem and its solution, while Devillers et al. specified a tree identify protocol. Hand proofs of specification properties were provided by the authors. In addition, Devillers et al. used PVS directly to mechanize the specifications and proofs of the tree identify protocol. In one case study, the third author, a new TAME user with no previous PVS experience, used TAME to create PVS specifications of the I/O automata presented by Romijn and Devillers et al. and to check the hand proofs of invariant properties. The PVS specifications and proofs of Devillers et al. provide the basis for the other case study, which compares the TAME approach to an alternate approach which uses PVS directly.
View Abstract
In high assurance avionics systems, such as systems for flight guidance, air traffic control, and collision avoidance, compelling evidence is required that the system behavior satisfies certain critical properties. Some critical properties are functional properties, i.e., properties of the services that the system delivers. For example, when another aircraft flies too close, a collision avoidance system must advice the pilot to move the aircraft up or down to avoid a collision. Researchers have proposed numerous approaches for specifying, constructing, and certifying high assurance systems. This paper presents a method, based on the SCR (Software Cost Reduction) requirements method, that has recently been developed for building high assurance systems. To illustrate the application of this method to avionics systems, we present the requirements specification of a small avionics system that was developed using the proposed approach.
View Abstract
Salsa is an invariant checker for specifications in SAL (the SCR Abstract Language). To establish a formula as an invariant without any user guidance Salsa carries out an induction proof that utilizes tightly integrated decision procedures, currently a combination of BDD algorithms and a constraint solver for integer linear arithmetic, for discharging the verification conditions. The user interface of Salsa is designed to mimic the interfaces of model checkers; i.e., given a formula and a system description, Salsa either establishes the formula as an invariant of the system (but returns no proof) or provides a counterexample. In either case, the algorithm will terminate. Unlike model checkers, Salsa returns a state pair as a counterexample and not an execution sequence. Also, due to the incompleteness of induction, users must validate the counterexamples. The use of induction enables Salsa to combat the state explosion problem that plagues model checkers -- it can handle specifications whose state spaces are too large for model checkers to analyze. Also, unlike general purpose theorem provers, Salsa concentrates on a single task and gains efficiency by employing a set of optimized heuristics.
View Abstract
To date, the SCR (Software Cost Reduction) requirements method has been used in industrial environments to specify the requirements of many practical systems, including control systems for nuclear power plants and avionics systems. This paper describes the use of the SCR method to specify the requirements of the Light Control System (LCS), the subject of a case study at the Dagstuhl Seminar on Requirements Capture, Documentation, and Validation in June 1999. It introduces a systematic process for constructing the LCS requirements specification, presents the specification of the LCS in the SCR tabular notation, discusses the tools that we applied to the LCS specification, and concludes with a discussion of a number of issues that arose in developing the specification.
View Abstract
Mechanical theorem provers have been shown to expose proof errors, some of them serious, that humans miss. Mechanical provers will be applied more widely if they are easier to use. The tool TAME (Timed Automata Modeling Environment) provides an interface to the prover PVS to simplify specifying and proving properties of automata models. Originally designed for reasoning about Lynch-Vaandrager (LV) timed automata, TAME has since been adapted to other automata models. This paper shows how TAME can be used to specify and verify properties of I/O automata, a class of untimed automata. It also describes the experiences of a new TAME user (the first author) who used TAME to check Lamport-style hand proofs of invariants for two applications: Romijn's solution to the RPC-Memory Problem and the verification by Devillers et al. of the tree identify phase of the IEEE 1394 bus protocol. For the latter application, the TAME mechanization of the hand proofs of Devillers is compared with the more direct PVS proofs of Devillers et al. Improvements to TAME in response to user feedback are discussed.
View Abstract
Although model checking has proven remarkably effective in detecting errors in hardware designs, its success in the analysis of software specifications has been limited. Model checking algorithms for hardware verification commonly use Binary Decision Diagrams (BDDs) to represent predicates involving the many Boolean variables commonly found in hardware descriptions. Unfortunately, BDD representations may be less effective for analyzing software specifications, which usually contain not only Booleans but variables spanning a wide range of data types. Further, software specifications typically have huge, sometimes infinite, state spaces that cannot be model checked directly using conventional symbolic methods. One promising but largely unexplored approach to model checking software specifications is to apply mathematically sound abstraction methods. Such methods extract a reduced model from the specification, thus making model checking feasible. Currently, users of model checkers routinely analyze reduced models but often generate the models in ad hoc ways. As a result, the reduced models may be incorrect.This paper, an expanded version of (Bharadwaj and Heitmeyer, 1997), describes how one can model check a complete requirements specification expressed in the SCR (Software Cost Reduction) tabular notation. Unlike previous approaches which applied model checking to mode transition tables with Boolean variables, we use model checking to analyze properties of a complete SCR specification with variables ranging over many data types. The paper also describes two sound and, under certain conditions, complete methods for producing abstractions from requirements specifications. These abstractions are derived from the specification and the property to be analyzed. Finally, the paper describes how SCR requirements specifications can be translated into the languages of Spin, an explicit state model checker, and SMV, a symbolic model checker, and presents the results of model checking two sample SCR specifications using our abstraction methods and the two model checkers.
View Abstract
Recently, many formal methods, such as the SCR (Software Cost Reduction) requirements method, have been proposed for improving the quality of software specifications. Although improved specifications are valuable, the ultimate objective of software development is to produce software that satisfies its requirements. To evaluate the correctness of a software implementation, one can apply black-box testing to determine whether the implementation, given a sequence of system inputs, produces the correct system outputs. This paper describes a specification-based method for constructing a suite of "test sequences", where a test sequence is a sequence of inputs and outputs for testing a software implementation. The test sequences are derived from a tabular SCR requirements specification containing diverse data types, i.e., integer, boolean, and enumerated types. From the functions defined in the SCR specification, the method forms a collection of predicates called "branches", which cover all possible software behaviors described by the specification. Based on these predicates, the method then derives a suite of test sequences by using a model checker's ability to construct counterexamples. The paper presents the results of applying our method to four specifications, including a sizable component of a contractor specification of a real system.
View Abstract
To date, the tabular-based SCR (Software Cost Reduction) method has been applied mostly to the development of embedded control systems. This paper describes the successful application of the SCR method, including the SCR* toolset, to a different class of system, a COMSEC (Communications Security) device called CD that must correctly manage encrypted communications. The paper summarizes how the tools in SCR* were used to validate and to debug the SCR specification and to demonstrate that the specification satisfies a set of critical security properties. The development of the CD specification involved many tools in SCR*: a specification editor, a consistency checker, a simulator, the TAME interface to the theorem prover PVS, and various other analysis tools. Our experience provides evidence that use of the SCR* toolset to develop high-quality requirements specifications of moderately complex COMSEC systems is both practical and low-cost.
View Abstract
A controversial issue in the formal methods community is the degree to which mathematical sophistication and theorem proving skills should be needed to apply a formal method. A fundamental assumption of this paper is that formal methods research has produced several classes of analysis that can prove useful in software development. However, to be useful to software practitioners, most of whom lack advanced mathematical training and theorem proving skills, current formal methods need a number of additional attributes, including more user-friendly notations, completely automatic (i.e., pushbutton) analysis, and useful, easy to understand feedback. Moreover, formal methods need to be integrated into a standard development process. I discuss additional research and engineering that is needed to make the current set of formal methods more practical. To illustrate the ideas, I present several examples, many taken from the SCR (Software Cost Reduction) requirements method, a formal method that software developers can apply without theorem proving skills, knowledge of temporal and higher order logics, or consultation with formal methods experts.
View Abstract
A controversial issue in the formal methods community is the degree to which mathematical sophistication and theorem proving skills should be needed to apply a formal method and its support tools. This paper describes the SCR (Software Cost Reduction) tools, part of a "practical" formal method--a method with a solid mathematical foundation that software developers can apply without theorem proving skills, knowledge of temporal and higher order logics, or consultation with formal methods experts. The SCR method provides a tabular notation for specifying requirements and a set of "light-weight" tools that detect several classes of errors automatically. The method also provides support for more "heavy-duty" tools, such as a model checker. To make model checking feasible, users can automatically apply one or more abstraction methods.
View Abstract
Exposing inconsistencies can uncover many defects in software specifications. One approach to exposing inconsistencies analyzes two redundant specifications, one operational and the other property-based, and reports discrepancies. This paper describes a "practical" formal method, based on this approach and the SCR (Software Cost Reduction) tabular notation, that can expose inconsistencies in software requirements specifications. Because users of the method do not need advanced mathematical training or theorem proving skills, most software developers should be able to apply the method without extraordinary effort. This paper also describes an application of the method which exposed a safety violation in the contractor-produced software requirements specification of a sizable, safety-critical control system. Because the enormous state space of specifications of practical software usually renders direct analysis impractical, a common approach is to apply abstraction to the specification. To reduce the state space of the control system specification, two "pushbutton" abstraction methods were applied, one which automatically removes irrelevant variables and a second which replaces the large, possibly infinite, type sets of certain variables with smaller type sets. Analyzing the reduced specification with the model checker Spin uncovered a possible safety violation. Simulation demonstrated that the safety violation was not spurious but an actual defect in the original specification.
View Abstract
Automatic generation of state invariants, properties that hold in every reachable state of a state machine model, can be valuable in software development. Not only can such invariants be presented to system users for validation, in addition, they can be used as auxiliary assertions in proving other invariants. This paper describes an algorithm for the automatic generation of state invariants that, in contrast to most other such algorithms, which operate on programs, derives invariants from requirements specifications. Generating invariants from requirements specifications rather than programs has two advantages: 1) because requirements specifications, unlike programs, are at a high level of abstraction, generation of and analysis using such invariants is easier, and 2) using invariants to detect errors during the requirements phase is considerably more cost-effective than using invariants later in software development. To illustrate the algorithm, we use it to generate state invariants from requirements specifications of an automobile cruise control system and a simple control system for a nuclear plant. The invariants are derived from specifications expressed in the SCR (Software Cost Reduction) tabular notation.
View Abstract
Although a number of mechanical provers have been introduced and applied widely by academic researchers, these provers are rarely used in the practical development of software. For mechanical provers to be used more widely in practice, two major barriers must be overcome. First, the languages provided by the mechanical provers for expressing the required system behavior must be more natural for software developers. Second, the reasoning steps supported by mechanical provers are usually at too low and detailed a level and therefore discourage use of the prover. To help remove these barriers, we are developing a system called TAME, a high-level user interface to PVS for specifying and proving properties of automata models. TAME provides both a standard specification format for automata models and numerous high-level proof steps appropriate for reasoning about automata models. In previous work, we have shown how TAME can be useful in proving properties about systems described as Lynch-Vaandrager Timed Automata models. TAME has the potential to be used as a PVS interface for other specification methods that are specialized to define automata models. This paper first describes recent improvements to TAME, and then presents our initial results in using TAME to provide theorem proving support for the SCR (Software Cost Reduction) requirements method, a method with a wide range of other mechanized support.
View Abstract
This report describes the results of a case study on the feasibility of developing and applying mechanical methods, based on the proof system PVS, to prove propositions about real-time systems specified in the Lynch-Vaandrager timed automata model. In using automated provers to prove propositions about systems described by a specific mathematical model, both the proofs and the proof process can be simplified by exploiting the special properties of the mathematical model. Because both specifications and methods of reasoning about them tend to be repetitive, the use of a standard template for specifications, accompanied by standard shared theories and standard proof strategies or tactics, is often feasible. Presented are the PVS specification of three theories that underlie the timed automata model, a template for specifying timed automata models in PVS, and an example of its instantiation. Both hand proofs and the corresponding PVS proofs of two propositions are provided to illustrate how these can be made parallel at different degrees of granularity. Our experience in applying PVS to specify and reason about real-time systems modeled as timed automata is also discussed. The methods for reasoning about timed automata in PVS developed in the study have evolved into a system called TAME (Timed Automata Modeling Environment). A summary of recent developments regarding TAME is provided. A shorter version of the report was presented at the 1996 Real-Time Applications Symposium.
View Abstract
A major barrier to more common use of mechanical theorem provers in verifying software designs is the significant distance between proof styles natural to humans and proof styles supported by mechanical provers. To make mechanical provers useful to software designers with some mathematical sophistication but without expertise in mechanical provers, the distance between hand proofs and their mechanized versions must be reduced. To achieve this, we are developing a mechanical prover called TAME on top of PVS. TAME is designed to process proof steps that resemble in style and size the typical steps in hand proofs. TAME's support of more natural proof steps should not only facilitate mechanized checking of hand proofs, but in addition should provide assurance that theorems proved mechanically are true for the reasons expected and also provide a basis for conceptual level feedback when a mechanized proof fails. While infeasible for all applications, designing a prover that can process a set of high-level, natural proof steps for restricted domains should be achievable. In developing TAME, we have had moderate success in defining specialized proof strategies to validate hand proofs of properties of Lynch-Vaandrager timed automata. This paper reports on our successes, the services provided by PVS that support these successes, and some desired enhancements to PVS that would permit us to improve and extend TAME.
View Abstract
Verifying properties of hybrid systems can be highly complex. To reduce the effort required to produce a correct proof, the use of mechanical verification techniques is promising. Recently, we extended a mechanical verification system, originally developed to reason about deterministic real-time automata, to verify properties of hybrid systems. To evaluate our approach, we applied our extended proof system to a solution, based on the Lynch-Vaandrager timed automata model, of the Steam Boiler Controller problem, a hybrid systems benchmark. This paper reviews our mechanical verification system, which builds on SRI's Prototype Verification System (PVS), and describes the features we added to handle hybrid systems. It also discusses some errors we detected in applying our system to the benchmark problem. We conclude with a summary of insights we acquired in using our system to specify and verify hybrid systems.
View Abstract
Researchers at the Naval Research Laboratory (NRL) have been developing a formal method, known as the SCR (Software Cost Reduction) method, to specify the requirements of software systems using tables. NRL has developed a formal state machine model defining the SCR semantics and support tools for analysis and validation. Recently, a verification capability was added to the SCR toolset. Users can now invoke the Spin model checker within the toolset to establish properties of a specification. This paper describes the results of our initial experiments to verify properties of SCR requirements specifications using Spin. After reviewing the SCR requirements method and introducing our formal requirements model, we describe how SCR specifications can be translated into an imperative programming notation. We also describe how we limit state explosion by verifying abstractions of the original requirements specification. These abstractions are derived using the formula to be verified and special attributes of SCR specifications. The paper concludes with the results of our experiments with Spin and a discussion of ongoing and future work.
View Abstract
Although formal methods for developing computer systems have been available for more than a decade, few have had significant impact in practice. A major barrier to their use is that developers find formal methods difficult to understand and apply. One exception is a formal method called SCR for specifying computer system requirements which, due to its easy-to-use tabular notation and demonstrated scalability, has achieved some success in industry. To demonstrate and evaluate the SCR method and tools, we recently used SCR to specify the requirements of a simplified mode control panel for the Boeing 737 autopilot. This paper presents the SCR requirements specification of the autopilot, outlines the process we used to create the SCR specification from a prose description, and discusses the problems and questions that arose in developing the specification. Formalizing and analyzing the requirements specification in SCR uncovered a number of problems with the original prose description, such as incorrect assumptions about the environment, incompleteness, and inconsistency. The paper also introduces a new tabular format we found useful in understanding and analyzing the required behavior of the autopilot. Finally, the paper compares the SCR approach to requirements with that of Rickey Butler of NASA Langley Research Center, who uses the PVS language and prover of SRI International to represent and analyze the autopilot requirements.
View Abstract
This paper reports the results of a case study on the feasibility of developing and applying mechanical methods, based on the proof system PVS, to prove propositions about real-time systems specified in the Lynch-Vaandrager timed automata model. In using automated provers to prove propositions about systems described by a specific mathematical model, both the proofs and the proof process can be simplified by exploiting the special properties of the mathematical model. This paper presents the PVS specification of three theories that underlie the timed automata model, a template for specifying timed automata models in PVS and an example of its instantiation, and both hand proofs and the corresponding PVS proofs of two propositions. It concludes with a discussion of our experience in applying PVS to specify and reason about real-time systems modeled as timed automata.
View Abstract
Assuring the correctness of specifications of real-time systems can involve significant human effort. The use of a mechanical theorem prover to encode such specifications and to verify their properties could significantly reduce this effort. A barrier to routinely encoding and mechanically verifying specifications has been the need first to master the specification language and logic of a general theorem proving system. Our approach to overcoming this barrier is to provide mechanical support for producing specifications and verifying proofs, specialized for particular mathematical models and proof techniques. We are currently developing a mechanical verification system called TAME (Timed Automata Modeling Environment) that provides this specialized support using SRI's Prototype Verification System (PVS). Our system is intended to permit steps in reasoning similar to those in hand proofs that use model-specific techniques. TAME has recently been used to detect errors in a realistic example.
View Abstract
This paper describes a formal analysis technique, called consistency checking, for automatic detection of errors, such as type errors, nondeterminism, missing cases, and circular definitions, in requirements specifications. The technique is designed to analyze requirements specifications expressed in the SCR (Software Cost Reduction) tabular notation. As background, the SCR approach to specifying requirements is reviewed. To provide a formal semantics for the SCR notation and a foundation for consistency checking, a formal requirements model is introduced; the model represents a software system as a finite state automaton, which produces externally visible outputs in response to changes in monitored environmental quantities. Results are presented of two experiments which evaluated the utility and scalability of our technique for consistency checking in a real-world avionics application. The role of consistency checking during the requirements phase of software development is discussed.
View Abstract
This paper describes a class of formal analysis called consistency checking that mechanically checks requirements specifications, expressed in the SCR tabular notation, for application-independent properties. Properties include domain coverage, type correctness, and determinism. As background, the SCR notation for specifying requirements is reviewed. A formal requirements model describing the meaning of the SCR notation is summarized, and consistency checks derived from the formal model are described. The results of experiments to evaluate the utility of automated consistency checking are presented.
View Abstract
A set of CASE tools is described for developing formal requirements specifications expressed in the SCR (Software Cost Reduction) tabular notation. The tools include an editor for building the specifications, a consistency checker for testing the specifications for consistency with a formal requirements model, a simulator for symbollically excecuting the specifications, and a verifier for checking that the specifications satisfy selected application properties. As background, the SCR method for specifying requirements is reviewed, and a formal requirements model is introduced. Examples are presented to illustrate the tools.
View Abstract
As computers and their supporting communication networks have become increasingly enmeshed in our national technological fabric, we have become increasingly dependent on high assurance computer systems, i.e., computer systems for which compelling evidence is required that the system delivers its services in a manner that satisfies certain critical properties. Examples of high assurance systems include military systems (e.g., weapon systems, C4I systems, etc), flight programs for both commercial and military aircraft, air traffic control systems, financial and commerce systems, medical systems (including medical databases and medical equipment), etc. These systems are extremely complicated and the science and engineering principles that underlie them are yet to be completely worked out. Nevertheless, our national well-being depends upon these systems satisfying certain critical properties including security properties, safety properties, real-time properties, and fault-tolerance properties. This paper briefly summarizes the results of a 1995 workshop on high assurance systems, identifies several examples of high assurance systems that were discussed, provides some details of one of the systems as a representative example, describes some problems that need to be addressed by basic research as well as problems that hinder the use of research results in practical applications, and proposes a research agenda.
View Abstract
A new solution to the Generalized Railroad Crossing problem, based on timed automata, invariants and simulation mappings, is presented and evaluated. The solution shows formally the correspondence between four system descriptions: an axiomatic specification, an operational specification, a discrete system implementation, and a system implementation that works with a continuous gate model. The details of the proofs, omitted from the conference paper due to lack of space, are included.
View Abstract
A new solution to the Generalized Railroad Crossing problem, based on timed automata, invariants and simulation mappings, is presented and evaluated. The solution shows formally the correspondence between four system descriptions: an axiomatic specification, an operational specification, a discrete system implementation, and a system implementation that works with a continuous gate model.
View Abstract
This paper describes a number of issues in human-computer interaction that arose in two projects which are developing CASE tools to support formal methods. It also proposes a research agenda.
View Abstract
This paper introduces MT, a collection of integrated tools for specifying and analyzing real-time systems using the Modechart language. The toolset includes facilities for creating and editing Modechart specifications. Users may symbolically execute the specifications with an automatic simulation tool to make sure that the specified behavior is what was intended. They may also invoke a verifier that uses model-checking to determine whether the specifications imply (satisfy) any of a broad class of safety assertions. To illustrate the toolset's capabilities as well as several issues that arise when formal methods are applied to real-world systems, the paper includes specifications and analysis procedures for a software component taken from an actual Naval real-time system.
View Abstract
This paper describes the Generic Railroad Crossing (GRC) Problem, which has become a popular benchmark for evaluating formal techniques for specifying and analyzing real-time systems.