Model checking of liveness property in a phase abstracted model

Phase abstraction may be utilized to increase efficiency of model checking techniques. A liveness property may be checked in respect to a phase abstracted model by modifying the liveness property in accordance with the phase abstracted model. A fairness property may be modified to ensure that the fairness property is held by the model checker. A counter-example produced by a model checker is modified to be in accordance to an original model. The counter-example comprises a repetitive behavior. The counter-example may be modified to shorten the repetitive behavior or to apply the repetitive behavior in an earlier cycle of the counter-example.

BACKGROUND

The present disclosure relates to formal verification in general, and to model checking of liveness properties in particular.

Computerized devices are an important part of the modern life. They control almost every aspect of our life—from writing documents to controlling traffic lights. However, computerized devices are bug-prone, and thus require a testing phase in which the bugs should be discovered. The testing phase is considered one of the most difficult tasks in developing a computerized device. Many developers of computerized devices invest a significant portion, such as 70%, of the development cycle to discover erroneous behaviors of the computerized device, also referred to as a target computerized system. The target computerized system may comprise hardware, software, firmware, a combination thereof and the like.

During the testing phase formal verification techniques may be applied to verify that a predetermined property is held. Formal verification may utilize a model checker to verify that the predetermined property, also referred to as a specification, is held. A model, also referred to as a design, represents a set of Boolean variables and functions for determining their values depending on environment inputs and on a portion of the set of Boolean variables. The Boolean variables are also referred to as registers. The model therefore represents all possible behaviors of the target computerized system over discrete time, also referred to as cycles. A gate in a model represents a portion of the model having a value, such as a variable, an outcome of a function based on values of one or more variables and the like.

The predetermined property may be a safety properties, in case it may be refuted using a finite counter-example. The predetermined property may be a liveness property in case it may only be refuted using an infinite counter-example. For example, a safety property may state that a “bad” event never happens, and be refuted by showing an exemplary finite trace in which the last state comprises the “bad” event occurring; whereas a liveness property may state that a “good” event eventually happens, for example, that “Process A eventually enters the critical section”. A refutation of such liveness property may be provided by showing an infinite trace in which the “good” event never occurs.

Some additional exemplary liveness properties may be “starvation freedom”, e.g., ensuring that the progress is always made; termination, e.g. ensuring that the final instruction may always be completed; “guaranteed service”, e.g. a service may always be eventually serviced and the like.

A counter-example for a liveness property is a description of an infinite behavior of the target computerized system. The infinite behavior is described using a finite number of states which are divided to a prefix and a suffix. The suffix also referred to as a loop or a repetitive portion of the counter-example, represents a repetitive behavior of a finite number of states for which the first state occurs after the last state, and therefore describe an infinite behavior.

In order to insure an “interesting” counter-example, the model may be required to comply with a fairness property. For example, in a model of a priority queue in which a message of high priority is passed before a message of low priority, a liveness property requiring that eventually every low priority message is removed from the queue may be refuted by a scenario in which in every cycle a new high priority message is received. An exemplary fairness property would require the input to provide both low priority and high priority messages.

In order to increase efficiency of the model checker, phase abstraction may be applied on an original model, producing a phase abstracted model. Phase abstraction is a technique that may reduce the size of a model by unfolding the transition relation function of the model, such that the transition relation function of the phase abstracted model represents more than one transitions in the model. Some may view a phase abstracted model as a model in which each cycle represents several cycles in the original model.

BRIEF SUMMARY OF THE INVENTION

One exemplary embodiment of the disclosed subject matter is a computerized system comprising: a processor; an interface for receiving a phase abstracted model; an interface for receiving an original liveness property associated with the original model; and a property modifier for transforming the original liveness property to a phase abstracted liveness property.

Another exemplary embodiment of the disclosed subject matter is a method comprising: retrieving a phase abstracted model, the phase abstracted model is a result of a phase abstraction on an original model; retrieving an original liveness property associated with the original model; and transforming the original liveness property to a phase abstracted liveness property; the transforming the original liveness property is performed using a processor; whereby the original liveness property is transformed to the phase abstracted liveness property that may be checked in respect to the phase abstracted model.

Yet another exemplary embodiment of the disclosed subject matter is a computer program product comprising: a computer readable medium; first program instruction for retrieving a phase abstracted model, the phase abstracted model is a result of a phase abstraction on an original model; second program instruction for retrieving an original liveness property associated with the original model; and third program instruction for transforming the original liveness property to a phase abstracted liveness property; wherein the first, second and third program instructions are stored on the computer readable medium.

DETAILED DESCRIPTION

