--%>

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 : What is a Real-Time System What is a

    What is a Real-Time System?

  • Q : State the term INODE State the term

    State the term INODE. Answer: It is a pointer to a block upon the disk and is a unique number. This holds metadata of files.

  • Q : State the term Standard Generalized

    State the term Standard Generalized Markup Language?

  • Q : What is BLAST in program model checking

    What is BLAST in program model checking: The abbreviation is Berkeley Lazy Abstraction Software Verification Tool (BLAST) is a software model checker for C programs. The main goal of BLAST (BLAST website) is to be able to check that software satisfies

  • Q : Write a program using simple loop

    Objective:  The purpose of this problem is to gain experience with the principles necessary to write a program using simple loop, decision processing, counters and accumulators Save the Barns, a bi-partisan po

  • Q : Explain Abstraction Abstraction : It is

    Abstraction: It is a simplified symbolization of something which is potentially quite complex. It is frequently not essential to know the precise details of how something works, is symbolized or is implemented, since we can still make use of it in its

  • Q : What is Pattern Pattern : It is a

    Pattern: It is a recurring theme in class usage or design. Interfaces like Iterator encapsulate a pattern of admission to the items in a collection, whereas freeing the client from the requirement to know details of the way in which the collection is

  • 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 an Instantiation What is an

    What is an Instantiation: It is a creation of an instance of a class, i.e., an object.

  • Q : What are the uses of microcontroller

    What are the uses of microcontroller?