Verification of Communication Protocols in Web Services: Model-Checking Service Compositions

CHAPTER 5

MEMORY-EFFICIENT STATE-SPACE ANALYSIS IN SOFTWARE MODEL CHECKING

Formal methods have an unprecedented ability to endorse the correctness of a system. Despite that, they have been limited to safety- and mission-critical systems, owing to the significant time and memory costs involved. Our ever-increasing dependency on software in many aspects of life has necessitated the use of formal methods for a wider range of software. In this chapter we present two techniques to reduce the memory requirement of model checking, a widely used formal method. To ensure termination a model checker stores in memory all states explored. The techniques presented slash memory costs by storing a state according to how different it is from one of its neighboring states. Our experiments report a memory reduction of 95% while only doubling the computation delay. This reduction allows model checking in a machine with only a fraction of the memory required otherwise. Consequently, the advantage is twofold: (1) the savings substantial are, as a smaller physical memory suffices; and (2) as more states can now be stored in a memory of the same size, the chances of accomplishing complete state-space analysis are considerably higher.

5.1 MOTIVATION

Traditionally, software is considered “fail-safe” if it has passed a rigorous testing phase [1]. However, the crash of the Ariane 5 launcher [5] and the deaths due to malfunctioning of the Therac-25 radiation therapy machine [18], despite rigorous software ...