One technical problem dealt with by the disclosed subject matter is to enable model checking of liveness properties in respect to phase abstracted model. Another technical problem dealt with by the disclosed subject matter is to preserve fairness properties in the phase abstracted model in accordance with the original model. Yet another technical problem dealt with by the disclosed subject matter is to provide a counter-example relating to the original model. Yet another technical problem dealt with by the disclosed subject matter is to provide a minimized counter-example, such as that a repetitive portion of the counter-example comprises a relatively small number of cycles or that the repetitive portion begins in the counter-example in a relatively early cycle.

One technical solution is to determine a phase abstracted liveness property in respect to the original liveness property. Another technical solution is to conjunct gates in the phase abstracted model to determine a phase abstracted liveness property. Yet another technical solution is to determine a phase abstracted fairness property in respect to the original fairness property. Yet another technical solution is to disjunct gates in the phase abstracted model to determine a phase abstracted fairness property. Yet another technical solution is to determine a cycle in the original model associated with a cycle in the phase abstracted model in which a repetitive behavior may end. Yet another technical solution is to determine a cycle in the original model associated with a cycle in the phase abstracted model in which a repetitive behavior may begin. Yet another technical solution is to determine a second repetitive behavior associated with a first repetitive behavior; the second repetitive behavior comprises less cycles than the first repetitive behavior; the first and second repetitive behaviors are comprised by a counter-example. Yet another technical solution is to determine a deterministic counter-example based on a non-deterministic counter-example associated with a liveness property. Yet another technical solution is to determine a deterministic counter-example using a satisfiability solver.

One technical effect of utilizing the disclosed subject matter is transforming an original liveness property to a phase abstracted liveness property. Another technical effect of utilizing the disclosed subject matter is transforming an original fairness property to a phase abstracted fairness property. Yet another technical solution of utilizing the disclosed subject matter is determining a counter-example based on an original counter-example generated in respect to a liveness property and a phase abstracted model.

Referring now toFIG. 1showing a computerized environment in which the disclosed subject matter is used, in accordance with some exemplary embodiments of the subject matter.

A computerized environment100may comprise a phase abstraction module110which may transform an original model105to a phase abstracted model115. A cycle in the phase abstracted model115, also referred to as a frame, is associated with a predetermined number of cycles in the original model105, such as for example four cycles. For a first register in the original model105the phase abstracted model115may comprise several registers associated with the first register. The several registers may represent a value of the first register in a frame. For example, in case the frame is four cycles, there may be four registers associated with the value of the first register, each corresponding to a different cycle in the frame, such as the first cycle of every frame, the second cycle of every frame and the like. A gate in the phase abstracted model associated with another gate in the original model in a cycle of a frame is also referred to as an unfolded gate.

The computerized environment100may comprise a phase abstraction adapter120configured to adapt an original liveness property118in accordance with the phase abstracted model115. The phase abstraction adapter120may determine a phase abstracted liveness property125. In some exemplary embodiments, the phase abstraction adapter120may further transform the phase abstracted model115to preserve an original fairness property.

The computerized environment100may comprise a model checker130utilized for model checking the phase abstracted model115in respect to the phase abstracted liveness property125. The model checker130may determine that a model preserves the phase abstracted liveness property125. The model checker130may alternatively determine that the model does not preserve the phase abstracted liveness property125. The model checker may further determine an original counter-example135exemplifying a behavior of the phase abstracted model115which does not comply with the phase abstracted liveness property125. In some exemplary embodiments, the model checker130is a BDD-based model checker, a SAT-solver based model checker or the like. The model checker130may be a third-party model checker that is not specifically configured to handle with phase abstracted models.

The computerized environment100may comprise a counter-example manipulation module140for modifying the original counter-example to a modified counter-example145. The modified counter-example145may exemplify a behavior of the original model105that does not comply with the original liveness property118, also referred to as a falsification of the original liveness property118.

In some exemplary embodiments of the disclosed subject matter, some of the aforementioned elements of the computerized system100may be coupled, such as for example the counter-example manipulation module140and the phase abstraction adapter120may be implemented by a single computerized device, such as software/firmware executed using Personal Computer (PC), a server, or other hardware, a specialized computerized hardware or the like.

Referring now toFIG. 2showing a phase abstraction adapter in accordance with some exemplary embodiments of the disclosed subject matter. A phase abstraction adapter200, such as120ofFIG. 1, may comprise a processor202. The processor202may be a Central Processing Unit (CPU), a microprocessor, an electronic circuit, an Integrated Circuit (IC) or the like. The processor202may be utilized to perform computations required by the phase abstraction adapter200or any of it subcomponents.

The phase abstraction adapter200may comprise an interface210. The interface210may be utilized to receive or otherwise obtain a phase abstracted model, an original liveness property or the like. The interface210may be an Application Programming Interface (API), a communication protocol, an input or output device or the like. The interface210may obtain information from a user220, a model checker230or a phase abstraction module (not shown), such as110ofFIG. 1, and the like. The interface210may further provide output interface to the phase abstraction adapter200enabling it to provide the user220, the model checker230or the like any determination, information, data, computation or the like produced by the phase abstraction adapter200.

