Runtime Verification of Distributed Programs

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.