Contact Information:
- Email: scr@itd.nrl.navy.mil
- Phone: (202) 404-8888
- Fax: (202) 404-7942
- U.S. Mail:
- Naval Research Laboratory
Code 5546
4555 Overlook Ave, SW
Washington, DC 20375-5337
- Building Location:
- Building 12, Room 143
- Phone: (202) 404-8888
-
Selected Publications:
2008
"Applying Infinite State Model Checking and Other Analysis Techniques to Tabular Requirements Specifications of Safety-Critical Systems," Design Automation for Embedded Systems, Vol. 12, Issues 1-2, pp. 97-137, June 2008. PDF
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.
"Applying Formal Methods to a Certifiably Secure Software System," IEEE Transactions on Software Engineering, vol. 34, no. 1, pp. 82-98, January 2008. PDF
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.
2007
"RE Theory Meets Software Practice: Lessons from the Software Development Trenches," Proceedings, 15th IEEE International Requirements Engineering Conference, pp. 265-268, New Delhi, India, October 2007. PDF
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.
"Formal Methods for Specifying, Validating, and Verifying Requirements," Journal of Universal Computer Science 13, 5, pp. 607-618, May 2007. PDF
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.
"Applying a Formal Requirements Method to Three NASA Systems: Lessons Learned," Proceedings of the 2007 IEEE Aerospace Conference, Big Sky, MT, March 2007. PDF
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.
2006
"Formal specification and verification of data separation in a separation kernel for an embedded system," Proceedings of the 13th ACM Conference on Computer and Communications Security (CCS 2006), Alexandria, VA, pp. 346-355, 2006. PDF
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.
"Analyzing Tabular Requirements Specifications Using Infinite State Model Checking," Proceedings, Fourth ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE'06), July 27-29, 2006, Napa, California. PDF,
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.
"Generating Optimized Code from SCR Specifications," in Proceedings, ACM SIGPLAN/SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES 2006), Ottawa, Canada, June 14-16, 2006. PDF
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 specifications. Moreover, code generation is relatively fast, and the code produced is relatively compact.
2005
"Tools for constructing requirements specifications: The SCR toolset at the age of ten," International Journal of Computer Systems Science and Engineering, 20(1): 19-35, January 2005. PDF
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.
"Point/Counterpoint," IEEE Software, January 2005, Volume 22, Issue 1, Jan.-Feb. 2005, pp. 48-51. PDF
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."
2004
"Managing complexity in software development with formally based tools," Proc. ETAPS Workshop on Formal Foundations of Software and Component-Based Software Architectures (FESCA 2004), Barcelona, SP, April 3 2004, ENTCS 236, Elsevier, Amsterdam (invited paper). PDF
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.
2003
"Program Synthesis from Formal Requirements Specifications using APTS", Higher-Order and Symbolic Computation 16 (1-2): 63-92, March - June, 2003, Kluwer Academic Publishers. PDF
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.
"A Strategy for Efficiently Verifying Requirements Specifications Using Composition and Invariants," to appear in Proc. European Software Engineering Conference/ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE 2003), Helsinki, Finland, September 1-5, 2003. PostScript, PDFThis 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.
2002
"Proving Invariants of I/O Automata with TAME", In Automated Software Engineering, Vol.9, 201-232. PostScript, PDF
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.
"Software Cost Reduction," Encyclopedia of Software Engineering, Two Volumes, John J. Marciniak, editor, ISBN: 0-471-02895-9, January 2002. PostScript, PDF
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.
2001
"Applying `Practical' Formal Methods to the Specification and Analysis of Security Properties," in Proc. Information Assurance in Computer Networks (MMM-ACNS 2001), LCNS 2052, Springer-Verlag, St. Petersburg, Russia, May 21-23, 2001. PostScript, PDF
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.
"An Algorithm for Strengthening State Invariants Generated from Requirements Specifications", in Proc. Fifth IEEE Int'l Symp. on Requirements Engineering (RE'01), Aug. 27-31, 2001, Toronto, Canada. PostScript, PDF
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. Keywords: requirements, specification, formal methods, invariants, verification, validation, software tools
"A security model for military message systems: retrospective," Proceedings 17th Annual Computer Security Applications Conference (ACSAC '01), pp. 174-190, 10-14 Dec 2001. PDF
Originally published in the 1984 ACM Transactions on Computer Systems, this paper was republished in 2001 as a "classic paper" in computer security. The Introduction to the Classic Papers by Dan Thomsen of Secure Computing Corporation (ACSAC '01 Proceedings, p. 161) states that because computer security is a "relatively new field that spans a wide range of topics", the question is how to sort through computer security history to find the data needed by computer security practitioners when they are "swamped with just the data published in the past year." The answer, according to Thomsen, is "to dust off papers that influenced security thought and print them again." In addition to republishing their papers, the authors of the three selected papers were asked to update their papers, place them in historical perspective, and describe what happened to the work after publication. This paper deals with a basic component of computer security: application-specific security policies.
2000"Using TAME to Prove Invariants of Automata Models: Two Case Studies", Proc. Third ACM Workshop on Formal Methods in Software Practice (FMSP'00), Portland, OR, August 24-25, 2000. To appear. PostScript, PDF
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.
"Developing High Assurance Avionics Systems with the SCR Requirements Method," in Proc. 19th Digital Avionics Systems Conference, 7-13 October 2000, Philadelphia, PA. PostScript, PDF
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.
"Applying the SCR Requirements Method to the Light Control Case Study", Journal of Universal Computer Science (JUCS), August 2000. PostScript, PDF
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.
"Applying TAME to I/O Automata: A User's Perspective". NRL Memorandum Report NRL.MR.5540--00-8848, April 10, 2000. PostScript, PDF
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.
1999"Hardware/Software Co-Design and Co-Validation Using the SCR Method", In Proc. IEEE International High Level Design Validation and Test Workshop (HLDVT'99), San Diego, Nov 1999. PostScript, PDF
To date, the SCR (Software Cost Reduction) method has been used to specify system requirements. This paper extends the SCR method to hardware/software co-design and co-validation. Our approach consists of three steps. First, the SCR method is used to specify the required system behavior, i.e., the required relation between environmental quantities (called monitored quantities) that the system monitors and environmental quantities (called controlled quantities) that the system controls. Next, the system designers specify the I/O devices required to compute estimates of the monitored quantities and to set values of the controlled quantities. Finally, the required software behavior is specified as three modules: a device-independent module, specifying how the (estimated) monitored quantities are to be used to compute estimates of the controlled quantities, and two device-dependent modules: an input device interface module, specifying how data from the input devices are to be used to compute estimates of the monitored quantities, and an output device interface module, specifying how the values of controlled variables are written to output devices. To illustrate the approach, we use SCR to specify a simple light control system.
"Model Checking Complete Requirements Specifications Using Abstraction," Automated Software Engineering, Vol 6, No. 1, pp. 37-68, January 1999, Kluwer Academic Publishers. PDF
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.
"Using Model Checking to Generate Tests from Requirements Specifications," Proc., Joint 7th Eur. Software Engineering Conf. and 7th ACM SIGSOFT Intern. Symp. on Foundations of Software Eng. (ESEC/FSE99), Toulouse, FR, Sept. 6-10, 1999. Postscript
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.
"Formal Methods for Developing Software Specifications: Paths to Wider Usage," Proceedings of the International Conf. on Parallel and Distributed Processing Techniques and Applications (PDPTA '99), Las Vegas, June 28-July 1, 1999. PostScript
Although many formal methods have been proposed for improving the quality of software specifications, a number of barriers to widespread use of these methods remain. This paper describes four of these barriers---failure to scale, unnatural interfaces, limited analysis capabilities, and insufficient tool integration---and suggests some promising approaches for overcoming them. These approaches include automated abstraction, user interfaces designed for ease of use, and the application of powerful decision procedures. To illustrate the barriers and approaches to overcoming them, several examples are presented based on the SCR (Software Cost Reduction) requirements method.
SCR: A Practical Approach to Building a High Assurance COMSEC System, Proc. 15th Annual Computer Security Applications Conference (ACSAC '99), IEEE Computer Society Press, December, 1999. To appear. PostScript, PDF
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.
Applying Formal Methods to an Information Security Device: An Experience Report Proc. 4th IEEE International Symposium on High Assurance Systems Engineering (HASE '99), IEEE Computer Society Press, November, 1999, pp. 81-88. PostScript, PDF
SCR (Software Cost Reduction) is a formal method for specifying and analyzing system requirements that has previously been applied to control systems. This paper describes a case study in which the SCR method was used to specify and analyze a different class of system, a cryptographic system called CD, which must satisfy a large set of security properties. The paper describes how a suite of tools supporting SCR---a consistency checker, simulator, model checker, invariant generator, theorem prover, and validity checker---were used to detect errors in the SCR specification of CD and to verify that the specification satisfies seven security properties. The paper also describes issues of concern to software developers about formal methods---e.g., ease of use, cost-effectiveness, scalability, how to translate a prose specification into a formal notation, and what process to follow in applying a formal method---and discusses these issues based on our experience with CD. Also described are some unexpected results of our case study.
Applying Formal Methods to an Information Security Device: A Case Study, Proc. of the Information Systems Technology Panel Symposium on Protecting NATO Information Systems in the 21st Century, Washington, DC, October, 1999. PostScript, PDF
One approach to assuring information security is to control access to information through an appropriately designed device. A cost-effective way to provide assurance that the device meets its security requirements is to detect and correct violations of these requirements at an early stage of development: when the operational requirements are specified. Once it is demonstrated that an operational requirements specification is complete and consistent, that it captures the intended device behavior, and that the operational specification satisfies the security requirements, this operational specification can be used both to guide development of implementations and to generate test sets for testing implementations. This paper describes the application of the SCR (Software Cost Reduction) requirements method and the NRL's SCR* toolset, which includes a set of verification and validation tools, to a US Navy communications security device. It reports on our success in proving that the operational requirements specification satisfies a set of security properties. The paper also discusses the practicality and cost of applying formal methods to the development of security devices.
1998"Formal Methods for Developing High Assurance Computer Systems: Working Group Report." Proceedings, Second IEEE Workshop on Industrial-Strength Formal Techniques (WIFT'98), Boca Raton, FL, Oct. 19, 1998. PostScript, PDF
This paper presents the results of a discussion conducted at the Workshop on Industrial-Strength Formal Techniques in October 1998 on the topic, "Formal Methods for Developing High Assurance Systems." It addresses three issues: the uses of formal methods in software development, the barriers to the use of formal methods in software development, and approaches to overcoming the barriers.
"On the Need for 'Practical' Formal Methods," Formal Techniques in Real-Time and Real-Time Fault-Tolerant Systems, Proc., 5th Intern. Symposium (FTRTFT'98), Lyngby, Denmark, September 14-18, 1998, LICS 1486, pp. 18-26, (invited paper). PostScript, PDF
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.
"SCR*: A Toolset for Specifying and Analyzing Software Requirements," Proc. Computer-Aided Verification, 10th Ann. Conf. (CAV'98), Vancouver, Canada, 1998. PostScript, PDF
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.
"Using the SCR* Toolset to Specify Software Requirements." Proceedings, Second IEEE Workshop on Industrial Strength Formal Specification Techniques (WIFT'98), Boca Raton, FL, Oct. 19, 1998. PostScript, PDF
Formulated in the late 1970s to specify the requirements of the Operational Flight Program (OFP) of the A-7 aircraft, the SCR (Software Cost Reduction) requirements method is a method based on tables for specifying the requirements of software systems. During the 1980s and the early 1990s, many companies, including Bell Laboratories, Grumman, Ontario Hydro, and Lockheed, applied the SCR requirements method to practical systems. Each of these applications of SCR had, at most, weak tool support. To provide powerful, robust tool support customized for the SCR method, we have developed the SCR* toolset. To provide formal underpinnings for the method, we have also developed a formal model which defines the semantics of SCR requirements specifications.
"Using Abstraction and Model Checking to Detect Safety Violations in Requirements Specifications," IEEE Transactions on Software Engineering, vol. 24, no. 11, November 1998. PostScript, PDF
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.
"SCR: A Practical Method for Requirements Specification," Proc., 17th AIAA/IEEE/SAE Digital Avionics System Conference (DASC), Bellevue, WA, Oct. 31-Nov. 7, 1998. PostScript, PDF
A controversial issue in the formal methods research community is the degree to which mathematical sophistication and theorem proving skills should be needed to apply a formal method. A premise of this paper is that formal methods research has produced several techniques with potential utility in practical software development, but that mathematical sophistication and theorem proving skills should not be prerequisites for using these techniques. In the paper, several attributes needed to make a formal method useful in practice are described. These attributes include user-friendly notation, automated (i.e., push-button) analysis, and easy to understand feedback. To illustrate the attributes of a practical formal method, a formal method for requirements specification called SCR (Software Cost Reduction) is introduced.
"Automatic Generation of State Invariants from Requirements Specifications," to be presented at 6th International Symposium on the Foundations of Software Engineering (FSE-6), Orlando FL, Nov. 3-5, 1998. PostScript, PDF
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.
"TAME: A PVS Interface to Simplify Proofs for Automata Models," UITP '98, July 1998. PostScript, PDF
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.
"Mechanical Verification of Timed Automata: A Case Study," NRL Memorandum Report 5546-98-8180, April, 1998. PostScript, PDF
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.
"Applying the SCR Requirements Method to a Weapons Control Panel: An Experience Report." To be presented at Formal Methods in Software Practice '98, Clearwater Beach, FL, March 4-5, 1998. PostScript, PDF
A major barrier to the use of formal methods in software practice is the difficulty software developers have understanding and applying the methods. To overcome this barrier, a requirements method called SCR (Software Cost Reduction) offers a user-friendly tabular notation to specify software requirements and a collection of easy-to-use tools that automatically detect many classes of errors in requirements specifications. This paper describes our experience in applying the SCR method and tools to a safety-critical military application---the problems encountered in translating the original contractor-produced software requirements specification into SCR and the lessons learned in applying the SCR technology to a practical system. The short time required to apply the SCR method, the serious safety violation detected, and the working system prototype produced demonstrate the utility and potential cost-effectiveness of SCR for developing safety-critical systems.
1997
"Human-Style Theorem Proving Using PVS," To be presented at TPHOLs '97, Murray Hill, NJ, August 19-22, 1997. PostScript, PDF
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.
"Verifying Hybrid Systems Modeled as Timed Automata: A Case Study," Proceedings of HART '97, Grenoble, France, March 26-28, 1997. PostScript, PDF
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.
"Verifying SCR Requirements Specifications using State Exploration," Proceedings of First ACM SIGPLAN Workshop on Automatic Analysis of Software, Paris, France, January 14, 1997. PostScript, PDF
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.
"Applying the SCR Requirements Method to a Simple Autopilot, " To be presented at the Fourth NASA Langley Formal Methods Workshop, Hampton, VA, September 10-12, 1997. PostScript [Warning: 4 MB!], PDF
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.
"Model Checking Complete Requirements Specifications Using Abstraction," NRL Memorandum Report NRL/MR/5540--97-7999, November 10, 1997. PostScript, PDF
Although model checking has proven remarkably effective in detecting errors in hardware designs, its success in the analysis of software specifications has been quite limited. Model checking algorithms for hardware verification commonly use Binary Decision Diagrams (BDDs), a highly effective technique for analyzing specifications with the scores of Boolean variables commonly found in hardware descriptions. Unfortunately, BDDs are relatively ineffective for analyzing software specifications, which usually contain not only Booleans but variables spanning a wide range of data types. Further, software specifications have huge, often infinite, state spaces that cannot be model checked directly using conventional symbolic methods. One promising, but largely unexplored technique for limiting the size of the state space to be analyzed by model checking is to extract a model with a smaller state space from a complete specification using sound abstraction methods. Users of model checkers routinely analyze reduced models, but most often generate the models in ad hoc ways. As a result, the reduced models are often incorrect.
This report first describes how one can model check a complete requirements specification expressed in the SCR (Software Cost Reduction) tabular notation. Unlike previous approaches, which apply model checking to mode transition tables with Boolean variables, we use model checking to analyze properties of complete SCR specifications with variables ranging over many data types. The report also describes two sound and complete methods for producing abstractions from requirements specifications. These abstractions are derived from the specification based on the property to be analyzed. Finally, the report 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.
"Tools for Formal Specification, Verification, and Validation of Requirements," Proceedings of 12th Annual Conference on Computer Assurance (COMPASS '97), June 16-19, 1997, Gaithersburg, MD. (Accepted for presentation) PostScript [Warning: 20 MB!], PDF
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 software 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 its demonstrated scalability, has already achieved some success in industry. Recently, a set of software tools, including a specification editor, a consistency checker, a simulator, and a verifier, has been developed to support the SCR method [9, 11, 5]. This paper describes recent enhancements to the SCR tools: a new dependency graph browser which displays the dependencies among the variables in the specification, an improved consistency checker which produces detailed feedback about detected errors, and an assertion checker which checks application properties during simulation. To illustrate the tool enchancements, a simple automobile cruise control system is presented and analyzed.
1996
"Mechanical Verification of Timed Automata: A Case Study," Proceedings of the 1996 Real-Time Technology and Applications Symposium, 1996. PostScript, PDF
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.
"TAME: A Specialized Specification and Verification System for Timed Automata," Presented in the Work in Progress session at RTSS '96, Washington, D.C., December 4-6, 1996. PostScript, PDF
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.
"Applying the SCR Requirements Specification Method to Practical Systems: A Case Study," Presented at the 21st Software Engineering Workshop, NASA GSFC, Greenbelt MD, USA, Dec 4-5, 1996. PostScript, PDF
Researchers at the Naval Research Laboratory (NRL) have been working on a formal method based on tables, known as the Software Cost Reduction (SCR) method, to specify the requirements of practical systems. In this paper, we present an SCR requirements specification of a simplified mode control panel for the Boeing 737 autopilot. We use the autopilot mode control panel as an example for comparing and contrasting the SCR approach to requirements specification and analysis with the approach of Ricky Butler, who uses the language of SRI's Prototype Verification System (PVS). We conclude with a discussion of general issues such as the appropriate level of abstraction for documenting requirements, the choice of notation, the kinds of analyses that can be performed, and the role of tool support.
"Automated Consistency Checking of Requirements Specifications," ACM Trans. on Software Eng. and Methodology 5, 3, July 1996, 231-261. PostScript, PDF
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.
Formal Methods for Real-Time Computing. Trends in Software, Volume 4. John Wiley, Chichester, U.K., 1996. Overview
"Formal Methods for Real-Time Computing: An Overview,", in Formal Methods for Real-Time Computing. John Wiley, New York, 1996.
This chapter defines real-time systems and illustrates them with a number of small examples. It also discusses issues central to applying formal methods in the development of real-time systems: the trade-offs between operational and descriptive specifications, different levels of formality that can be applied, and the requirements of formal methods for building industrial-strength systems. To put the newer formal methods into perspective, two methods widely used in practice to design and analyze real-time systems, namely, structured analysis and Statecharts, are reviewed. Several promising new techniques for specifying and analyzing real-time systems are then summarized and illustrated with examples. These include graphical notations, state machine and logic-based models, process algebras, and analysis techniques, such as model checking and deductive reasoning.
"Formal Verification of Real-Time Systems Using Timed Automata,", in Formal Methods for Real-Time Computing. John Wiley, New York, 1996.
The use of the Lynch-Vaandrager timed automaton model is illustrated with a solution to the Generalized Railroad Crossing problem. The solution shows formally the correspondence between four system descriptions: an axiomatic (i.e., descriptive) specification, an operational specification represented in terms of timed automata, a discrete system implementation, and a system implementation that works with a continuous gate model. Several sample proofs are given. In the development of the solution, a number of guidelines were applied. These guidelines, which should prove useful in applying formal methods to practical systems, are described and illustrated with examples.
"Requirements Specifications for Hybrid Systems," Proceedings, Hybrid Systems Workshop III, Lecture Notes in Computer Science, Springer-Verlag, edited by R. Alur, T. Henzinger, and E. Sontag, 1996. PostScript, PDF
This paper presents a formal framework for representing and reasoning about the requirements of hybrid computer systems. By a hybrid computer system, we mean a computer system whose environment includes both continuous and discrete entities. As background, the paper briefly reviews an abstract model for specifying system and software requirements, called the Four Variable Model, and a related requirements method, called SCR (Software Cost Reduction). The paper then introduces a special discrete version of the Four Variable Model, called the SCR requirements model, and suggests how the SCR model can be extended to specify and to reason about hybrid systems. Examples of how the SCR model can be used to specify a system's timing and accuracy requirements are given.
1995
"Consistency Checking of SCR-Style Requirements Specifications," Proceedings, International Symposium on Requirements Engineering, York, England, March 26-27, 1995. PostScript, PDF
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.
"SCR*: A Toolset for Specifying and Analyzing Requirements," Proceedings of the Tenth Annual Conference on Computer Assurance (COMPASS '95), Gaithersburg, MD, June 25-29, 1995, pp. 109-122. PostScript, PDF
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.
"High Assurance Computer Systems: A Research Agenda," America in the Age of Information, National Science and Technology Council Committee on Information and Communications Forum, Bethesda, 1995. PostScript, PDF
1994
"The Generalized Railroad Crossing: A Case Study in Formal Verification of Real-Time Systems," NRL Memorandum Report 7619, Naval Research Laboratory, Wash., DC, Dec. 1994. PostScript, PDF
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.
"The Generalized Railroad Crossing: A Case Study in Formal Verification of Real-Time Systems," Proceedings, IEEE Real-Time Systems Symposium, San Juan, Puerto Rico, Dec. 7-9, 1994. PostScript, PDF
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 Role of HCI in CASE Tools Supporting Formal Methods", Proceedings, Workshop on Software Engineering an human-Computer Interaction, Sorrento, Italy, May 16-17, 1994. PostScript, PDF
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.
1993
"MT: A toolset for specifying and analyzing real-time systems," Proc. IEEE Real-Time Systems Symposium, 1993, pp. 12 -22. PDF
"A Benchmark for Comparing Different Approaches for Specifying and Verifying Real-Time Systems," Proceedings, Tenth IEEE Workshop on Real-Time Operating Systems and Software, IEEE Computer Society Press, 1993. PostScript, PDF
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.
1984
"A Security Model for Military Message Systems,'' ACM Transactions on Computer Systems, vol. 2, no. 3, Aug. 1984.
"A Formal Statement of the MMS Security Model," Proc. 1984, IEEE Symposium on Research in Security and Privacy, IEEE Press, 1984.
1983
"Abstract Requirements Specification: A New Approach and Its Application,'' IEEE Transcactions on Software Engineering, vol. 9, no. 5, Sept. 1983.
Related Web Servers
Automatic Construction of High Assurance Systems from Requirements Specifications
Project Description:
In previous research funded by NRL's 6.1 Base Program, Code 5546 has developed a comprehensive formal model and numerous algorithms and other formal techniques for developing complete, consistent and correct software requirements specifications. In this new 6.1 program, Code 5546 is undertaking new research that will produce a formal foundation for transforming a verified, validated requirements specification into a reliable, provably correct, efficient software implementation. The formal foundation is intended to allow the development of user-friendly automated support for the tranformation process. The result will be a tool set and methodology that can support the full software development cycle for developers of Navy and other high assurance applications.
Principal Investigator: Constance Heitmeyer
Sponsor: Office of Naval Research (NRL Base 6.1 Program)
The appearance of external hyperlinks does not constitute endorsement by the United States Department of Defense, the United States Department of the Navy and The Naval Research Laboratory of the linked web sites, or the information, products or services contained therein. For other than authorized activities such as military exchanges and Morale, Welfare and Recreation (MWR) sites, the United States Department of Defense, the Department of the Navy and The Naval Research Laboratory does not exercise any editorial control over the information you may find at these locations. Such links are provided consistent with the stated purpose of this DoD web site.