The phase abstraction adapter200may comprise a property modifier240configured to transform an original liveness property to a phase abstracted liveness property. In some exemplary embodiments, the property modifier240may comprise a liveness gate identifier245configured to identify one or more unfolded gates in the phase abstracted model that are associated with the original liveness property. The one or more unfolded gates may be associated with a gate in the original model that is associated with the original liveness property.

In some exemplary embodiments, an original liveness property is refuted by exemplifying a behavior in which a value of a gate remains TRUE. The property modifier240may determine the phase abstracted liveness property to be a conjunction of the one or more unfolded gates in the phase abstracted model.

The phase abstraction adapter200may comprise a fairness property identification module250for identifying or otherwise determining an original fairness property. The fairness property identification module250may determine a definition in a model that defines a fairness property such as for example a fairness directive in PSL/Sugar specification language.

The phase abstraction adapter200may comprise a fairness modification module260for modifying or otherwise transforming the original fairness property to a phase abstracted fairness property. In some exemplary embodiments, the fairness modification module260may comprise a fairness gate identifier265configured to identify one or more unfolded gates in the phase abstracted model that are associated with the original fairness property. The one or more unfolded gates may be associated with a gate in the original model that is associated with the original fairness property.

In some exemplary embodiments, an original fairness property is held by having a predetermined gate be TRUE in at least one cycle in a repetitive portion of a counter-example. The fairness modification module260may determine the phase abstracted fairness property be a disjunction of one or more unfolded gates associated with the predetermined gate.

Referring now toFIG. 3showing a counter-example manipulation module, in accordance with some exemplary embodiments of the disclosed subject matter. A counter-example manipulation module300, such as140ofFIG. 1, may be configured to transform an original counter-example to a modified counter-example. The original counter-example may be produced or otherwise determined by a model checker in respect to the phase abstracted model and the phase abstracted liveness property. The modified counter-example may be associated with the original model and the original liveness property.

The counter-example manipulation module300may comprise an interface310, similar to210ofFIG. 2. The interface310may be utilized to receive or otherwise obtain the original counter-example, for example from a model checker. The interface310may be utilized to output the modified counter-example.

The counter-example manipulation module300may comprise an unfolding module320for determining a value of a gate in a cycle in the modified counter-example based on a value of a corresponding gate in corresponding cycle in the original counter-example. For example, the unfolding module320may determine the value of the gate in the original model the be the value of an unfolded gate in the phase abstracted model. The unfolding module320may perform an iterative process in which each a value of a gate is determined in each cycle to be the value of an unfolded gate. For example, in case a frame comprises four cycles, a value of a gate in cycle ten is set to a value of a third unfolded gate in the second cycle of the phase adapted model, as the second cycle of the phase adapted model represents cycles eight to eleven in the original model.

In some exemplary embodiments, the unfolding module320may truncate the modified counter-example such that the modified counter-example comprise a loop. The truncation may be performed on the last cycle in the original counter-example, such that only some of the cycles corresponding to the frame of the last cycle appear in the modified counter-example.

The counter-example manipulation module300may comprise an early loop determination module330. The early loop determination module330may determine a first cycle in the original model that is equal to a second cycle in the original model which corresponds to a beginning of a loop. The first cycle is earlier than the second cycle. The first cycle may be determined to be a beginning cycle of the loop in the modified counter-example, thereby providing a loop that begins in an earlier cycle.

The counter-example manipulation module300may comprise a short loop determination module340. The short loop determination module340may determine a first cycle in the original model such that a second cycle in the original model which corresponds to a beginning of a loop is successive to the first cycle. The first cycle may be determined to be an ending cycle of the modified counter-example, thereby providing a loop comprising fewer cycles.

The counter-example manipulation module300may comprise a state comparison module350that may compare a first cycle and a second cycle in the original model. The comparison may be based on the values in the original counter-example, and a determination of values of gates in the original model based on the value of unfolded gates in the phase abstracted model.

In some exemplary embodiments of the disclosed subject matter, a deterministic counter-example producer360may determine a deterministic counter-example based on an original counter-example which is non-deterministic. The deterministic counter-example producer360may determine a deterministic value for each gate having a non-deterministic value, such as by employing a satisfiability solver355or by selecting an arbitrary deterministic value.

In some exemplary embodiments of the disclosed subject matter, the state comparison module350may utilize the satisfiability solver355to determine if two states, of which at least one is non-deterministic, may represent a same state. The satisfiability solver355may be a Constraint Satisfaction Problem (CSP) solver, a Boolean satisfiability (SAT) solver, a theorem prover, a Quantified Boolean Formula (QBF) solver or the like.

