Data processing: software development – installation – and managem – Software program development tool – Translation of code
Reexamination Certificate
1999-06-11
2002-01-29
Dam, Tuan Q. (Department: 2122)
Data processing: software development, installation, and managem
Software program development tool
Translation of code
C717S152000, C717S152000, C703S002000
Reexamination Certificate
active
06343372
ABSTRACT:
FIELD OF THE INVENTION
The invention relates to the generation of a verified algorithm, e.g., an abstraction algorithm, capable of transforming a program, e.g., a protocol and associated correctness properties, from a first form, e.g., concrete or original, to a second form, e.g., abstracted, and more particularly to the generation of such algorithm via an implicit syntax approach to a formal metatheory of programming languages.
BACKGROUND OF THE INVENTION
As is well known, a system model is a computer program, block of code, or set of program operations that, upon execution, simulates intended properties, i.e., functions and/or features, of a subject system. That is, a system model may represent a system's protocol and/or specification and its correctness properties, as will be explained. The system model is typically designed to accept inputs, perform functions and generate outputs in the same manner as would the actual system. By way of example, it may be useful to create a system model that simulates a communications protocol in order to test the protocol prior to use in a communication system. However, once a system model is created, the model must be verified to determine whether the model accurately simulates the intended properties of the system. This can be accomplished by inputting the model to a model checker. The model checker is a computer program, block of code, or set of program operations that verifies that the performance of the model matches the desired system behavior envisioned by the system designer.
In formal verification, the system model is converted into a finite state machine. As is well known, a finite state machine is a set of states and state transitions which mimic the operation of the system model in response to any given set of system model inputs. More particularly, each state represents a state or operational mode that the system model would enter given a set of inputs, and each transition state indicates the condition, i.e., the value of system model inputs and system model variables, that must be satisfied for the system model to successfully transition from one state to another state.
Once a system model is converted to a state machine, a model checker can test whether the system model operates in accordance with the desired set of expected behaviors, i.e., system properties. In operation, the checker varies the system model inputs and monitors which states the system model enters as a result of the inputs. As will be appreciated by those skilled in the art, this operation is known as searching the state space of the system model. While searching the system model state space, the model checker checks whether the system model enters a state or a cycle of states which the system designers have defined as so-called “bad” or unintended operations. Thus, the model checker can identify for the system designers particular problematic system design features that require redesign in order to comply with intended system performance.
However, it is also known that more complicated systems require more complicated system models. This means that the state machine used to represent the system model includes more states and more state transitions, thus, a larger state space. Unfortunately, when the state space becomes larger, it becomes more difficult to determine whether the model is correct. In order to reduce the difficulty in verifying the correctness of such large models, model creators have proposed generating an abstracted version of the model, i.e., a model that represents the actual system but that includes a reduced set of states and transitions. The abstracted system model then serves as input to the model checker. The model checker then has less difficulty in verifying the reduced state program. This abstraction approach requires the creation of an abstraction algorithm (i.e., computer program, block of code, or set of program operations) capable of transforming the original system model into an abstracted system model. However, it must be proven or verified that the abstraction algorithm applies to the model sought to be abstracted. That is, it is critical that the abstraction algorithm be verified for correctness with respect to the protocol or specification to be input thereto.
It is known that theorem proving and model checking can be combined in a useful manner by employing a theorem proving system to verify abstractions of protocols or system specifications, i.e., system models. In particular, as mentioned above, one can often use a model checker to verify some property of a protocol that has an infinite or intractably large state space, by first transforming the original or concrete protocol into a more abstracted version for which model checking is feasible. For example, this is described in: P. Wolper, “Expressing Interesting Properties of Programs in Propositional Temporal Logic,” In Proc. 13
th
Ann. ACM Symp. On Principles of Prog. Lang., January 1986; and E. M. Clarke, O. Grumberg, and D. E. Long, “Model Checking and Abstraction,” In Proc. 19
th
Ann. ACM Symp. on Principles of Prog. Lang., January 1992. A theorem prover can be used to check, for example, that the property (or some transformation of it) holds of the abstract protocol if and only if it holds of the original protocol. This can be done directly by formalizing the two versions of the protocol and proving the specific property of interest. This approach is taken in K. Havelund and N. Shankar, “Experiments in Theorem Proving and Model Checking for Protocol Verification,” In Proc. of Formal Methods in Europe (FME), 1996, which discloses using the integration of a BDD (boolean decision diagram) based model checker as a decision procedure in the theorem prover PVS (Prototype Verification System). PVS is disclosed in S. Rajan, N. Shankar, and M. K. Srivas, “An Integration of Model Checking with Automated Proof Checking,” In Proc. of the Seventh International Conference on Computer Aided Verification (CAV '95), Vol. 939 of Lecture Notes in Computer Science, pages 84-97, Springer-Verlag, 1995.
One can also provide general support for doing this kind of reasoning by formalizing a refinement calculus and methodology relating system specifications and abstractions, as in O. Muller, “A Verification Environment for I/O Automata Based on Formalized Metatheory,” PhD thesis, Technische Universitat Munchen, 1998. One can also use a model checker with assumption commitment style reasoning on the abstract system and then use a theorem prover to discharge the assumptions in the concrete system, as in J. Dingel and T. Filkorn, “Model Checking for Infinite State Systems Using Data Abstraction, Assumption-Commitment Style Reasoning and Theorem Proving,” In Proc. of the Seventh International Conference on Computer Aided Verification (CAV '95), Vol. 939 of Lecture Notes in Computer Science, pages 54-69, 1995.
Typically, when a system specification is represented in a theorem prover, a so-called “shallow embedding” is used. In a shallow embedding of a programming or specification language in a theorem prover, programs and specifications are directly interpreted in the logic of the theorem prover. Thus, one formalizes only the semantics of the language. For example, the commands of an imperative programming language might be encoded as objects of type com=state→state, with language constructs for forming commands being operators over this type, for example c
1
; c
2
=&lgr;s:state.c
2
(c
1
(s)). Thus, in a shallow embedding, the commands of the imperative language are defined as particular functions of type com, but the type com will also contain objects that are not the meaning of any command expressible in the given programming language.
In comparison to shallow embedding, “deep embedding” of a programming or specification language includes representing both the semantics and syntax of the embedded formalism in the theorem prover. Using this approach, one might have a type comsyn consisting of abstract syntax trees of commands, and then a meaning function M&e
Felty Amy Patricia
Howe Douglas J.
Roychoudhury Abhik
Dam Tuan Q.
Lucent Technologies - Inc.
Ryan & Mason & Lewis, LLP
LandOfFree
Methods and apparatus for generating a verified algorithm... does not yet have a rating. At this time, there are no reviews or comments for this patent.
If you have personal experience with Methods and apparatus for generating a verified algorithm..., we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Methods and apparatus for generating a verified algorithm... will most certainly appreciate the feedback.
Profile ID: LFUS-PAI-O-2875041