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

CHAPTER 2

MODEL CHECKING

It has been observed [18] that the industry average (1) is 15 to 50 errors per 1000 lines of code delivered, (2) is about 10 to 20 defects per 1000 lines of code in Microsoft applications, and that (3) formal development methods, peer reviews, and statistical testing have helped to reduce this to zero per 500,000 lines of code.

The world has recognized the advantages of using the proper software for a particular need. This is almost as important as using the proper hardware. For example, video-streaming software might significantly inflate the broadband bill unless the correct compression technology is used. Consequently, a significant amount of time is spent in testing software prior to releasing it. Based on the magnitude of failures and their consequences, this might involve a massive cost.

Software engineering is different from other engineering disciplines because the product envisioned has no physical existence. It needs appropriate hardware to exhibit its presence and abilities. Furthermore, it was observed in 1997 that (1) software systems are discontinuous compared to physical systems, which are continuous, and (2) modern systems require that most functionalities be provided by software, thereby increasing their complexity. Continuous systems exhibit smooth changes in output in response to a smooth change in input, whereas the output for a discontinuous system can change significantly even for a small change in input.

In recent years, the software ...