Referring now toFIG. 4showing a flowchart diagram of a method to determine a phase abstracted property, in accordance with some exemplary embodiments of the disclosed subject matter.

In step400, a phase abstracted model is retrieved or otherwise obtained, using for example an interface such as210ofFIG. 2.

In step410, an original liveness property is retrieved or otherwise obtained, using for example an interface such as210ofFIG. 2.

In step420, a conjunction of relevant gates in the phase abstracted model is determined. The conjunction may be of unfolded gates relating to liveness gates in the original model. Liveness gates refer to one or more gates that are associated with a liveness property, such as the original liveness property. The conjunction may be used to determine and provide for a phase abstracted liveness property.

In step430, an original fairness property is determined, for example by a fairness property identification module250ofFIG. 2.

In step440, a disjunction of relevant gates in the phase abstraced model is determined. The disjunction may be of unfolded gates relating to fairness gates in the original model. Fairness gates refer to one or more gates that are associated with fairness property, such as the original fairness property. The disjunction may be used to determine and provide for a phase abstracted fairness property. In some exemplary embodiments, the phase abstracted model is modified to include the phase abstracted fairness property. In other exemplary embodiments, the phase abstracted fairness property is provided to a model checker using a specification language describing the specification.

Referring now toFIG. 5showing a flowchart diagram of a method to determine a modified counter-example, in accordance with some exemplary embodiments of the disclosed subject matter.

In step500, an original counter-example associated with a liveness property is retrieved or otherwise obtained, using for example an interface such as310ofFIG. 3. The original counter-example exemplifies a falsification of a phase abstracted liveness property by a phase abstracted model.

In step502, the original counter-example is unfolded to an unfolded counter-example. The unfolded counter-example is associated with the original model. Step502may be performed by an unfolding module such as320ofFIG. 3. In some exemplary embodiment, step502is performed by iterating over unfolded gates in the phase abstracted model associated with a gate in the original model and for each frame in the original counter-example copy the value of the M-th unfolded gate to the value of the gate at cycle M−1+I*K, where I is the frame and K is a number of cycles in a frame. Step502may produce an unfolded counter-example

In some exemplary embodiments, a deterministic counter-example is determined in step505based on the unfolded counter-example. A deterministic counter-example producer such as360ofFIG. 3may be utilized.

In step510, a repetitive portion of the original counter-example is identified. In some exemplary embodiments, the counter-example comprises a LOOP gate that is raised upon entering to the repetitive portion. A corresponding portion in the unfolded counter-example may be determined to be a repetitive portion.

In step515, a determination may be made as to which cycle should be the last cycle of the unfolded counter-example in order to ensure that a correct loop appears in the unfolded counter-example. In some exemplary embodiments, the last K cycles of the unfolded counter-example are examined, where K is a number of cycles in a frame. The last K cycles may be examined to determine which of the K states in the K cycles is a predecessor state of the first state of the repetitive portion of the unfolded counter-example. The determined predecessor state may be determined to be the last cycle of the unfolded counter-example. The cycles after the last cycle may be removed from the unfolded counter-example.

In step520, a determination may be made whether the repetitive portion may start in an earlier cycle in the unfolded counter example. Step520may be performed by an early loop determination module such as330ofFIG. 3. In some exemplary embodiments, some cycles before the repetitive portion are examined to determine if any of the some cycles is equal to the cycle beginning the repetitive portion. Alternatively, the some cycles may be examined to determine if they are the next state successive (according to the original model) to the state in the last cycle of the unfolded counter-example. If a cycle is identified, the unfolded counter-example may be modified such that the repetitive portion may begin in the cycle.

In step530, a determination may be made whether the repetitive portion of the unfolded counter example may consist less cycles. Step530may be performed by a short loop determination module such as340ofFIG. 3. In some exemplary embodiments, cycles of the repetitive portion may be examined to determine if a state in a first cycle is equal to the state in the ending cycle of the repetitive portion. Alternatively, a determination may be made whether the state beginning the repetitive portion is a next state successive to the state in the first cycle. If a first cycle is identified, the unfolded counter-example may be modified such that the repetitive portion may end in the first cycle.

In step540, the modified counter-example may be produced or otherwise determined based on the unfolded counter-example and the determination made in any of the previous steps.

In some exemplary embodiments of the disclosed subject matter, a satisfiability solver, such as a SAT solver, may be utilized to determine the modified counter-example. In an exemplary embodiment, any non-deterministic state in the unfolded counter-example is examined using the satisfiability solver to determine if it could represent a state in accordance with a cycle. The satisfiability solver may be utilized, for example, in steps520or530. In case the satisfiability solver determines that a satisfactory assignment exists, the satisfactory assignment may be utilized to determine deterministic values for the non-deterministic state. The satisfiability solver enables decreasing the size of the modified counter-example such that the repetitive portion begins in an early cycle or consists of a small number of cycles.