| Summary: | 碩士 === 國立暨南國際大學 === 資訊管理學系 === 91 === Among the increasingly widespread e-commerce protocols, RosettaNet is developed initially to support the specific electronic industry domain, especially for their vertical collaborative integration of the entire supply chain of electronic products. RosettaNet provides a complete and easy way to build a platform for electronic business document exchange. Similar to other communication protocols, RosettaNet is subject to protocol verification problems, like issues of liveness. However, there are neither research efforts devoted to these problem nor any solid results to resolve them. There are risks and difficulties incurred during the implementation of RosettaNet without any protocol verification scheme applied.
RosettaNet PIPs (Partner Interface Processes) are XML-based dialogs that are specially designed for system-to-system information exchange of business processes between trading partners. In each PIP specification, there define a business process with the choreography of the message dialog, and a business document with the vocabulary. Although, RosettaNet PIPs intend to provide open e-commerce standards for automated information excess and exchange across the boundaries of individual companies, some of their pilot implementations, however, faced fierce obstacles and difficulties. Most of them are caused by the inability to handle exceptional conditions. For instance, consider a situation when a buyer places a purchase order to a seller. The buyer first sends a business
document to the seller. Complying to the PIPs specifications, the seller side has to return an acknowledgement to the buyer side after receiving the purchase order. Assume that due to some
unexpected noises during data transferring, this message of
acknowledgement were lost. According to the PIPs, the buyer side
has to resend the business document to at most three times and
resume its state at being executing after then. One problem arises with the question whether the seller does receive the purchase order, but the buyer doesn't receive the confirmation of the purchase order. Such ambiguities impose difficulties and burdens on system testing activities.
This paper deals with the verification problem of RosettaNet. The PIPs Specifications are first modeled with time Petri nets. Time Petri nets allow an explicit modeling of concurrency and
parallelism and have been widely used in real-time system specification and verification. Behavioral specification models
can be automatically translated into a state transition graph,
from which properties such as deadlock and reachability become
explicit. The correctness of the time Petri nets models is then
verified to ensure the capability of deadlock-free, auto-repairing implementations of RosettaNet applications. Ideas of the deadlock detection mechanism to check the possible existence of an uncontrolled siphon are adopted. We then extend the models to complete the RosettaNet PIPs specifications at both the sender and receiver counterparts.
|
|---|
