O'Reilly logo

Verification of Communication Protocols in Web Services: Model-Checking Service Compositions by Peter Bertok, Zahir Tari, Kazi Sakib

Stay ahead with the world's most comprehensive technology and business learning platform.

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, tutorials, and more.

Start Free Trial

No credit card required

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 ...

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, interactive tutorials, and more.

Start Free Trial

No credit card required