--%>
Assignment Help - homework help

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 : State the term web service State the

    State the term web service?

    		•
  • Q : Main function of context switching What

    What is the main function of context switching?

    		•
  • Q : How much does Symbian Signed

    How much does Symbian Signed certification and testing cost? Answer: Test houses contain their own prices for Symbian Signed testing. So you can check that prices through searching over the internet.

    		•
  • Q : Write a recursive function intpower(base

    Write a recursive function intpower(base, exponent) that when invoked returns base^exponent. For example, intpower(3,4) = 3*3*3*3. Assume that the exponent is an integer greater than or equal to 1.

  • Q : Explain main quality of unsuitable life

    What are the main quality consequences of selecting an unsuitable life cycle model for a software project?

    		•
  • Q : What is Memory leak Memory leak : It is

    Memory leak: It is a situation in which memory which is no longer being employed has not been returned to the pool of free memory. The garbage collector is designed to return unreferenced objects to the free memory pool in order to shun memory leaks.<

    		•
  • Q : What is Stepwise refinement Stepwise

    Stepwise refinement: It is a divide and conquer approach to the programming, in which a complicated problem is recursively divided into smaller, sub-problems and more manageable. This approach to program design is frequently employed with structured p

    		•
  • Q : Define Fully evaluating operator Fully

    Fully evaluating operator: An operator which computes all of its arguments to generate an outcome. Standard arithmetic operators, like +, are totally evaluating. In contrary, some Boolean operators, like &&, are short-circuit operators.

    		•
  • Q : What is Avoid Redundancy Avoid

    Avoid Redundancy: While not every form of redundancy is as bad from a verification perspective as it is from a maintenance point of view, behavioral redundancy to re-create (local) state can impose problems because the model checker does not distingui

    		•
  • Q : Explain If statement If statement : A

    If statement: A control structure employed to select between performing or not performing additional actions.     if(boolean-expression){        // Statements

    		•