| The new yet ubiquitous Internet computing technology and consequently the blossoming of electronic commerce is changing the way markets and businesses operate. Digital processes have become the brains and nerves of an e-business and their proper function is crucial for the business' economic well-being. There is a growing need for rigorous methods to verify digital process design and implementation.; This dissertation suggests that due to the complexity and specialties of digital operations, the only viable approach for systematic control and assurance is to use rigorous mathematical and computational methods to represent and analyze operational systems. Traditional control and auditing methods, mostly based on manual verification, piece-meal analysis and post-audits, are useful but not sufficient. A set of methods is proposed: (1) Applying economic reasoning, such as mechanism design, to ensure that e-commerce market trading rules and business policies are incentive compatible and lead to the expected system outcome; (2) Applying the concept of atomic transaction to define system properties and specifications; (3) Applying modern formal verification techniques, such as model checking, to ensure the correctness of system design and implementation at the code level; and (4) Applying distributed computing agent technology, such as Java, to ensure the correctness of system operations in real execution. Different methods are applied in different phases of the System Development Life Cycle. However, these methods complement each other, refining system specifications and implementation and enhancing the relevance, completeness and reliability of control and assurance.; Suggested methods are demonstrated through examples. For instance, to deal with one of the weaknesses in online auction markets, i.e., the lack of authentication, a Sealed-bid Multi-round Auction Protocol (S-MAP) is introduced, which is not only robust against false-name bidding but also efficient. An online ticket-sales prototype is implemented and model checking is applied to verify its correctness. A model of a Real-time Assurance Monitor (RAM) is suggested to monitor system executions.; Auditors, as traditional trust providers for financial markets, have great potential to provide control and assurance services for electronic commerce, but they need to equip themselves with the new set of methods. |
