E-process design and assurance using model checking

Trust in e-commerce is difficult to establish and maintain. Almost daily, news headlines cover some incident, causing users to question e-commerce systems' trustworthiness. Strong e-process design and implementation is the first line of defense against errors, fraud and hacking. Minimizing program faults in business operations is critical for an e-business's survival. Carefully designed and implemented code can handle most expected situations, so these e-processes often function well within their defined boundaries, but guaranteeing correct processing under all circumstances is extremely difficult, if not impossible. Hidden flaws and errors, triggered only under unexpected, hard-to-anticipate scenarios, lead to subtle mistakes and even catastrophic failures. The authors use an online ticket sales example to illustrate the potential of model checking (an advanced formal method) for economically finding certain flaws. Model checking is a powerful verification method that determines whether a system model satisfies certain specifications under all circumstances. It can locate subtle but critical flaws that conventional design and assurance methods, such as testing and simulation, often miss