E-process design and assurance using model checking

Trust in e-commerce is difficult to establish and maintain. Almost daily, n ews headlines cover some incident, causing users to question e-commerce sys tems' trustworthiness. Strong e-process design and implementation is the first line of defense aga inst errors, fraud, and hacking. Minimizing program faults in business oper ations is critical for an e-business's survival. Carefully designed and imp lemented code can handle most expected situations, so these e-processes oft en function well within their defined boundaries. But guaranteeing correct processing under all circumstances is extremely difficult, if not impossibl e. Hidden flaws and errors, triggered only under unexpected, hard-to-antici pate 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 cert ain flaws. Model checking is a powerful verification method that determines whether a system model satisfies certain specifications under all circumst ances. It san locate subtle but critical flaws that conventional design and assurance methods, such as testing and simulation, often miss.