--%>
Assignment Help - homework help

Environment Modeling in Java Pathfinder

Environment Modeling: In JPF, Java class files can be processed in two different ways:

A) As ordinary Java classes managed and executed by the host JVM (e.g., standard Java library classes, JPF implementation classes)

B) As “modeled” classes managed and processed (verified) by JPF

We have to clearly distinguish between these two modes. In particular, JPF’s “Model” layer has its own class and object model, which is completely different than and incompatible with the hidden class and object models of the underlying host JVM executing JPF.

Each standard JVM supports a Java Native Interface (JNI), that is used to delegate execution from the JVM-controlled bytecode down into the platform-dependent native layer (machine code). This is normally used to interface certain functionalities such as I/O or graphics to the platform OS and architecture. JPF provides an analogous mechanism to lower the “execution” level in JPF from JPF-controlled bytecode into JVM-controlled bytecode. This mechanism is called Model Java Interface (MJI). It supports the creation of dedicated classes to be executed by the underlying JVM rather than JPF. Such classes are not model checked by JPF.

   Related Questions in Programming Languages

  • Q : Detecting sequence in signal line

    Explain how to detect a sequence of ‘1101’ arriving serially from the signal line?

    		•
  • Q : Explain the differences among SEI

    What in your advice are the most important fundamental differences among SEI SW-CMM and ISO 9000-3?

    		•
  • Q : What is Bandera Bandera: The main goal

    Bandera: The main goal of Bandera project is to integrate existing programming language processing methods with newly developed methods to provide automated support for the extraction of safe, compact, finite-state models which are suitable for verifi

    		•
  • Q : Write the benefits of DLR Write the

    Write the benefits of DLR?

    		•
  • 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 : Define Thread starvation Thread

    Thread starvation: It is a condition which applies to a thread which is prevented from running by other threads which do not yield or turn into blocked.

    		•
  • Q : Differentiate between RDO and ADO

    Differentiate between RDO and ADO?

    		•
  • Q : What is an Overriding for breadth

    Overriding for breadth: It is a form of method overriding in which the sub-class version of a technique implements its own behavior within the context of attributes and behavior of the sub-class and then calls the super-class version and hence it can

    		•
  • Q : Explain Cohesion Cohesion : The level

    Cohesion: The level to which a component executes a single well-stated task. A strongly cohesive technique, for example, will execute a single task, like adding an item to a data structure, or sorting several data, while a weakly cohesive technique wi

    		•
  • Q : What is Java What is Java: It is a

    What is Java: It is a portable high level programming language introduced by Sun Microsystems.

    		•