Runtime Verification - History and Context

History and Context

The terminology runtime verification was formally introduced as the name of a 2001 workshop aimed at addressing problems at the boundary between formal verification and testing. Nevertheless, checking formally or informally specified properties against executing systems or programs is an old topic (notable examples are dynamic typing in software, or fail-safe devices or watchdog timers in hardware), whose precise roots are hard to identify. Currently, runtime verification techniques are often presented with various alternative names, such as runtime monitoring, runtime checking, runtime reflection, runtime analysis, dynamic analysis, runtime/dynamic symbolic analysis, trace analysis, log file analysis, etc., all referring to instances of the same high-level concept applied either to different areas or by scholars from different communities. Runtime verification is intimately related to other well-established areas, such as testing (particularly model-based testing) when used before deployment and fault-tolerant systems when used during deployment.

Within the broad area of runtime verification, one can distinguish several categories, such as:

  • "specification-less" monitoring that targets a fixed set of mostly concurrency-related properties such as atomicity. The pioneering work in this area is by Savage et al. with the Eraser algorithm
  • monitoring with respect to temporal logic specifications; early contributions in this direction has been made by Lee, Kannan, and their collaborators, and Havelund and Rosu,.

Read more about this topic:  Runtime Verification

Famous quotes containing the words history and, history and/or context:

    We aspire to be something more than stupid and timid chattels, pretending to read history and our Bibles, but desecrating every house and every day we breathe in.
    Henry David Thoreau (1817–1862)

    I believe that history has shape, order, and meaning; that exceptional men, as much as economic forces, produce change; and that passé abstractions like beauty, nobility, and greatness have a shifting but continuing validity.
    Camille Paglia (b. 1947)

    The hippie is the scion of surplus value. The dropout can only claim sanctity in a society which offers something to be dropped out of—career, ambition, conspicuous consumption. The effects of hippie sanctimony can only be felt in the context of others who plunder his lifestyle for what they find good or profitable, a process known as rip-off by the hippie, who will not see how savagely he has pillaged intricate and demanding civilizations for his own parodic lifestyle.
    Germaine Greer (b. 1939)