--%>
Assignment Help - homework help

Describe MCP or Model Checker for C plus

MCP: Model Checker for C++ (MCP) is an explicit-state software model checker being introduced by the Robust Software Engineering group at NASA Ames Research Center (Thompson and Brat, 2008). MCP was constructed specifically to allow programs written in C or C++ to be model-checked directly, devoid of requiring prior translation or model extraction. It builds upon the LLVM (low level virtual machine) compiler infrastructure (LLVM website), thereby avoiding the requirement to directly recognize the extremely complex C++ language at source-level. This approach allows MCP to support the entire C++ language, comprising templates. The C language is handled fully, not merely as an improper subset of C++. Experience from the JPF project has demonstrated the utility of program model checking. However, current flight software is mostly implemented in C, not Java, and in the future it seems increasingly likely that C++ will become the platform of choice. The MCP model checker was developed to fill the requirement for an explicit-state software model checker, in the style of JPF, that fully supports the C++ language. As a test example, it was applied to the unmodified C code of the prototype CEV Onboard Abort Executive Flight Rules Checker.

   Related Questions in Programming Languages

  • Q : Define PS3 Debug/TEST/Prototype

    Define PS3 Debug/TEST/Prototype Consoleroduction deployment.

    		•
  • Q : Define Stream class Stream class : An

    Stream class: An input stream class is one which delivers data from its source (frequently the file system as a series of bytes. Likewise, an output stream class will write byte-level data. The stream classes must be contrasted with the operation of r

    		•
  • Q : Pointer in C What is pointer? What

    What is pointer? What significance of pointer in C programming languages?

    		•
  • Q : What is an Implicit type conversion

    Implicit type conversion: The type conversion which does not need a cast. Implicit type conversions usually do not comprise any loss of information. For example, joining an integer operand with a floating point operand in an arithmetic expression will

    		•
  • Q : CORBA In what respects did CORBA seek

    In what respects did CORBA seek to improve on technologies such as SunRPC?

    		•
  • Q : "this" pointer is different from a

    		•
  • Q : Explain Switch statement Switch

    Switch statement: It is a selection statement in which the value of an arithmetic expression {expression!arithmetic} is compared for the match alongside different case labels. When no match is found, the optional default label is chosen For example:

    		•
  • Q : State the term Win32 State the term

    State the term Win32. Answer: Win32 considers to Microsoft 32 bit Windows API. Applications of Win32 are programs that are built along with the Win32 API.

    		•
  • Q : Explain Timesharing system Timesharing

    Timesharing system: It is an operating system which shares processor time among multiple processes by assigning each a time slice. Once a process's time slice has finished or expired, the other procedure is given a possibility to run.

    		•
  • Q : What is Unique Identifier and how do I

    What is Unique Identifier and how do I determine one?

    		•