--%>
Assignment Help - homework help

Define the term Data Abstraction

Data Abstraction: Our presentation for data abstraction follows the abstract interpretation framework (Cousot and Cousot 1999). Abstract interpretation establishes a rigorous methodology for building data abstractions that are weakly preserving with respect to safety properties. In this framework, an abstraction maps the set of values of a program data type to an abstract domain and it maps the operations on that data type to functions over abstract values. Thus, the abstract program has a non-standard execution. Typically, the behaviors of the abstracted program are an over-approximation of the behaviors of the original program; each executable behavior in the original program is “covered” by a behavior in the abstract program. Thus, the abstraction is weakly preserving. When the abstract behaviors are checked with a model checker against a safety property (or a property written in LTL) and found to be in conformance, we can be sure that the true executable behaviors of the unabstracted program satisfy the property.

   Related Questions in Science

  • Q : Define Black-Box Testing Black-Box

    Black-Box Testing: Black-box testing assumes an external perspective of the system under test (SUT). It uses concrete input test data to obtain results from the SUT, which are then checked against some oracle. Usually, the oracle uses functional prope

    		•
  • Q : Safety Properties-Software lifecycle

    Safety Properties: This property asserts that nothing bad will happen during the execution of the program (e.g., no deadlocks, or no attempts to take an item from an empty buffer). Safety properties are used mainly

    		•
  • Q : Benefits to Boeing Case Study Building

    Building the Boeing 787 Boeing's newest commercial jet aircraft, the wide-bodied 787 jet, is a bold bet on the future of both airline travel a

    		•
  • Q : Define Model Extraction Model

    Model Extraction: Several program model checkers are based on automated model extraction, where program is translated into an input notation of an existing model checker (Corbett 1998; Havelund and Pressburger 2000; Corbett et al. 2000; Ball et al. 20

    		•
  • Q : Hot Keys for bash shell Normal 0 false

    Normal 0 false false

  • Q : Define Design pattern Design pattern :

    Design pattern: It is a general reusable solution to a normally occurring problem in software design. A design pattern is not finished design which can be transformed directly into code. It is explanation or template for how to solve out a problem whi

    		•
  • Q : Recover Plex from disabled state Normal

    Normal 0 false false

  • Q : Instance of microkernel Normal 0 false

    Normal 0 false false

  • Q : Obtain microseconds of system time from

    Normal 0 false false

  • Q : EAS309 Lab Assignment Note that this is

    Note that this is a formal report. The report is to evaluate the flight stability and control characteristics, and evaluate its compliance against the MIL-F-8785C specification. Whether the aircraft design FAIL or PASS, it is NOT important.

    		•