--%>

Reducing state space of code

What is the way to reduce the state space of the code during model checking?

E

Expert

Verified

One way to dramatically reduce the state space of this code during model checking is to:

A) Replace the time variables with non-deterministic choices (e.g., a simple integer whose value can becontrolled by the model checker and possibly kept to a restricted range), and

B) ?Replace all time comparisons with a simple non-deterministic Boolean choice.

The problem with doing this across the entire program is that it may involve modifications to many parts of the code—everywhere the corresponding variable has been used or referenced. This is a time-consuming task for realistic systems and is error-prone.

   Related Questions in Programming Languages

  • Q : Define Iteration Iteration : The

    Iteration: The repetition of a set of statements, generally employing a looping control structure, like a while loop, for loop and do loop.

  • Q : What is Quotient Quotient: Whenever

    Quotient: Whenever integer division is executed, the outcome comprises of a quotient and a remainder. The quotient symbolizes the integer number of times which the divisor divides into the dividend. For example, in 5/3, 5 is the dividend and 3 is the

  • Q : Define the term Internet Define the

    Define the term Internet: It is a global network of numerous interconnected networks.

  • Q : Explain Operator Explain Operator with

    Explain Operator with their types and examples?

  • Q : Define Property Specifications Property

    Property Specifications: Users can specify assertions using the assert(expr) statements. An assert statement is used to check if the property specified by the expression expr is valid within a state. If expr evaluates to 0, this implies that it is not

  • Q : What do you mean by Class variable What

    What do you mean by Class variable: It is a synonym for the static variable.

  • Q : What is Shallow copy Shallow copy : It

    Shallow copy: It is a copy of an object in which copies of each and every object's sub-components are not as well made. For example, a shallow copy of an array of objects would outcome in two separate array objects, each having references to similar s

  • Q : Problem on Gaussian Matlab function

    Solve the system Ax = b, with using the given Matlab function gauss (it cal

  • Q : What is an Argument Argument : It is

    Argument: It is the information passed to a method. Arguments are as well sometimes termed as parameters. The method expecting to receive arguments should contain a formal argument declaration for each as portion of its method header. Whenever a metho

  • Q : Scalability aspects of a Java PathFinder

    Scalability of program model checkers such as JPF encompasses two aspects: How large a program can be model checked, and Once a defect has been detected, how readily meaningful debugging informati