Search

Semiconductor companies have increasingly adopted a methodology that starts with a system-level design specification in C/C++/SystemC. This model is extensively simulated to ensure correct functionality and performance. Later, a Register Transfer Level (RTL) implementation is created in Verilog, either manually by a designer or automatically by a high-level synthesis tool. It is essential to check that the C and Verilog programs are consistent. In this paper, we present a two-step approach, embodied in two equivalence checking tools, VERIFOX and HW-CBMC, to validate designs at the software and RTL levels, respectively. VERIFOX is used for equivalence checking of an untimed software model in C against a high-level reference model in C. HW-CBMC verifies the equivalence of a Verilog RTL implementation against an untimed software model in C. To evaluate our tools, we applied them to a commercial floating-point arithmetic unit (FPU) from ARM and an open-source dual-path floating-point adder.

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, properties of the services that the system delivers. For example, when another aircraft flies too close, a collision avoidance system must advise the pilot to move the aircraft up or down to avoid a collision. Besides functional properties, four other classes of critical system properties may be identified: security, safety, realtime, and fault-tolerance. In most cases, an avionics system must satisfy properties in more than a single class. For example, a collision avoidance system must satisfy not only functional properties, but real-time constraints, fault-tolerance properties, and safety properties., Published in the Proceedings of the 19th Digital Avionics Systems Conference, held in Philadelphia, PA on 7-13 Oct 2000.

This paper introduces MT, a collection of integrated tools for specifying and analyzing real-time systems using the Mode chart language. The toolset includes facilities for creating and editing Modechart specifications. Users may symbolically execute the specifications with an automatic simulation too! 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 Navy real-time system.

To be considered correct or useful, real-time systems must deliver results within specified time intervals, either without exception or with high probability. Recently, a large number of formal methods have been invented for specifying and verifying real-time systems. It has been suggested that these formal methods need to be tested out on actual real-time systems. Such testing will allow the scalability of the methods to be assessed and also will uncover new problems requiring a formal solution. However, before these methods can be productively applied to industrial systems, greater understanding is needed about how they compare (e.g., what classes of problems they are designed to solve, the availability of mechanical support, etc.). To provide insight into the utility of different methods for solving real-time problems, the authors have developed a generic version of a real-time railroad crossing system. Their plan is to use this example as a benchmark for comparing different formalisms. In this paper, the authors define the problem, describe three classes of formalisms that can be applied, and summarize efforts currently in progress to specify the system of interest and prove properties about its behavior., Prepared in cooperation with Locus, Inc., Alexandria, VA.

This report presents informal specifications for the user commands supported by three message systems, all members of the Military Message System (MMS) family. The message systems constitute a family because it is worthwhile to study their similarities before studying their differences. The members of the MMS family share a common definition of security. This report is intended to be an example of both good requirements documentation and an appropriate design for a secure message system. Keywords include: Computer security, Message systems, Requirements documentation, Software engineering, Specifications, Office automation, and Program families.

Military systems that process classified information must operate in a secure manner; i.e., they must protect information adequately against unauthorized disclosure, modification, and withholding. A goal of current research in computer security is to facilitate the construction of multilevel secure systems, systems that protect information of various classifications from users with different clearances. Security models are used to define the concept of security embodied by a computer system. A single model, called the Bell-LaPadula model, has dominated recent efforts to build secure systems but has deficiencies. We are developing a new approach to defining security models based on the idea that a security model should be derived from a specific application. To evaluate our approach, we have formulated a security model for a family of military message systems. This report introduces the message-system application, describes the problems of using the Bell-LaPadula model in real applications, presents our security model both informally and formally, and summarizes our approach to developing secure message systems. Significant aspects of the security model are its definition of multilevel objects and its inclusion of application-dependent security assertions. Prototypes based on this model are being developed.

Military systems that process classified information must operate in a secure manner, i.e., they must adequately protect information against unauthorized disclosure, modification, and withholding. A goal of current research in computer security is to facilitate the construction of multilevel secure systems, i.e., systems that protect information of different classifications from users with different clearances. Security models are used to define the concept of security embodied by a computer system. A single model, called the Bell and LaPadula model, has dominated recent efforts to build secure systems but has some deficiencies. We are developing a new approach to defining security models based on the idea that a security model should be derived from a specific application. To evaluate our approach, we are formulating a security model for a family of military message systems. This paper introduces the message system application, summarizes our approach to developing a family of secure message systems, presents our security model, and summarizes our plans. (Author)

This is the notebook from the updated edition of the well-received course originated by the Naval Research Laboratory and taught annually for the past six years. It is a two-week technical course for personnel managing a software project or designing software. The purpose of the course is to improve the participant's ability to evaluate software requirements, specifications, design, correctness, and maintainability. Its purpose is not to transform the participant into an expert software designer. The course concentrates on technical problems of software design. It introduces generally accepted design practices, as well as software design research that may result in practical design applications in the near future. Design for ease of maintenance is emphasized. All course material is unclassified. Topics covered include information-hiding modules (modules that isolate the effects of changes), abstract interfaces (a technique for designing the interfaces of information-hiding modules), responses to undesired events, cooperating sequential processes (in real-time systems, software tasks in which scheduling and resource allocation decisions are not embedded), disciplined documentation techniques, techniques for formal specification, and designing systems with useful subsets. (Author)