Runtime Verification of Distributed Programs

Runtime Verification of Distributed Programs

Eslam Al Maghayreh (Yarmouk University, Jordan)
DOI: 10.4018/978-1-4666-0089-8.ch003
OnDemand PDF Download:
$30.00
List Price: $37.50

Abstract

Ensuring the correctness of a distributed program is not an easy task. Testing and formal methods can play a significant role in this regard. However, testing does not allow for formal specification of the properties to be checked. On the other hand, formal methods verify that a model of a distributed system satisfies certain properties that are formally specified. However, formal methods do not guarantee that a particular implementation of the system under consideration will also satisfy all of the necessary properties. Runtime verification tries to combine some of the advantages of testing and some of the advantages of formal methods. Runtime verification works on a particular implementation of the system and at the same time it allows us to specify the properties of interest formally. In this chapter we have talked about runtime verification of distributed programs. The main components of a runtime verification framework have been presented and discussed in some details. The reasons that make runtime verification of distributed programs a difficult task have been discussed. A summarization of some of the techniques presented in the literature to simplify runtime verification of distributed programs has also been presented.
Chapter Preview
Top

Introduction

Runtime verification is a technique that combines formal verification and traditional testing. The main components of a runtime verification framework are shown in Figure 1. The observed behavior (in terms of log traces) of a program can be monitored and verified dynamically to make sure that given requirements (properties) are satisfied. Such requirements are typically specified by a formalism which can express temporal constraints, such as LTL-formulae (Linear Temporal Logic).

Figure 1.

The main components of a runtime verification framework

Testing is an ad hoc technique that does not allow for formal specification and verification of the properties that the program needs to satisfy. Formal methods work on an abstract model of the program. Consequently, even if a program has been formally verified, we still cannot be sure of the correctness of a particular implementation. However, for highly dependable systems, it is important to analyze the particular implementation.

Runtime verification is more practical than other verification methods such as model checking and testing. Runtime verification verifies the implementation of the system directly rather than verifying a model of the system as done in model checking. It is also based on formal logics and provides formalism, which is lacked in testing. Figure 2 demonstrates that runtime verification combines the benefits of traditional testing techniques and formal method.

Figure 2.

Runtime verification combines the advantages of formal methods and traditional testing

In the literature, the following four reasons were mentioned in order to argue for runtime verification:

  • 1.

    If you check the model of your system you cannot be confident on the implementation since correctness of the model does not imply correctness of the implementation.

  • 2.

    Some information is available only at runtime or is convenient to be checked at runtime.

  • 3.

    Behavior may depend heavily on the environment of the target system; then it is not possible to obtain the information necessary to test the system.

  • 4.

    Runtime verification allows for formal specification and verification or testing of the properties that a system has to satisfy. Traditional testing techniques such as unit testing are ad hoc and informal. It is only a partial proof of correctness in that it does not guarantee that the system will operate as expected under untested inputs.

In terms of its ability to guarantee software correctness, runtime verification is weaker than formal methods but stronger than testing. Testing can only guarantee the correctness of a limited set of inputs at implementation time. As a result, undiscovered faults may result in failures at runtime. Formal methods are stronger than runtime verification but are hard to be understood and applied properly by software engineers, for this reason runtime verification are sometimes referred to as light weight formal methods and hence it has a better chance of being accepted and used by software engineers.

Distributed programs are particularly vulnerable to software faults. These programs often contain bugs, which are very difficult to detect without automatic verification. Verification of distributed programs and software fault-tolerance are important ways to ensure the reliability of distributed systems. Detecting a fault in an execution of a distributed system is a fundamental problem that arises during the verification process. A programmer upon observing a certain distributed computation for bugs can check whether the observed computation satisfies some expected property. The idea of checking whether a distributed program run satisfies an expected property (also referred to as runtime verification) has recently been attracting a lot of attention for analyzing execution traces.

Complete Chapter List

Search this Book:
Reset