1、Model checking is a promising technique for the verication of complex software systems. As the use of the Internet for conducting e-business extends the reach of many organizations, well-designed software becomes the foundation of reliable implementation of e-business processes.These distributed, el
2、ectronic methods of conducting transactions place reliance on the control structures embedded in the transaction processes.Deciencies in control structures of processes that support e-business can lead to loss of physical assets, digital assets, money, and consumer condence. Yet, assessing the relia
3、bility of e-business processes is complex andtime-consuming.This paper explicates how model-checking technology can aid in the design and assurance of e-business processes in complex digital environments. Specically, we demonstrate how model checking can be used to verify e-business requirements con
4、cerning money atomicity, goods atomicity, valid receipt, and communication-link failure. These requirements are fundamental to many e-business applications.Model checking can be used to test a broad range of systems requirementsnot only for system designers, but also for auditors and security specia
5、lists. Systems that are examined by auditors need to have adequate controls built in prior to implementation and will need adequate auditing after implementation to ensure that none of the processes have been corrupted. Model checkers may also provide value in examining the processes of highly integ
6、rated applications as found in enterprise resource planning systems.Index Terms：Atomicity, data typing, e-Business, model checking,process and communication protocols.I. INTRODUCTIONInternet-based business operations offer considerable potential, but they are accompanied by a broad range of often un
7、precedented risks.An actual or perceived lack of system security and reliability can signicantly constrain the growth of the digital economy. While progress is being made in reducing Internet computational risks through a variety of software patches and cryptographic algorithms, these efforts addres
8、s only a small portion of the larger challenge of establishing thenecessary security and reliability of e-business systems. To resolve this challenge, systematic management of the associated operational risks is essential 1.According to Wang et al. 2, management of operational risks requires careful
9、 examination of the e-business infrastructure. Distributed Internet computing is changing e-market structures and e-business models in fundamental ways. Although the exibility of distributed e-operations supports open accessibility and dynamic interactions,exibility can intensify problems arising fr
10、om e-market information asymmetry and e-business operational uncertainty. These problems militate against innovative e-commerce developments. Although e-commerce offers the opportunity for businesses to gain efciency and effectiveness through network-based ad-hoc partnerships, many businesses do not
11、 take advantage of these opportunities because of the heightened risks of operational uncertainty and perceived information asymmetry among unfamiliar business partners.Manuscript received November 18, 2003; revised May 17, 2004. This paper was recommended by Associate Editor S. Lakshmivarahan.The a
12、uthors are with the Marriott School of Management andKevin and Debra Rollins Center for e-Business, Brigham YoungUniversity, Provo, UT 84602 USA （e-mail: Bonnie_AndersonBYU.edu;James_HansenBYU.edu, Paul_LowryBYU.edu; Scott_SummersBYU.edu）.Digital Object Identier 10.1109/TSMCC.2004.843181 These issue
13、s take on added importance as new business models and architecturessuch as Internet auctions, web services 3 and the semantic web 4offer broad support for loosely coupled, e-commerce transactions where buyers and sellers may not have any prior trading experience with one another. For example, the we
14、b services 3 platform provides the Universal Description, Discovery and Integration （UDDI） registry for discovery of e-commerce services, WSDL for service description, and SOAP for transaction execution. These facilities require no prior knowledge of buyer and seller by either party.In such environm
15、ents, merchants and customers may be reluctant to trust one another and the following situations may arise: A customer is unwilling to pay for a product without being certain the correct product will be sent. A merchant is unwilling to send a product without certainty of receiving payment. If a merc
16、hant delivers the product without receiving payment, a fraudulent customer may receive the product and then disappear, with a resulting loss to the merchant. If a customer pays before receiving the product, a merchant may not deliver or may deliver a wrong product. These possibilities underscore the
17、 need for carefully designed e-commerce models that are robust under all events.As Wang et al. 5 note, e-system complexity and human limitations make it impossible to imagine all scenarios and guarantee correct processing under all circumstanceseven for carefully designed and implemented code. Much
18、of this difculty is due to interconnectivity, which widens the potential range of error or vulnerability. Variation in execution of concurrent processes in nonstop, nondeterministic systems increases the potential for automation failures. Consequently mini mizing aws in transaction protocols is cruc
19、ial for the survival and sustainability of e-business. Stakeholders, such as system designers,users, and auditors need methods to preclude these subtle but potentially critical mistakesbefore erroneous processing occurs or an attacker exploits themto enhance control and assurance to e-commerce users
20、. Model checking offers a promising method for addressing these issues.II. MODEL CHECKING FUNDAMENTALSAutomation failures occur when an automated system behaves differently than its stakeholders expect. If the actual system behavior and the stakeholders model are both described as nite state transit
21、ion systems, then mechanized techniques known as model checking can be used to automatically discover any scenarios that cause the behaviors of the two descriptions to diverge from one another. These scenarios identify potential failures and pinpoint areas where design changes or revisions should be
22、 consideredModel checking can trace through all relevant states with respect to any given requirement. Since model checking operates on logic rather than individual execution paths, verication can be more thorough and efcient than test runs and simulation. Some of the most compelling features of mod
23、el checkers are summarized as follows 6.1） They help delimit a systems boundary or the interface between the system and its environment.2） They precisely dene a systems desired properties.3） They characterize a systems behavior more accurately. Most current methods focus on functional behavior only
24、（e.g., “What is the correct answer?”） but some can handle real-time behavior as well （e.g., “Is the correct answer delivered on time?”）.4） They can aid in proving that a system meets required specications. By providing counterexamples that show how specications are not satised, model checkers can pi
25、npoint the circumstances under which a system does not meet its specications.This can also help to correct the system.These features of model checkers aid stakeholders in two important ways.1） Through specication, by focusing a system designers attention to crucial questions, such as: What is the in
26、terface? What are the assumptions about the applications environment? What is the system supposed to do under this condition or that condition?What happens if that condition is not met? What are the systems invariant properties?2） Through verication, by providing additional assurance. Relying on pro
27、of that a system meets its security goals is better than relying on opinioneven expert opinion.It should be emphasized that any proof of correctness is relative to both the formal specication of a system and the formal specication of the desired properties: a system proven correct with respect to an
28、 incorrect specication leaves no assurance about the system at all.The process of proving entails three actions: First, the system of interest must be modeled. A mathematical model is constructed that expresses the semantic structure of an e-business implementation.Second, all properties to be guara
29、nteed in the implementation are formally specied. In an e-business context, one such specication might be that goods must always be received before payment is initiated.Third, a proof is provided. Typically, a proof relies on induction over traces of the e-commerce communication and transaction oper
30、ations.In general, verifying that any e-business process is resilient to hidden aws and errors is a daunting task. Manual methods are slow and error prone. Even theorem provers, which provide a formal structure for verifying standard characteristics, may require human intervention and can be time-co
31、nsuming. Moreover, even if a failure is found using a theorem prover, it may provide little help in locating the source of thefailure 2. Simulations offer computational power, but they are ad hoc in nature and there is no guarantee they will explore all important contingencies 2.In contrast, model c
32、hecking is an evolving technology that can provide effective and efcient evaluation of e-business processes. Model checking was originally developed for validating highly complex integrated circuits and software packages 7, 8, but it has recently been adopted to tackle the complexity of e-commerce transactions 9,2, 10. Current model-checking technology is based on automated techniques that a
