Model checking for design and assurance of e-Business processes

Use of the Internet for electronic business has the potential to revolutionize the way many businesses are conducted. Yet, several businesses have fallen victim to problems in information systems that facilitate e-Business. These problems are characterized by uncertainties due to system complexity, rapid development, interconnectivity, and a lack of familiarity with the new technologically based economy. This paper demonstrates how model checking can aid in the design and assurance of e-Business processes in environments characterized by distributed processing, parallelism, concurrency, communication uncertainties, and continuous operations.