Data processing: software development – installation – and managem – Software program development tool – Translation of code
Reexamination Certificate
1997-07-02
2002-05-07
Powell, Mark R. (Department: 2122)
Data processing: software development, installation, and managem
Software program development tool
Translation of code
C717S152000, C717S152000
Reexamination Certificate
active
06385765
ABSTRACT:
BACKGROUND OF THE INVENTION
1. Field of the Invention
This invention generally concerns methods for specifying and verifying systems having concurrently executing components and specifically concerns specification, simulation, verification, implementation and testing of concurrent and distributed systems.
2. Description of the Related Art
There are innumerable concurrent and distributed systems working and implemented each day throughout the world and, in some instances, beyond our world. Communication protocols, security protocols, embedded systems and process control systems are all examples of concurrent systems. These systems have become increasingly important to our personal lives and our society. Nearly every aspect of modern life is touched by a concurrent or distributed system multiple times each day. Our dependence on these systems makes their reliability critical. Therefore, their reliability should be insured.
There have been several industry and government studies done on the reliability and quality of commercially available software. These studies have consistently found software to be below accepted quality standards. The number of failures and “bugs” present in commercially available software is well above what is tolerated in other industries. The United States government and several software industry groups have begun efforts to implement quality control standards for commercial software. The greatest obstacle confronting these efforts is the lack of means to study, ascertain and correct errors within software designs and code.
Concomitantly, the design and implementation of concurrent and distributed systems have become increasingly more sophisticated and expensive. To insure these systems are being designed and implemented correctly and will perform in the manner intended without failure or error, certain computer aided software engineering (CASE) tools have been developed. CASE tools aim to ease and sometimes automate the process of software development.
Verification tools are a type of CASE tool that provide a means for verifying whether a planned or pre-existing system will satisfy its requirements. The use of CASE tools, and especially verification tools, can lead to the detection of errors early within the system development life cycle. The early detection of design errors will lead to money and time saved, increased quality and greater reliability and robustness of the final system.
Most existing verification tools have been designed to analyze synchronous hardware systems. Such tools, typically found in computer aided design (CAD) packages, are being routinely used in the hardware industry. However, asynchronous systems, possessing multiple independent threads of control, are becoming more prevalent. Software systems are typically asynchronous and the popularity of asynchronous hardware design is increasing. Thus, the need for verification tools for asynchronous systems is acute. This need is further accentuated since many functions originally performed in hardware are now being delegated to software systems.
Most verification tools today are severely limited in their ability to analyze these complex systems. One source of this limitation is known as the “state explosion” problem. A “state” in this context is a possible configuration the system can enter, or, alternatively, a snapshot of the system's execution.
State explosion occurs because, in general, the size of a system's state space grows exponentially in the size of the system's description. Therefore, the analysis of systems with relatively succinct descriptions can prove intractable for even the most powerful computers available.
To overcome state explosion, partial-order reduction techniques have been developed. Partial-order reduction is made possible since some system states, and the execution paths leading to these states are, in a formal sense, redundant. These redundancies can be safely ignored without compromising verification efforts. By avoiding these redundant states during analysis, the size of the state space to be searched may be dramatically reduced.
Another technique that has been developed for overcoming state explosion is local verification. Local verification is incremental, demand driven exploration of the state space, depending on the needs of the specific verification task at hand.
Model checking is a formal verification technique based on state exploration. Model checking allows one to check whether a state-machine representation of a system is a model of, or satisfies, a formula in temporal logic. Temporal logic allows for the specification of critical system properties such as freedom from deadlock and eventual service guarantees. Temporal logic formulas can be seen as mathematically precise system requirements.
The input to a model checker is a state-machine-based specification of the system to be verified and one or more system properties expressed in temporal logic. The output is either a declaration that the property is true or an identification of a portion of the state space falsifying the property.
There are several commercial and academic version model checkers available today. These use versions of temporal logic that restrict the class of logical properties that can be expressed.
SUMMARY OF THE INVENTION
Software designed to analyze and generate concurrent and distributed systems is herein disclosed. The invention's preferred embodiment comprises specification, simulation, verification, and code-generation capabilities.
For specification, the invention comprises graphical and textual editors. In the preferred embodiment, these allow one to render systems in GCCS and VPL. GCCS is a graphical coordination language for specifying hierarchically structured systems of communicating state machines. The GCCS network editor allows users to define the communication topology of their system in terms of nodes and communication links. Each node represents a system (network), and systems may be composed of sub-systems, sub-systems may be composed of sub-sub-systems, and so on. At the lowest level of a GCCS hierarchy are processes. The graphical process editor supports the creation of state machines. Users may also create networks and processes using VPL.
Two distinguishing aspects of GCCS and its realization via the network and process editors are: (1) GCCS has a formal “operational semantics” that allows GCCS-based specifications to be simulated and analyzed in mathematically precise ways; (2) GCCS is a true coordination language in the sense that any notation for processes with a suitable operational semantics could be used for defining processes.
VPL stands for “value passing language”. It is a textual specification language used to define system components that exchange data values and that exhibit complex control structure. The invention contains a VPL editor that allows users to input VPL descriptions in a structure-based way. The VPL editor also performs static type checking to ensure that the right kinds of values are communicated in all contexts. Like GCCS, VPL is equipped with a formal operational semantics.
The graphical/textual combination is extremely useful in practice. In system design, some aspects (e.g. system architecture) are best captured graphically, while others (e.g. complex data and control structures) are easier to express textually. This improves the efficiency of system designers and maintainers.
Preferably, each editor comprises a structure-based editor and static type checker. The structure-based editor guarantees that one's input is syntactically correct. The static type checker insures that all data is used in a sound and complete manner.
The specification tools of this invention support open system specifications and support the analysis of subsystems independently of other subsystems. These tools can describe and analyze system components without specifying the entire system. These tools overcome what has been necessary, closed-world assumptions made by other specification tools. Since GCCS is able to combine syst
Cleaveland Rance
Lewis Philip M.
Ramakrishna Y. S.
Smolka Scott A.
Ingberg Todd
Powell Mark R.
The Research Foundation
LandOfFree
Specification and verification for concurrent systems with... does not yet have a rating. At this time, there are no reviews or comments for this patent.
If you have personal experience with Specification and verification for concurrent systems with..., we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Specification and verification for concurrent systems with... will most certainly appreciate the feedback.
Profile ID: LFUS-PAI-O-2861996