当前位置:首页 >> >>

Eighth Workshop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools


ISSN 0105-8517

Eighth Workshop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools
Aarhus, Denmark, October 22-24, 2007

Kurt Jensen (Ed.)

DAIMI PB - 584 October 2007

DEPARTMENT OF COMPUTER SCIENCE UNIVERSITY OF AARHUS
IT-parken, Aabogade 34 DK-8200 Aarhus N, Denmark

Preface
This booklet contains the proceedings of the Eighth Workshop on Practical Use of Coloured Petri Nets and the CPN Tools, October 22-24, 2007. The workshop is organised by the CPN group at Department of Computer Science, University of Aarhus, Denmark. The papers are also available in electronic form via the web pages: http://www.daimi.au.dk/CPnets/workshop07/ Coloured Petri Nets and the CPN Tools are now licensed to more than 5.600 users in 129 countries. The aim of the workshop is to bring together some of the users and in this way provide a forum for those who are interested in the practical use of Coloured Petri Nets and their tools. The submitted papers were evaluated by a programme committee with the following members: Wil van der Aalst, Netherlands Jo?o Paulo Barros, Protugal Jonathan Billington, Australia J?rg Desel, Germany Joao M. Fernandes, Portugal Jorge de Figueiredo, Brazil Monika Heiner, Germany Thomas Hildebrandt, Denmark Kurt Jensen, Denmark (chair) Ekkart Kindler, Denmark Lars M. Kristensen, Denmark Johan Lilius, Finland Daniel Moldt, Germany Laure Petrucci, France Rüdiger Valk, Germany Lee Wagenhals, USA Jianli Xu, Finland Karsten Wolf, Germany The programme committee has accepted 13 papers for presentation. Most of these deal with different projects in which Coloured Petri Nets and their tools have been put to practical use – often in an industrial setting. The remaining papers deal with different extensions of tools and methodology. The papers from the first seven CPN Workshops can be found via the web pages: http://www.daimi.au.dk/CPnets/. After an additional round of reviewing and revision, some of the papers have also been published as special sections in the International Journal on Software Tools for Technology Transfer (STTT). For more information see: http://sttt.cs.uni-dortmund.de/ Kurt Jensen

Table of Contents
Invited Tutorials:
Lars M. Kristensen and Michael Westergaard The ASCoVeCo State Space Analysis Platform: Next Generation Tool Support for State Space Analysis............................................................................... 1 Ekkart Kindler Component Tools: A Frontend for Formal Methods ................................................. 7

Regular Papers:
Paul Fleischer and Lars M. Kristensen Towards Formal Specification and Validation of Secure Connection Establishment in a Generic Access Network Scenario .............................................. 9 E. Bacarin, W.M.P van der Aalst, E. Madeira, and C. B. Medeiros Towards Modeling and Simulating a Multi-party Negotiation Protocol with Colored Petri Nets.................................................................................................... 29 Jonathan Billington and Amar Kumar Gupta Effectiveness of Coloured Petri nets for Modelling and Analysing the Contract Net Protocol .............................................................................................. 49 Carmen Bratosin, Wil van der Aalst, and Natalia Sidorova Modeling Grid Workflows with Colored Petri Nets................................................ 67 Karolina Zurowska and Ralph Deters Overcoming Failures in Composite Web Services by Analysing Colored Petri Nets .......................................................................................................................... 87 Nick Russel1, Arthur H.M. ter Hofstede and Wil M.P. van der Aalst newYAWL: Specifying a Workflow Reference Language using Coloured Petri Nets................................................................................................................ 107 Kristian Bisgaard Lassen and Simon Tjell Translating Colored Control Flow Nets into Readable Java via Annotated Java Workflow Nets............................................................................................... 127 Visar Januzaj CPNunf: A tool for McMillan’s Unfolding of Coloured Petri Nets ...................... 147 Christine Choppy, Laure Petrucci, and Gianna Reggio Designing coloured Petri net models: a method .................................................... 167 R.S. Mans, W.M.P. van der Aalst, P.J.M. Bakker, A.J. Moleman, K.B. Lassen and J.B. J?rgensen From Requirements via Colored Workflow Nets to an Implementation in Several Workflow Systems.................................................................................... 187 J?ao M. Fernandes, Simon Tjell, and Jens B?k J?rgensen Requirements Engineering for Reactive Systems with Coloured Petri Nets: the Gas Pump Controller Example?....................................................................... 207 ?scar R. Ribeiro and J?ao M. Fernandes On the Use of Coloured Petri Nets for Visual Animation ..................................... 223 Kristian L. Espensen, Mads K. Kjeldsen, and Lars M. Kristensen Towards Modelling and Validation of the DYMO Routing Protocol for Mobile Ad-hoc Networks ...................................................................................... 243

The ASCoVeCo State Space Analysis Platform: Next Generation Tool Support for State Space Analysis?
Invited Tutorial

Lars M. Kristensen and Michael Westergaard
Department of Computer Science, University of Aarhus, IT-parken, Aabogade 34, DK-8200 Aarhus N, Denmark, Email: {kris,mw}@daimi.au.dk

Extended Abstract State space analysis is one of the main approaches to model-based veri?cation of concurrent systems and is one of the most successfully applied analysis methods for Coloured Petri Nets (CP-nets or CPNs) [13, 16, 17]. The basic idea of state space exploration and analysis is to compute all reachable states and state changes of the concurrent system under consideration and represent these as a directed graph. From a constructed state space it is possible to verify and analyse a large class of behavioural properties by considering, e.g., the standard behavioural properties of CP-nets, traverse a constructed state space by means of user-de?ned queries, or conduct LTL and CTL model checking [4, 10]. Another main advantage of state space analysis is that it can be supported by computer tools in a highly automatic way, and it can provide counter examples demonstrating why the system does not have a certain property. The main limitation of using state spaces to verify behavioural properties of systems is the state explosion problem [24], i.e., that state spaces of systems may have an astronomical number of reachable states which means that they are too large to be handled with the available computing power (CPU speed and memory). Methods for alleviating this inherent complexity problem is an active area of research and has led to the development of a large collection of state space reduction methods . These methods have signi?cantly broadened the class of systems that can be veri?ed and state spaces can now be used to verify systems of industrial size. Some of these methods [2, 15, 14, 25] have been developed in the context of the CPN modelling language. Other methods (e.g., [23, 22, 26, 11]) have been developed outside the context of the CPN modelling language, but state space reduction methods are generally independent of any concrete modelling language and hence also applicable for CP-nets. A computer tool supporting state spaces must implement a wide range of state space reduction methods since no single reduction method works well on all systems. Both CPN Tools [5] and its predecessor Design/CPN [6] have supported state space analysis in it most basic form and experimental prototype libraries have been developed supporting state space reduction methods such as the symmetry method [15, 18], the equivalence method [14, 19], time condensed state spaces [3], and the sweep-line method [2, 21]. The software architectures of CPN Tools and Design/CPN have, however, made it di?cult to support a collection of state space reduction methods in a coherent manner in these tools. This tutorial presents the ASCoVeCo State Space Analysis Platform (ASAP) which is currently being developed in the context of the ASCoVeCo research project [1]. ASAP represents the next generation of tool support for state space exploration and analysis of CPN
?

Supported by the Danish Research Council for Technology and Production.

1

models. The aim and vision of ASAP is to provide an open platform suited for research, educational, and industrial use of state space exploration. This means that the ASAP will support a wide collection of state space exploration methods and have an architecture that allows the research community to extend the set of supported methods. Furthermore, ASAP will be su?ciently mature to be used for educational purposes, including teaching of advanced state space methods, as well as su?ciently mature to be used in industrial projects as has been the case with CPN Tools and Design/CPN. ASAP is a stand-alone tool and is able to load models created with CPN Tools. ASAP will be available for Windows XP/Vista, Linux, and Mac OS X. The ASAP platform consists of a graphical user interface (GUI) and a state space exploration engine (SSE engine). Figure 1(left) shows the software architecture of the graphical user interface which is implemented in Java based on the Eclipse Rich Client Platform (RCP) [9]. The software architecture of the SSE engine is shown in Fig. 1(right). It is based on Standard ML (SML) and relies on the CPN simulator used in CPN Tools. The SSE engine implements the state space Exploration and model checking algorithms supported by ASAP. The state space exploration and model checking algorithms implemented rely on a set of Storage and Waiting Set components for e?cient storage and exploration of state spaces. Furthermore, the SSE engine implements the Query Languages(s) used for writing state space queries and to verify properties.

l

l

r

r

r

d

e

d

e

r

t o

l

e

t o

c

J

o

b

E

x

e

c

u

t

i

o

n a

i

M

o

d

e

M

o

d

u

t

p e

L

a

n

g

u

a

g

e

n

a

N

N

h

e

s

t

a

L o c

s P P

E

d

i

t

o

r

S

I

n

C

C

I

n

J

o

b

E

x

e

c

u

t

i

o

n

C

P

N

M

o

d

e

l

r E x p l o

a

t

i o

n

(

s

)

L

a

n

g

u

a

g

e

R

e

p

r

e

s

e

n

t

a

t

i

o

n

G

r

a

p

h

i

c

a

l

)

)

E

c

l

i

p

s

e

M

o

d

e

l

l

i

n

g

F

r

a

m

e

w

o

r

k

)

M

o

d

e

l

l

i

n

g

(

s

(

s

r

(

s

F

r

a

m

e

w

o

r

k

g

?

y

l )

e g

r

t

o e g

d

e

(

s

i

n

t

t

e u

a u

i

l

a

u

r

a M o Q g

S

e

W

a

t o

E

c

l

i

p

s

e

R

i

c

h

C

l

i

e

n

t

P

l

a

t

f

o

r

m

S n

i

m

S

L

a

S J a v a

t

a

n

d

a

r

d

M

L

Fig. 1. ASAP platform architecture: GUI (left) and SSE engine (right).

The ASAP GUI makes it possible to create and manage veri?cation projects consisting of a collection of veri?cation jobs . The GUI has three di?erent perspectives for working with veri?cation projects: – An editing perspective for creating and editing veri?cation jobs. – An execution perspective for controlling the execution of veri?cation jobs. – An inspection perspective for inspecting and interpreting analysis results. Veri?cation jobs are constructed and speci?ed using the veri?cation Job Execution Language (JEL) and the JEL Editor. JEL is a graphical language inspired by data-?ow diagrams that

2

makes it possible to specify the CPN models, queries, state space explorations, and processing of analysis results that constitute a veri?cation job. JEL and the JEL Editor are implemented using the Eclipse Modelling Framework (EMF) [8] and the Graphical Modelling Language [7] (GMF). The ASAP GUI additionally has a Model Loader component and a Model Instantiation component that can load and instantiate CPN models created with CPN Tools. Hence, models created using CPN Tools can be used directly with ASAP and since ASAP relies on the same underlying CPN simulator as CPN Tools, there is no CPN semantical gap between the two tools. It is worth noticing that it is only the CPN Model Loader, CPN Model Instantiator, and CPN Model Representation components that are speci?c to CPN models. The other components are independent of the CPN modelling formalism. Figure 2 shows a snapshot of the graphical user interface in the editing perspective. The user interface consists of three main parts apart from the usual menus and tool-bars at the top.

Fig. 2. Snapshot of the graphical user interface – editing perspective.

To the left is an overview of the veri?cation projects loaded, in this case just a single project named Demo is loaded. A veri?cation project consists of a number of veri?cation jobs, models, and queries. In this case there are three veri?cation job all concerned with checking

3

deadlock properties. A CPN model named erdp is loaded, which is a CPN model of an edge router discovery protocol [20]. At the bottom of the user interface is a console, which makes it possible to interact directly with the SSE engine using SML. This makes it easy to experiment with the tool and to issue queries that need not be stored as part of the veri?cation project. The large area at the top-right is the editing area. The editing area can be used to edit queries and veri?cation jobs. In this case two jobs are being edited and the two windows shows the graphical representation in JEL of the parts being edited. ASAP has an interface to the CPN simulator providing a set of primitives that makes it easy to access the transition relation of the CPN model and thereby augment the platform with new state space exploration and model checking algorithms. The primitives available is speci?ed by the MODEL SIMULATOR SML signature (interface) listed in Fig. 3. The signature deals with states and events (ll. 3–4). It is possible to get the initial states of the model (l. 9). Each state is represented as the actual state and all enabled events in that state. In order to accommodate non-deterministic formalisms, we allow a number of initial states, so a list of states is returned instead of just a single state. From a state and an event, it is possible to get (all) successor states (l. 12), and from a state and a sequence (list) of events, it is possible to get (all) states that are the result of executing the sequence of events from the speci?ed state (l. 16). If a user tries to execute an event that is not enabled, the EventNotEnabled exception (l. 6) is raised in both nextStates and executeSequence.

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17

signature MODEL_SIMULATOR = sig eqtype state eqtype event exception EventNotEnabled (* --- get the initial states and enabled events in each state --- *) val getInitialStates : unit -> (state * event list) list (* --- get the successor states and enabled events in each successor state --- *) val nextStates : state * event -> (state * event list) list (* --- execute an event sequence and return the list of resulting states --- *) (* --- and enabled events --- *) val executeSequence : state * event list -> (state * event list) list end

Fig. 3. SML signature of the model simulator interface.

The SSE engine currently implements full state space exploration, bit-state hashing [11], hash compaction [26], the comback method [25], state caching [12], and the equivalence method [14] based on canonicalisation of equivalent markings. All these methods have been implemented using the CPN simulator interface in Fig. 3 and the storage and waiting set components provided by the SSE engine. Currently only veri?cation of safety properties is supported by ASAP. State space exploration can be done both breadth-?rst and depth-?rst. It is worth observing that the model simulator interface allows the state space exploration

4

and model checking algorithms to be implemented such that they are independent from a concrete modelling language. As part of the development of ASAP, we have also developed a test and benchmarking tool containing a collection of small, medium, and large CPN models. This benchmarking suite makes it simple to pro?le the performance (e.g., time and space usage) of state space methods and their implementation. The benchmarking tool includes an SQL database where pro?ling data can be stored and a web-based GUI that makes it possible to query the database and display the results graphically. During the CPN workshop we plan to make a ?rst technology preview release of ASAP. For version 1.0 we plan to complete the implementation of the simulator interface in the SSE engine, and additionally implement the sweep-line method [2, 21], time condensed state spaces [3], and CTL and LTL model checking [10, 4]. Also, we plan to implement and provide the same set of state space query functions available in the state space tool of CPN Tools. In the user interface we will complete the implementation of the JEL Editor, implement an SML Query Editor, and implement the inspection perspective. Also, we will implement a functionality similar to the state space report and a simple interactive and automatic visualisation of state spaces as known from CPN Tools. Acknowledgements. The authors wish to acknowledge the work of Surayya Urazimbetova and Mads K. Kjeldsen who are signi?cantly contributing to the development of ASAP via their employment as student programmers in the ASCoVeCo project.

References
1. The ASCoVeCo Project. www.daimi.au.dk/~ascoveco. 2. S. Christensen, L.M. Kristensen, and T. Mailund. A Sweep-Line Method for State Space Exploration. In Proc. of TACAS’01, volume 2031 of LNCS, pages 450–464. Springer-Verlag, 2001. 3. S. Christensen, L.M. Kristensen, and T. Mailund. Condensed State Spaces for Timed Petri Nets. In Proc. of 22nd International Conference on Application and Th eory of Petri Nets, volume 2075 of Lecture Notes in Computer Science, pages 101–120. Springer-Verlag, 2001. 4. E. Clarke, O. Grumberg, and D. Peled. Model Checking. The MIT Press, 1999. 5. CPN Tools. www.daimi.au.dk/CPNTools. 6. Design/CPN. www.daimi.au.dk/designCPN. 7. Eclipse Graphical Modelling Framework (GMF). www.eclipse.org/modeling/gmf/. 8. Eclipse Modelling Framework (EMF). www.eclipse.org/modeling/emf/. 9. Eclipse Rich Client Platform (RCP). www.eclipse.org/home/categories/rcp.php. 10. E. A. Emerson. Temporal and Modal Logic, volume B of Handbook of Theoretical Computer Science, chapter 16, pages 995–1072. Elsevier, 1990. 11. G.J. Holzmann. An Analysis of Bitstate Hashing. Formal Methods in System Design, 13:289–307, 1998. 12. C. Jard and T. Jeron. Bounded-memory Algorithms for Veri?cation On-the-?y. In Proc. of CAV’91, volume 575 of LNCS, pages 192–202. Springer-Verlag, 1991. 13. K. Jensen. Coloured Petri Nets. Basic Concepts, Analysis Methods and Practical Use. Volume 1:Basic Concepts. Monographs in Theoretical Computer Science. Springer-Verlag, 1992. 14. K. Jensen. Coloured Petri Nets. Basic Concepts, Analysis Methods and Practical Use. Volume 2: Analysis Methods. Monographs in Theoretical Computer Science. Springer-Verlag, 1994. 15. K. Jensen. Condensed State Spaces for Symmetrical Coloured Petri Nets. Formal Methods in System Design, 9, 1996. 16. K. Jensen and L.M. Kristensen. Coloured Petri Nets – Modelling and Validation of Concurrent Systems. Springer-Verlag, In preparation. 17. K. Jensen, L.M. Kristensen, and L. Wells. Coloured Petri Nets and CPN Tools for Modelling and Validation of Concurrent Systems. In International Journal on Software Tools for Technology Transfer (STTT), 9(34):213–254, 2007.

5

18. J.B. J?rgensen and L.M. Kristensen. Computer Aided Veri?cation of Lamports Fast Mutual Exclusion Algorithm Using Coloured Petri Nets and Occurrence Graphs with Symmetries. IEEE Transactions on Parallel and Distributed Systems, 10(7):714–732, 1999. 19. J.B. J?rgensen and L.M. Kristensen. Veri?cation of coloured petri nets using state spaces with equivalence classes. In Petri Net Approaches for Modelling and Validation, volume 1 of LINCOM Studies in Computer Science, chapter 2, pages 17–34. Lincoln Europa, 2003. 20. L.M. Kristensen and K. Jensen. Speci?cation and validation of an edge router discovery protocol for mobile ad-hoc networks. In Proc. of Integration of Software Speci?cation Techniques for Applications in Engineering, volume 3147 of Lecture Notes in Computer Science, pages 248–269. Springer-Verlag, 2004. 21. L.M. Kristensen and T. Mailund. A Generalised Sweep-Line Method for Safety Properties. In Proc. of FME’02, volume 2391 of LNCS, pages 549–567. Springer-Verlag, 2002. 22. D. Peled. All from One, One for All: On Model Checking Using Representatives. In Proceedings of CAV’93, volume 697 of Lecture Notes in Computer Science, pages 409–423. Springer-Verlag, 1993. 23. A. Valmari. Error Detection by Reduced Reachability Graph Generation. In Proceedings of the 9th European Workshop on Application and Theory of Petri Nets, pages 95–112, 1988. 24. A. Valmari. The State Explosion Problem. In Lectures on Petri Nets I: Basic Models, volume 1491 of Lecture Notes in Computer Science, pages 429–528. Springer-Verlag, 1998. 25. M. Westergaard, L.M. Kristensen, G.S. Brodal, and L.A. Arge. The ComBack Method – Extending Hash Compaction with Backtracking. In Proc. of ICATPN’07, volume 4546 of Lecture Notes in Computer Science, pages 445–464. Springer-Verlag, 2007. 26. P. Wolper and D. Leroy. Reliable Hashing without Collision Detection. In Proc. of CAV’93, volume 697 of LNCS, pages 59–70. Springer-Verlag, 1993.

6

Component Tools: A Frontend for Formal Methods
Ekkart Kindler, Technical University of Denmark, Copenhagen

Abstract
Petri Nets are a powerful technique for modelling, analysing, and validating all kinds of systems. In order to exploit the full power of Petri nets, different versions of Petri nets and tools need to be used, and, sometimes, we need to combine them with other techniques. This makes it necessary to model the same system in different Petri net formalisms or other notations over and over again. Moreover, systems will often be constructed from standard components so that the modeller would like to build his system from these components. This way, even users with no experience in Petri nets can model systems. In order to help this group of users, the analysis results obtained by Petri net tools or other formal methods must be presented and visualized independently from Petri nets. Component Tools is a platform designed for this purpose. Along with a 3D-visualisation of the behaviour of the system (PNVis), non-experts can build Petri net models and see their model running in (virtual) reality. The tutorial will cover the concepts of ComponentTools as well as the concepts and modelling philosophy of the 3D-visualisation. Moreover, the tutorial will discuss the underlying software technology which makes it easy to implement this kind of tools. In addition to the existing concepts the tutorial will give an overview of ideas for future work and challenging research projects -- with the potential for many PhD theses.

References
E. Kindler and F. Nillies: Petri Nets and the Real World. Petri Net Newsletter 70, Cover Picture Story, pp. 3-8, April 2006. http://www.upb.de/cs/kindler/publications/copies/PRW-PNNL70.pdf E. Kindler and C. Páles: 3D-Visualization of Petri Net Models: Concept and Realization. In: J. Cortadella and W. Reisig (eds.): International Conference on Theory and Application of Petri Nets 2004, 25th International Conference, Bolgna, Italy. Springer, LNCS 3099: 464-473, June 2004. E. Kindler, V. Rubin, and R. Wagner: Component Tools: Application and Integration of Formal Methods. In: Electronic proceedings of the Workshop Object Orientierte Software Entwicklung 2005 (OOSE '05), Satellite event of Net.ObjectDays 2005, Erfurt, Germany, September 2005. http://www.upb.de/cs/kindler/publications/copies/OOSE05.pdf E. Kindler, V. Rubin, and R. Wagner: Component Tools: Integrating Petri nets with other formal methods. International Conference on Theory and Application of Petri Nets 2006, 27th International Conference, Turku, Finland. June 2006. LNCS 4024, pp. 37-56. E. Kindler and R. Wagner: Triple Graph Grammars: Concepts, Extensions, Implementations, and Application Scenarios. Tech. Rep. tr-ri-07-284, Software Engineering Group, Department of Computer Science, University of Paderborn, June 2007. http://www.upb.de/cs/ag-schaefer/Veroeffentlichungen/Quellen/Papers/2007/tr-ri-07-284.pdf 7

8

Towards Formal Speci?cation and Validation of Secure Connection Establishment in a Generic Access Network Scenario?
Paul Fleischer and Lars M. Kristensen
Department of Computer Science, University of Aarhus, IT-parken, Aabogade 34, DK-8200 Aarhus N, Denmark, {pf,kris}@daimi.au.dk

Abstract. The Generic Access Network (GAN) architecture is de?ned by the 3rd Generation Partnership Project (3GPP), and allows telephone services, such as SMS and voice-calls, to be accessed via generic IP networks. The main usage of this is to allow mobile phones to use WiFi in addition to the usual GSM network. The GAN speci?cation relies on the Internet Protocol Security layer (IPSec) and the Internet Key Exchange protocol version 2 (IKEv2) to provide encryption across IP networks, and thus avoid compromising the security of the telephone networks. The detailed usage of these two internet protocols (IPSec and IKEv2) is only roughly sketched in the GAN speci?cation. As part of the process to develop solutions to support the GAN architecture, TietoEnator Denmark has developed a more detailed GAN scenario which describes how IPsec and IKEv2 are to be used during the connection establishment procedure. The constribution of this paper is to present a CPN model developed to formally specify and validate the detailed GAN scenario considered by TietoEnator.

1

Introduction

The Generic Access Network (GAN) [1] architecture as speci?ed by the 3rd Generation Partnership Project (3GPP) [2] allows access to common telephone services such as SMS and voice-calls via generic Internet Protocol (IP) [3] networks. The operation of GAN is based on a Mobile Station (e.g., a cellular phone) opening an encrypted tunnel to a Security Gateway via an IP-network. A GAN Controller is responsible for relaying the commands send via this tunnel to the telephone network, which in turn allows mobile stations to access the services on the telephone network. The Security Gateway and the GAN Controller can either reside on the same physical machine or on two separate machines communicating by IP. The encrypted tunnel is provided by the Encapsulating Security Payload (ESP) mode of the IP security layer (IPSec) [4]. In order to provide such an encrypted tunnel, both ends have to authenticate each other, and agree
?

Supported by the Danish Research Council for Technology and Production and TietoEnator Denmark.

9

on both encryption algorithm and keys. This is achieved using the Internet Key Exchange v2 (IKEv2) protocol [5]. The GAN speci?cation [1] merely states that IKEv2 and IPSec are to be used, and in which operating modes. However, what that means for the message exchange is not speci?ed, and is left to the IKEv2 and IPSec standards. As such, there is no clear speci?cation of the IKEv2 message exchange and the states that the protocol entities are to be in when establishing a GAN connection. TietoEnator Denmark [6] is working on providing solutions to support the GAN architecture. Prior to the implementation, a textual usage scenario was formulated [7] which constitutes a speci?c instantiation of the full GAN architecture. The purpose of this scenario was two-fold. First, it de?nes the scope of the software to be developed, i.e., which parts of the full GAN speci?cation are supposed to be supported. Secondly, the scenario describes thoughts about the initial design of both the software and the usage of it. The scenario describes the details of how a mobile station is con?gured with an IP-address using DHCP [8] and then establishes an ESP-tunnel [9] to the Security Gateway using IKEv2 [5] and IPSec [4]. At this point, the mobile station is ready to communicate securely with the GAN Controller. The focus of the scenario is the establishment of the secure tunnel and initial GAN message exchanges which are the detailed parts omitted in the full GAN speci?cation. Throughout this paper the term GAN scenario refers to the detailed scenario [7] described by TietoEnator, while GAN architecture refers to the generic architecture as speci?ed in [1]. The contribution of this paper is to describe the results of a project at TietoEnator, where Coloured Petri Nets [10] were used as a supplement to a textual description of the GAN scenario to be implemented. The model has been constructed from the material available from TietoEnator [7], the GAN speci?cation [1], and the IKEv2 speci?cation [5]. The CPN model deals only with the connection establishing aspect of the GAN architecture, as this is the main focus of the TietoEnator project. As the scenario from TietoEnator deals with the aspect of con?guring the mobile station with an initial IP-address, the model does not only cover the communication of the GAN protocol, but also of the DHCP messages and actual IP-packet ?ow. The CPN model includes a generic IP-stack model, which supports packet forwarding and ESP-tunnelling. This modelling approach was chosen to allow the model to be very close to the scenario description used by TietoEnator with the aim of easing the understanding of the model for TietoEnator engineers which will eventually implement the GAN scenario. The model was presented to the engineers at two meetings. Each meeting resulted in minor changes of the model. Even though the TietoEnator engineers have did not have any experience with Coloured Petri Nets, they quickly accepted the level of abstraction and agreed that the scenario was the same as they had described by text. Coloured Petri Nets have been used to model various Internet protocols (e.g., [11][12]). The general approach of modelling Internet protocols is to abstract as much of the environment away, and only deal with the core of the protocol. The advantage of this approach is that the model gets simpler and the analysis

10

becomes easier due to restricted state space size. The approach presented in this paper also makes use of abstraction. However, the chosen abstraction level is based on a scenario, rather than a single protocol speci?cation. This gives a complete picture of the scenario, rather than a single protocol. This is an advantage when working with design of actual protocol implementations as it gives an overview of the needed features and component interaction. The main drawback is that the model becomes larger and more di?cult to analyse. Such a scenario model is not well suited for checking properties of a single protocol as done in [11] and [12]. The rest of this paper is organised as follows. Sect. 2 gives an introduction to the GAN scenario as de?ned by TietoEnator and presents the top-level of the constructed CPN model. Sect 3 and Sect. 4 present selected parts of the constructed CPN model including a discussion of the modelling choices made. In Sect. 5 we explain how the model of the GAN speci?cation was validated using simulation and state space analysis. Finally, in Sect. 6 we sum up the conclusions and discuss future work. The reader is assumed to be familiar with the CPN modelling language [10] and CPN Tools [13].

2

The GAN Scenario

This section gives an introduction to the GAN scenario [7] as de?ned by TietoEnator and the constructed CPN model. Fig. 1 shows the top-level module of the constructed CPN model. The top-level module has been organised such that it re?ects the network architecture of the GAN scenario. The six substitution transitions represent the six network nodes in the scenario and the four places with thick lines represent networks connected to the network nodes. The places with thin lines connected to the substitution transitions Provisioning Security Gateway, Default Security Gateway, Provisioning GAN Controller, and Default GAN Controller are used to provide con?guration information to the corresponding network nodes. The module has been annotated with network and interface IP addresses to provide that information at the topmost level. The substitution transition MobileStation represents the mobile station which is connecting to the telephone network via a generic IP-network. The place Wireless Network connected to MobileStation represents the wireless network which connects the mobile station to a wireless router represented by the substitution transition WirelessRouter. The wireless router is an arbitrary access point with routing functionality, and is connected to the ProvisioningSecurityGateway, through Network B. The provisioning security gateway is connected to the ProvisioningGANController via Network C. There is a second pair of security gateway (DefaultSeurityGateway) and GAN controller (DefaultGANController). The provisioning GAN controller is responsible for authenticating any connection, and redirecting them to another GAN controller in order to balance the load over a number of GAN controllers. In the GAN scenario, the default GAN controller represents the GAN controller which everything is redirected to. It is worth mentioning, that the generic GAN architecture sees the security gateway as a

11

SecurityGateway Provisioning Security Gateway Network C NET_PACKET 12.0.0.0/8

GANController Provisioning GAN Controller

iface 0: 172.1.1.1

iface 1: 12.0.0.1

iface 0: 12.1.1.1

ConfigProvSG SG Config MobileStation Mobile Station Wireless Network NET_PACKET 190.0.0.0/8 WirelessRouter Wireless Router Network B NET_PACKET 172.0.0.0/8 ConfigDefaultSG Default SGConfig NODE_CONFIG NODE_CONFIG

ConfigProvGANC Prov. GANCConfig NODE_CONFIG

iface 0: 190.1.1.1

iface 0: 190.1.1.254

iface 1: 172.1.1.254

ConfigDefaultGANC Default GANCConfig NODE_CONFIG

iface 0: 172.1.1.2

Default Security Gateway SecurityGateway

iface 1: 13.0.0.1

Network D NET_PACKET 13.0.0.0/8

iface 0: 13.1.1.1

Default GAN Controller GANController

Fig. 1. Top-level module the GAN scenario CPN model.

component within the GAN controller. However, TietoEnator decided to separate the two which makes the message exchange more clear. Neither the Wireless Router nor Network B are required to be owned or operated by the telephone operator. However, all security gateways, GAN controllers, and Network C and Network D are assumed to be under the control of the telephone operator, as non-encrypted messages will be exchanged across them. The basic exchange of messages in the GAN scenario consists of a number of steps as depicted in the Message Sequence Charts (MSCs) in Figs. 2-4. The MSCs have been generated from the constructed CPN model using the BritNeY animation tool [14]. The scenario assumes that the Mobile Station is completely o?-line to begin with. It then goes through 5 steps: Acquire an IP address using DHCP, Create a secure tunnel to the provisioning security gateway, use the GAN protocol to acquire the addresses of the security gateway and GAN controller to use for further communication, create a secure tunnel to the new security gateway, and ?nally initiate a GAN connection with the new GAN controller. The last step is not modelled, and step 4 is similar to step 2 and will as such not be treated separately. The ?rst step is to create a connection to an IP-network which is connected to the Provisioning Security Gateway of the service provider. It is assumed that a physical connection to the network is present. This step is depicted in Fig. 2 where the Mobile Station sends a DHCP Request to the Wireless Router and re-

Fig. 2. MSC showing DHCP step of connection establishment.

12

ceives a DHCP Answer containing the IP address. The Mobile Station is assumed to be equipped with either the domain name or IP address of the provisioning security gateway and the provisioning GAN controller. In this paper, we assume that the IP address is known, as this allows us to not model the DNS server and name lookup. Having obtained an IP-address via DHCP, the mobile station can now start negotiating the parameters for the secure tunnel with the provisioning security gateway using IKEv2. This is illustrated in the MSC shown in Fig. 3. This is done in 3 phases. The ?rst phase is the initial IKEv2 exchange, where the two parties agree on the cryptographic algorithms to use, and exchange Di?e-Hellman values in order to established a shared key for the rest of the message exchanges. The second phase is the exchange of Extensible Authentication Protocol (EAP) messages. The idea of EAP is that it is possible to use any kind of authentication protocol with IKEv2. In this situation, a protocol called EAP-SIM is used. As can be seen in Fig. 3, the Provisioning Security Gateway initiates the

Fig. 3. MSC showing IKE step of connection establishment.

EAP message exchange by returning an EAP Request to the Mobile Station’s authentication request. The actual EAP-SIM protocol exchanges 4 messages (2 requests and 2 responses) before it succeeds. As an result of the EAP-phase, the two parties have a shared secret key. In the third phase the Mobile Station

13

uses this shared key to perform ?nal authentication. The last packet sent by the Provisioning Security Gateway contains the network con?guration for the Mobile Station needed to establish a secure tunnel. Having established the secure tunnel, the Mobile Station can open a secure connection to the Provisioning GAN Controller and register itself. This is shown in the MSC in Fig. 4. If the Provisioning GAN Controller accepts the Mobile Station, it sends a redirect message, stating a pair of security gateway and GAN controller to use for any further communication. The Mobile Station closes the connection to the Provisioning GAN Controller and the Provisioning Security Gateway. The ?nal two steps of establishing a connection are to negotiate new IPSec tunnel parameters with the new security gateway, and establish a connection to the GAN controller. Having established the connection, the scenario ends. Fig. 4 only shows the registration with the Provisioning Security Gateway.

Fig. 4. MSC showing GAN step of connection establishment.

The scenario modelled involves multiple layers of the IP network stack. DHCP, used to con?gure the mobile station, is a layer 2 protocol, while IKE is a layer 4 protocol, and GAN is a layer 5 protocol. In order to accomodate all these layers in the model, a rather detailed representation of the IP components has been made. However, where simpli?cations were posible they have been made. For instance, the GAN protocol uses TCP, but TCP has not been modelled. Instead the network is currently lossless, but may reorder packets. This is not a problem, as GAN messages can be received out of order without messing things up. This is due to the fact, that the GAN Client only receives exactly the message it expects. The IP model contains routing which behaves similarly to the routing procedures implemented in real IP stacks. Some simpli?cations have been made to the routing algorithm, however, the end behaviour is the same. Each network node connected to an IP network has a routing table which contains information on how to deliver IP packets. In its simplest form, the entries in a routing table are pairs of destination network address and next hop, describing what the next hop is for IP packets matching the network address. In the IP model presented in this paper, IP addresses assigned to local interfaces have entries in the routing table as well, with a special next hop value. This is usually not the case for IP-stacks, but simpli?es the routing model as ingoing routing can be performed without inspecting the list of interfaces. The ESP tunnel, which is used to secure the communication between the mobile station and the security gateway, is a part of the IPSec protocol suite, which is an

14

extension to the IP stack. Only enough of IPSec is modelled to support this tunnelling, and as such IPSec is not modelled. There are two components that are related to IPSec in the model: Routing and the Security Policy Database (SPD). The routing system ensures that packets are put into the ESP tunnel, and extracted again at the other end. The SPD describes what packets are allowed to be sent and received by the IP-stack, and is also responsible for identifying which packets are to be tunnelled. Each entry in the SPD contains the source and destination addresses to use for matching packets, and an action to perform. Modelled actions are bypass, which means allow, and tunnel, which means that the matched packet is to be sent through an ESP tunnel.

3

Modelling the GAN Network Nodes

The CPN module is organised in 31 modules, with the top-level module being depicted in Fig. 1. The top module has four submodules: MobileStation, WirelessRouter, SecurityGateway and GANController. Each of these modules has one or more protocol modules and an IP layer module. The modelling of the protocol entities and the IP layer will be discussed in Sect. 4. In this section we present these modules in further detail. It can be seen that the provisioning and default GAN controller is represented using the same module and the same is the case with the provisioning and default security gateways. 3.1 Mobile Station

Fig. 5 shows the MobileStation module. The IP Layer substitution transition represents the IP layer of the mobile station and the Physical Layer substitution transition represents the interface to the underlying physical network. To the left are the three places which con?gure the IP layer module with a Security Policy Database, a Routing Table, and IP and MAC Addresses of the mobile station. These are also accessed in the DHCP, IKE, and GAN modules, as the con?guration places are fusion places. This has been done to reduce the number of arcs in the module and since the security policy database, routing table, and addresses are globally accessible in the mobile station. The remaining substitution transitions model the steps that the mobile station goes through when establishing a GAN connection. The mobile station is initially in a Down state represented by a unit token on the place Down. There are two tokens on the Addresses place representing the MAC and IP addresses assigned to the interfaces of the mobile station. The ADDR colour set is de?ned as follows: colset colset colset colset IP_ADDR MAC_ADDR IFACE IFACExIP_ADDR = = = = product INT * INT * INT * INT; INT; INT; product IFACE * IP_ADDR;

15

() Down 1 UNIT 1`()

DHCP DHCP Client

Ready IP_ADDR

Connect to Provisioning SG IKEInitiator VIF open to P-SG IP_ADDR

GANC Communication GANClient VIF Closed IP_ADDR

Connect to Default SG IKEInitiator 1`[{src=((0,0,0,0),0),dest=((0,0,0,0), 0),nl_info=PayloadList([PAYLOAD_DH CP]),policy=SpdBypass}] MSInitSPD MS SPD Security Policy Database SPD_ENTRY_LIST 1 VIF open to Def-SG IP_ADDR Send Buffer IP_PACKET Receive Buffer IP_PACKET

Routing Table MS Routing Table ROUTING_TABLE 1`IpAddr((0,(0,0,0,0)))++ 1`MacAddr((0,2))++ 1`MacAddr((0,2)) 1`IpAddr((0, (0,0,0,0))) 2 Addresses MS Addresses ADDR MS Interfaces IP-Layer

IP Layer

Network Buffer

IFACEBUFxNET_PACKET

Physical Layer

Network A I/O

NET_PACKET

Fig. 5. The MobileStation module.

16

colset IFACExMAC_ADDR = product IFACE * MAC_ADDR; colset ADDR = union IpAddr : IFACExIP_ADDR + MacAddr : IFACExMAC_ADDR; IP addresses are represented as a product of four integers, one for each octet of the address it represents. So, the IP address 192.0.0.1 becomes (192,0,0,1). MAC addresses and interfaces are represented as integers. On Fig. 5, IpAddr((0,(0,0,0,0))) means that interface 0 is assigned the all-zero IP address ((0,0,0,0)). MacAddr((0,2)) means that interface 0 has the MAC address 2. Initially, the SPD is con?gured to allow DHCP messages to pass in and out of the mobile station. The single token on the Security Policy Database place represents a single rule, matching packets with any source and any destination (src=((0,0,0,0),0) and dest=((0,0,0,0),0)) and DHCP payload (nl info=PayloadList([PAYLOAD DCHP])). The policy for this rule is bypass, meaning that packets matching this rule are to be allowed. As the routing table is initially empty (no IP con?gured), there are no tokens on the Routing Table place. The ?rst step is to perform DHCP con?guration as was previously illustrated in Fig. 2. This is done in the submodule of the DHCP substitution transition in Fig. 5. The DHCP module accesses all three con?guration places. After having con?gured the mobile station with DHCP, a token is placed on the Ready place, representing that the mobile station is now ready to start to communicate with the provisioning security gateway. The Connect to provisioning SG substitution transition takes care of establishing the ESP tunnel to the provisioning security gateway, as shown in the MSC on Fig. 3. After having connected to the provisioning security gateway, the GAN Communication transition is responsible for sending a GAN discovery message to the provisioning GAN controller and receiving the answer, which will be either reject or accept. In the ?rst case, the mobile station keeps sending discovery messages until one is accepted. When an accept message is received, the ESP tunnel to the provisioning security gateway is closed, and the IP address of the security gateway in the accept packet is placed on the VIF Closed place. Finally, the Connect to Default SG transition is responsible for establishing a new ESP tunnel to the default security gateway (which was the one received with the GAN accept message). 3.2 Wireless Router

Fig. 6 shows the WirelessRouter module. The wireless router has an IP layer, a physical layer, a security policy database, a routing table, and a set of associated addresses similar to the mobile station. The SPD is setup to allow any packets to bypass it. The wireless router has 2 interfaces, the Addresses place assigns MAC address 1 and IP address 190.1.1.254 to interface 0, and MAC address 3 and IP address 172.1.1.254 to interface 1. The routing table contains a single token of the colour set ROUTING TABLE which represents the complete routing table. The de?nition of this colour set is as follows:

17

colset NETWORK_ADDR = product IP_ADDR * INT; colset ROUTING_ENTRY = product NETWORK_ADDR * IP_NEXTHOP; colset ROUTING_TABLE = list ROUTING_ENTRY; The colour set is a list of ROUTING ENTRY. The NETWORK ADDR colour set represents a network address in an IP-network. It consists of an IP address and a pre?x, which selects how much of the IP address to use for the network address. For instance, a pre?x of 24 means to use the 24 ?rst bits the IP address as the network address, which corresponds to using the ?rst 3 octets (3 ? 8 = 24). Usually, this is written as 192.2.0.0/24, but in our model it becomes ((192,2,0,0),24) The IP NEXTHOP ?eld is explained in detail in Sect. 4.4. In the Wireless Router module, the routing table is set up such that packets to the host with IP address 190.1.1.1 are to be delivered directly via interface 0 (Direct(0)), packets to the network 172.1.1.0/24 are to be delivered directly through interface 1 (Direct(1)), and ?nally packets destined for 190.1.1.254 (the Wireless Router itself) are terminated at interface 0 (Terminate(0)). The wireless router implements the DHCP Server which is used initially by the mobile station to obtain an IP address. It can be seen that the wireless router has a physical connection to both Network A and Network B. 3.3 Security Gateway

Fig. 7 shows the SecurityGateway module. The security gateway has an IP layer, a physical layer, a security policy database, routing table, and a set of associated addresses similar to the mobile station and the wireless router. The con?guration places are initialised via the Init transition which obtains the con?guration parameters from the input port place Con?g. The security gateway implements the IKE responder protocol module which communicates with the IKE Initiator of the mobile station as described by the MSC shown in Fig. 3. The Con?g place is associated with the SG Con?g socket place of the top-level module (see Fig. 1) for the instance of the SecurityGateway module that corresponds to the Provisioning Security Gateway substitution transition (see Fig. 1). The initial marking of the SG Con?g con?gures the provisioning security gateway with two physical interfaces and a virtual interface for use with the ESP-tunnel. Interface 0 is con?gured with MAC address 4 and IP address 172.1.1.1, while interface 1 is con?gured with MAC address 5 and IP address 12.0.0.1. The third interface, interface 2, does not have any MAC address assigned to it, but only the IP address 80.0.0.1. The reason for this is that it is a virtual interface. The security policy database is set up such that packets sent via interface 2 are put into an ESP tunnel. The default security gateway is con?gured in a similar way. 3.4 GAN Controller

Fig. 8 shows the GAN Controller module which is the common submodule of the substitution transitions Provisioning GAN Controller and Default GAN Controller

18

1`[{src=((0,0,0,0),0),dest=((0,0,0,0), 1`{src=(ip_any_addr,0), 0),nl_info=AnyNextLayer,policy=SpdB dest=(ip_any_addr,0),nl_info = ypass}] AnyNextLayer,policy=SpdBypass} 1 Security Policy Database SPD_ENTRY_LIST 1`[(((190,1,1,1),0),Direct(0)),(((172,1, 1`(((190,1,1,1),0),Direct(0))++ 1,0),24),Direct(1)),(((190,1,1,254),0), 1`(((172,1,1,0),24),Direct(1))++ Terminate(0))] 1`(((190,1,1,254),0),Terminate(0)) 1 Routing Table IP-Layer ROUTING_TABLE Send Buffer IP_PACKET DHCPServer

DHCP Server

Receive Buffer IP_PACKET

IP Layer

4 1`IpAddr((0,(190,1,1,254)))++ 1`MacAddr(0,1)++ 1`IpAddr((1,(172,1,1,254)))++ 1`MacAddr(1,3)++ Addresses 1`MacAddr((0,1))++ 1`IpAddr((0,(190,1,1,254)))++ 1`MacAddr((1,3)) 1`IpAddr((1,(172,1,1,254))) ADDR

Network Buffer IFACEBUFxNET_PACKET

Physical Layer WR Interfaces

Network A I/O NET_PACKET

Network B I/O NET_PACKET

Fig. 6. The WirelessRouter module.

IKE Responder IKEResponder

Send Buffer spe_list SPD p IP_PACKET

Receive Buffer IP_PACKET p

SPD_ENTRY_LIST (spe_list, rt, addrList) NODE_CONFIG ROUTING_TABLE addrList

Config In

Init

rt

Routing Table IP-Layer

IP Layer

Addresses

Network Buffer IFACEBUFxNET_PACKET

ADDR Physical Layer SG Interfaces

I/O

Network B NET_PACKET

I/O

Network C NET_PACKET

Fig. 7. The SecurityGateway module.

19

in Fig. 1. Besides the IP and physical network layers, the GAN Controller implements the GANServer module which will be presented in the next section. The GAN controllers are con?gured in a similar way as the security gateways.

GAN Server GANServer

spe_list

Security Policy Database SPD_ENTRY_LIST

Send Buffer IP_PACKET

Receive Buffer IP_PACKET

Config In NODE_CONFIG

(spe_list, rt, addrList)

Init

rt

Routing Table IP-Layer ROUTING_TABLE

IP Layer

addrList Addresses

Network Buffer IFACEBUFxNET_PACKET

ADDR GANC Interfaces

Physical Layer

I/O

Network C NET_PACKET

Fig. 8. The GAN Controller module.

4

Modelling the Protocol Entities

This section describes the modelling of the protocol entities present in the mobile station, wireless router, security gateways, and GAN controllers. The description of the protocol entities has been organised such that it re?ects how we have decided to organise the protocol entities in the CPN model. This means that we always describe peer protocol entities, i.e., when describing the DHCP client of the mobile station we simultaneously describe its peer protocol entity which is the DHCP server of the wireless router. 4.1 Dynamic Host Con?guration Protocol

Fig. 9(top) shows the DHCP Client module of the mobile station and Fig. 9(bottom) shows the DHCP Server module of the wireless router. The two modules model the part of GAN connection establishment which was shown in Fig. 2. The DHCP client starts by broadcasting a request for an IP address and then awaits a response from the DHCP server. When the DHCP server receives a request it selects one of its FreeAddresses and sends an answer back to the DHCP client. When the client receives the answer it con?gures itself with the IP address and updates it routing table and security policy database accordingly. Three entries are added to the routing table: 1‘((#ip(da),32), Terminate(0)) means that the IP address received in the DHCP answer belongs to interface 0, while

20

1‘(calcNetwork(#ip(da), #netmask(da)), Direct(0)) speci?es that the network from which the IP address has been assigned, is reachable via interface 0. Finally, a default route is installed with 1‘(((0,0,0,0),0), Via(#default gw(da))), such that packets which no other routing entry matches, are send to the default gateway speci?ed in the DHCP answer. The SPD is modi?ed so that the previous rule, which allowed all DHCP tra?c is removed and replaced with a new rule, which states that all packets sent from the assigned IP address are allowed to pass out, and all packets sent to the assigned IP address are allowed to pass in.
() Down In () UNIT

{src=ip_any_addr, dest=(255,255,255,255), payload=DhcpRequest(mac)}

Send DHCP Request () Wait for DHCP Response UNIT ()

MacAddr(iface, mac) 1`MacAddr((0,2))++ 1`IpAddr((0, (0,0,0,0)))

Addresses MS Addresses ADDR

1`((#ip(da),32), Terminate(0))++ 1`(calcNetwork(#ip(da), #netmask(da)),Direct(0))++ 1`(((0,0,0,0),0), Via(#default_gw(da))) Routing Table MS Routing Table ROUTING_TABLE MSInitSPD spe_list 1`{src=(#ip(da),0), dest=(ip_any_addr,0), nl_info=AnyNextLayer, policy=SpdBypass} MS SPD SPD_ENTRY_LIST Send Buffer Out IP_PACKET Out

IpAddr(iface,ip_any_addr) Receive DHCP Answer IpAddr(iface, #ip(da)) p

[#payload(p) = DhcpAnswer(da)]

(172,1,1,1)

SPD

Node Configured IP_ADDR In Receive Buffer IP_PACKET

1`(190,1,1,1) Assigned Addresses (mac,ip_addr) ip_addr Receive DHCP Request Free Addresses

MACXIP_ADDR {src=ip_any_addr, dest=(255,255,255,255), payload=DhcpAnswer( {ip = ip_addr, out_iface = 0, target=mac, netmask=(255,255,255,0), default_gw=(190,1,1,254), dns_servers=[(190,1,1,250)]} )}

IP_ADDR

{src=src_ip, dest=dest_ip, payload=DhcpRequest(mac) }

Send Buffer Out IP_PACKET In

Receive Buffer IP_PACKET

Fig. 9. DHCP client (top) and DHCP server (bottom) modules.

4.2

IKEv2 Modules

Fig. 10(left) shows the IKEInitiator module of the mobile station and Fig. 10(right) shows the IKEResponder module of the security gateways. The modules model second step of the GAN connection establishment that was illustrated in Fig. 3. Each module describes the states that the protocol entities go through during the IKE message exchange. The state changes are represented by substitution transitions and Fig. 11 shows the Send IKE SA INIT Packet and Handle SA INIT Request modules.

21

The Send IKE SA INIT Packet transition on Fig. 11(top) takes the IKE Initiator from the state Ready to Await IKE SA INIT and sends an IKE message to the security gateway initialising the communication. The IP address of the security gateway is retrieved from the Ready place. Fig. 11(bottom) shows how the IKE SA INIT packet is handled by the IKE Responder module (which the security gateway implements). Upon receiving an IKE SA INIT packet it sends a response and moves the responder to the Wait for EAP Auth state. The submodules of the other substitution transition of the IKE modules are similar. Neither initiator nor responder will receive packets that are not expected. They remain in the network bu?er forever.

Ready In IP_ADDR

Send IKE_SA_INIT Packet Send IKE_SA_INIT Packet
Handle SA_INIT Request

Await IKE_SA_INIT UNIT

Handle SA_INIT Request

Send IKE_AUTH Packet Send IKE_AUTH Packet

Wait for EAP AUTH IP_ADDR

Await IKE_AUTH ongoing EAP UNIT

Handle EAP AUTH Request Handle EAP AUTH Request

Send EAP Data Send EAP Data

Wait for EAP IP_ADDR

Wait for EAP Reply UNIT

Handle EAP Request Handle EAP Request

Send EAP Data 2 Send EAP Data 2

Wait for EAP 2 IP_ADDR

Wait for EAP Reply 2 UNIT
Handle EAP Data Handle EAP Data

Receive EAP Reply Receive EAP Reply
Wait for AUTH IP_ADDR

Wait for IKE_AUTH Reply UNIT
Handle AUTH Request Handle AUTH Request Outgoing IKE Replies IPxIP_PAYLOAD Incoming IKE Requests IPxIKE_PACKET

Receive IKE_AUTH Reply Setup vif

IKE Packets Initiator

(dest_ip, ip_payload)

IPxIP_PAYLOAD

Out

IKE_AUTH Done IP_ADDR
Append IP Header IpAddr(0,src_ip) Addresses I/O ADDR {src=src_ip, dest=dest_ip, payload=ip_payload}

(#src(p), ike_packet)

(dest_ip, ip_payload) Append IP Header {src=(190,1,1,1), dest=dest_ip, payload=ip_payload} Send Buffer IP_PACKET Receive Buffer IP_PACKET

Receive IKE Request [#payload(p) = IkeInitiator(ike_packet)] p

In

Send Buffer Out IP_PACKET In

Receive Buffer IP_PACKET

Out

Fig. 10. IKE initiator (left) and IKE responder (right) modules.

22

4.3

GAN Modules

On Fig. 12(top) the GANClient module of the mobile station is shown, while Fig. 12(bottom) shows the GANServer module of the GAN controller. In the Tunnel Con?gured state, a secure tunnel to the security gateway has been established. The mobile station initiates the GAN communication by sending a GA-RC discovery message. The Send GA RC Discovery Message transition does just that, and places the mobile station in the Wait for GA RC Response, where the mobile station will wait until a response is received from the GAN controller. As can be seen in Fig. 12(right), the GAN controller can either answer a request with an accept or reject message. If the GANClient receives a reject response, the Handle GA RC Reject transition will put the client back into the Tunnel Con?gured state, and another discovery message will be sent. This will continue until an accept message is received, in which case the Handle GA RC Accept transition puts the client in the GA RC Accept Received state, and closes the secure tunnel. The is done by removing the address associated with the tunnel from the Addresses place, and removing any entries in the SPD and routing table containing references to the interface. 4.4 IP Network Layer

Fig. 13 shows the IPLayer module which is used to model the IP network layer in the mobile station, wireless router, security gateways, and the GAN controllers. As mentioned in Sect. 2 many details of the IP stack have been modelled, such as the routing system and the security policy database. Transport protocols (e.g., TCP), are however, not modelled. The access to the underlying physical network is modelled via the input/output port place Network which has the colour set NET PACKET de?ned as: colset NET_PACKET = product MAC_ADDR * MAC_ADDR * IP_PACKET; The ?rst component of the product is the source MAC address, while the second is the destination MAC address. The ?nal component is the payload, which currently can only be an IP packet. MAC addresses are represented by integers. The actual physical network layer has been abstracted away, as we do not care whether the physical network is, e.g., an Ethernet or an ATM network. The chosen representation of a network cannot lose packets but can reorder them, as tokens are picked non-deterministically from the Network place. A real network does occasionally drop packets, and considering losing packets is especially important when building fault-tolerant systems. Both IKE and TCP use timeouts and sequence numbers to retransmit packets, such that the protocols deal with lossy networks. Rather than modelling the retransmission schemes, we have chosen to have a losseless network. Receiving packets from the network is modelled as a transition which consumes a NET PACKET-token, with the destination MAC address corresponding to the MAC address of the network node. Sending packets is a matter of producing a NET PACKET-token with the correct source and destination addresses and

23

Ready In dest_ip IP_ADDR

Send IKE_SA_INIT (dest_ip, Packet IkeInitiator({ exch = IKE_SA_INIT({ SAi=[sa_proposal1], KEi=2, SAr=[], () KEr=0}), msg_id = 0}))

IKE Packets Initiator Out

IPxIP_PAYLOAD

Out

Await IKE_SA_INIT UNIT

Handle SA_INIT Request (src_ip, IkeResponder({ msg_id=(#msg_id(ike_packet)), exch=IKE_SA_INIT({SAr = [hd(#SAi(sa_init))], KEr = (#KEi(sa_init)), src_ip SAi=[], KEi=0 }) }))

(src_ip, ike_packet) [#exch(ike_packet)= IKE_SA_INIT(sa_init)]

Outgoing IKE Replies Out

IPxIP_PAYLOAD

Wait for EAP AUTH Out

IP_ADDR

Incoming IKE Requests In IPxIKE_PACKET

Fig. 11. Example of IKE initiator (top) and IKE responder (bottom) submodules.
In Tunnel Configured IP_ADDR ip_addr {src=ip_addr, dest=(12,1,1,1), payload=GANPayload(GARCDiscovery)} ip_addr

Send GA RC Discovery Message

1`[{src=((0,0,0,0),0),dest=((0,0,0,0), 0),nl_info=PayloadList([PAYLOAD_DH MSInitSPD CP]),policy=SpdBypass}] 1 MS SPD SPD_ENTRY_LIST spe_list SPD spd_remove_iface (1, ip_addr, spe_list)

ip_addr Wait for GA RC Response ip_addr IP_ADDR Handle GA RC Reject p

[#payload(p) = GANPayload(GARCReject)]

ip_addr

Routing Table MS Routing Table ROUTING_TABLE

rt_remove_iface(1, ip_addr, rt) rt

Handle GA RC Accept

p

[#payload(p) = GANPayload(GARCAccept(ip_addr2, ip_addr3))]

1`MacAddr((0,2))++ 1`IpAddr((0,(0,0,0,0)))++ 1`IpAddr((0, (0,0,0,0))) 1`MacAddr((0,2))

IpAddr(1,ip_addr) ip_addr2

2

Addresses

MS Addresses ADDR

Send Buffer Out IP_PACKET

Out

GA RC Accept Received IP_ADDR In

Receive Buffer IP_PACKET

{src=(12,1,1,1), dest=(#src(p)), payload=GANPayload( GARCAccept((172,1,1,2),(13,1,1,1)))}

Accept Discovery Request

p

[#payload(p) = GANPayload(GARCDiscovery)]

{src=(12,1,1,1), dest=(#src(p)), payload=GANPayload( GARCReject)}

Reject Discovery Request

p

[#payload(p) = GANPayload(GARCDiscovery)]

Send Buffer Out IP_PACKET In

Receive Buffer IP_PACKET

Fig. 12. GANC modules mobile station (top) and controller (bottom).

24

Receive Buffer Out Send Buffer In IP_PACKET Routing Table I/O ROUTING_TABLE Ingoing Routing Ingoing Routing IP_PACKET

Allowed Incoming Packets IP_PACKET

Check SPD Out Check SPD Out

SPD I/O SPD_ENTRY_LIST

Check SPD In Check SPD In

Allowed Packets IP_PACKET

Received Packets IP_PACKET p [(dest_mac = 0 andalso src_mac <> mac) orelse dest_mac = mac]

Outgoing Routing Outgoing Routing

Addresses I/O ADDR

MacAddr(iface,mac)

Receive Network Packet (NetIn iface,(src_mac, dest_mac, p))

Network I/O IFACEBUFxNET_PACKET

Fig. 13. The IP-Layer module. In-going packet ?ow (right) and outgoing packet ?ow (left).

the intended IP packet. The IP layer is completely generic and con?gured with 3 places for network addresses, routing table, and Security Policy Database (SPD ). The Routing Table place corresponds to the routing table found in real IP implementations. It consists of a number of entries, each of a pair (NETWORK ADDR, IP NEXTHOP), where IP NEXTHOP is as de?ned as: colset IP_NEXTHOP = union Direct : IFACE + Via : IP_ADDR + Terminate : IFACE; The colour set de?nes which action is to be taken for packets going to the speci?ed IP network. There are three possible actions to take: Direct, the packet can be delivered directly via the local physical network via IFACE. Via, the packet can get closer to its destination by being delivered to the IP ADDR. Terminate, the destination network address is a local interface address of IFACE. The SPD place is the SPD database, and describes which packets are allowed to be sent and received by the IP layer. An entry in the SPD database can also specify that certain packets are to be tunnelled through a secure tunnel. Finally, the Addresses place contains one token for each address known to the IP Layer. These addresses are both physical (MAC) addresses, and IP addresses. Each ADDR token contains both an interface number, and the address (MAC or IP). Packets to be sent are put on the Send Bu?er place by upper-layers. The ?rst step done by the IP layer, is to check the SPD database, which is done by the Check SPD Out transition. The Check SPD Out module looks through the SPD

25

database to ?nd an entry which matches the source and destination addresses of the packet. If no entry is found, the packet is dropped. If an entry is found, the entries action is applied. Either the action in bypass, meaning that the packet can be sent further down the IP-stack, or the action is tunnel, meaning that the packet is to be sent through a secure tunnel. In the latter case, a new IP-packet is constructed according to the tunnel information associated with the tunnel action. The new packet is placed on the Outgoing Packets place, and has to pass the outgoing SPD check as well. If the packet is allowed to be sent, it is put on the Allowed Packets place. In order to be able to construct a NET PACKET token, the destination MAC needs to be found. This is done by the Outgoing Routing transition. As can be seen in Fig. 13, it needs to know both about the routing table and the addresses. If a next-hop has been found, a token is placed on the Network place with information about which interface to send on and the MAC address of the next-hop. Ingoing packets are retrieved from the Network place by the Receive Network Packet transition. Destination MAC and interface number of the network packet have to match one of the MAC addresses con?gured in the Addresses place. The IP PACKET inside the NET PACKET is placed on the Received Packets place. Check SPD In performs incoming SPD check, while Ingoing Routing decides if the packet is to be delivered locally, forwarded, or is a tunnelled packet which has to be de-tunnelled. In the latter case, the packet is put on the Received Packets place, and goes through SPD checking and routing again. If the packet has its ?nal destination at the local node, it is put in the Receive Bu?er. The IP PACKET colour set models IP packets and is de?ned as: colset IP_PACKET = record dest : IP_ADDR * src : IP_ADDR * payload : IP_PAYLOAD; It has a source and destination IP address and a payload. The IP PAYLOAD colour set is a union of all possible payloads. The colour set is never used by any of the generic network components, and is as such de?ned accordingly to the rest of the model. In the GAN scenario, the IP PAYLOAD colour set has constructors for DHCP, IKEv2, and GAN packets.

5

Validation of the GAN Scenario

During the construction of the model, simulation was used to check that the model behaviour was as desired. Even though simulation does not guarantee correct behaviour, it was very useful in ?nding modelling errors and make explicit where further speci?cation of the message exchanges were required. For instance, simulation was a valuable tool in validating the packet forwarding capabilities of the IP-layer. By placing tokens that represent packets to be forwarded on a network nodes input bu?er and starting the simulation, it is easy to see if the packet is being placed in the output bu?er as expected. If not, then singlestepping through the simulation helps to understand the behaviour of the model,

26

and modify it so that it behaves as intended. Simulation was also heavily used to show engineers at TietoEnator, how the model and especially how the IP-packet ?ow worked and thereby enabling discussions of the speci?cation. The advantage of simulation over state space veri?cation is that the simulation has immediate visual feedback, and as such is much easier to understand. A formal validation was performed on the state space generated from the model. The generated state space consists of 683 nodes, while the Strongly Connected Component (SCC) graph consists of 598 nodes of which 1 is non-trivial. There is a single home marking with number 683 which also is a dead marking. The most interesting property to check is that the mobile station can always end up being con?gured properly, i.e., that it has both gotten an IP address, has successfully communicated with the provisioning GAN controller, and received addresses of the default security gateway and GAN controller. For this, we checked that in marking 683 there is a token in the VIF open to Def-SG place of the mobile station (see Fig. 5). Furthermore, we checked that there were no tokens in any of the other places of the mobile station state machine. This would indicate an error in the model, as we do not want the mobile station to be able to be in two states at the same time. To do this we de?ned a predicate, which checks that only the VIF open to Def-SG contains tokens. Checking all nodes in the state space for this predicate, shows that it holds only for marking 683. It is also interesting to investigate whether the routing table and security policy database look as expected. Rather than de?ning predicates, we displayed the dead marking in the simulator tool of CPN Tools and inspected the con?guration of the mobile station. This showed that both routing tables, address assignments, and security policy database were as expected. The state space report also showed that the transitions RejectDiscoveryRequest and HandleGARCReject (see Fig. 12) both were impartial. This means that if the system does not terminate in marking 683, then it is because the GAN controller keeps rejecting the connection.

6

Conclusion and Future Work

The overall goal of the project was to construct a CPN model and obtain a more complete speci?cation of the GAN scenario to be implemented by TietoEnator. The act of constructing the CPN model helped to specify the details of the message exchanges that were not explicit in the textual scenario description. Including a detailed modelling of the IP stack was necessary in order to capture the details of sending GAN packets from the mobile station to the GAN controller. Furthermore, it was required in order to validate correctness of the the routing table contents, SPD entries, and IP address distribution. The CPN model has been discussed with TietoEnator engineers, and they were convinced of its correctness by using the simulation capabilities of CPN Tools. Using simulation and state space analysis has helped to give further con?dence in the constructed model, but more importantly it has provided valuable information about the properties of the scenario.

27

The initial GAN model presented in this paper matches the GAN scenario as closely as possible, meaning that every entity in the scenario has been represented in the model, and every action in the scenario has a model counterpart. This allows much easier understanding of the model, when the scenario is known, as all components in the model are known in advance. Currently, we are working on an extended version with multiple mobile stations and GAN controllers. In near future, TietoEnator is to implement the GAN controller. Based on the experience from the project presented in this paper, it has been decided that CP-Nets will be used to model the initial controller design. Besides the advantages of having a formal model which can be validated by means of state space analysis, the goal is to generate template code for the GAN controller directly from a CPN model of the controller. This will ease the work of the initial implementation and help ensure that the implementation is consistent with the design as speci?ed by the CPN model.

References
1. 3GPP: Digital cellular telecommunications system (Phase 2+); Generic access to the A/Gb interface; Stage 2. 3GPP TS 43.318 version 6.9.0 Release 6 (2007) 2. 3GPP: Website of 3GPP. http://www.3gpp.org (2007) 3. Postel, J.e.a.: Internet Protocol DARPA Internet Program Protocol Speci?cation. RFC791 (1981) 4. Kent, S., Seo, K.: Security Architecture for the Internet Protocol. RFC4301 (2005) 5. Kaufman, C.E.: Internet Key Exchange (IKEv2) Protocol. RFC4306 (2005) 6. TietoEnator: Website of TietoEnator Denmark. http://www.tietoenator.dk (2007) 7. Grimstrup, P.: Interworking Description for IKEv2 Library. Ericsson Internal. Document No. 155 10-FCP 101 4328 Uen (2006) 8. Droms, R.: Dynamic Host Con?guration Protocol. RFC2131 (1997) 9. Kent, S.: IP Encapsulating Security Payload (ESP). RFC4303 (2005) 10. Jensen, K., Kristensen, L.M., Wells, L.: Coloured Petri Nets and CPN Tools for Modelling and Validation of Concurrent Systems. STTT (International Journal on Software Tools for Technology Transfer) (2007) 11. Villapol, M.E., Billington, J.: Analysing properties of the resource reservation protocol. In: Applications and Theory of Petri Nets 2003: 24th International Conference, ICATPN 2003, Eindhoven, The Netherlands, June 23-27, 2003. Proceedings. Volume Volume 2679/2003 of Lecture Notes in Computer Science., Springer Berlin / Heidelberg (2003) 377–396 12. Kristensen, L.M., Jensen, K.: Speci?cation and validation of an edge router discovery protocol for mobile ad hoc networks. In Ehrig, H., Damm, W., Desel, J., Groe-Rhode, M., Reif, W., Schnieder, E., Westkmper, E., eds.: Integration of Software Speci?cation Techniques for Applications in Engineering. Volume Volume 3147/2004 of Lecture Notes in Computer Science. Springer Berlin / Heidelberg (2004) 248–269 13. University of Aarhus: CPNTools. http://www.daimi.au.dk/CPNTools (2007) 14. Westergaard, M.: BRITNeY Suite. http://wiki.daimi.au.dk/britney (2007)

28

Towards Modeling and Simulating a Multi-party Negotiation Protocol with Colored Petri Nets
E. Bacarin1 , W.M.P van der Aalst2 , E. Madeira3 , and C. B. Medeiros3
1 2

Department of Computer Science - UEL - CP 6001 86051-990 Londrina,PR Brazil. bacarin@uel.br Department of Mathematics and Computer Science, Eindhoven University of Technology, P.O. Box 513, NL-5600 MB, Eindhoven, The Netherlands. w.m.p.v.d.aalst@tue.nl 3 Institute of Computing - UNICAMP - CP 6176 13081-970 Campinas,SP Brazil. {edmundo,cmbm}@ic.unicamp.br

Abstract. E-contracting, i.e., establishing and enacting electronic contracts, has become important because of technological advances (e.g., the availability of web services) and more open markets. However, the establishment of an e-contract is complicated and error prone. There are multiple negotiation styles ranging from auctions to bilateral bargaining. This paper provides an approach for modeling multi-party negotiation protocols in colored Petri nets. It is shown how di?erent negotiation styles can be modeled in a uni?ed and consistent way. Moreover, CPN Tools is used to analyze the resulting colored Petri nets. Simulation can be used for both validation and performance analysis, while state-space analysis can be used to discover anomalies in various multi-part negotiation protocols.

1

Introduction

Contracts are documents that states the mutual obligations and authorizations that re?ect the agreements between two trading partners [1]. An e-contract is a contract modeled, speci?ed and enacted by a software system [2]. E-contracting has become important because of technological advances, for instance, agent technology and web services have allowed for the establishment of virtual enterprises or management of supply chains. E-contracting is a means to regulate the relationship among partners of a virtual enterprise or a particular supply chain. According to Angelov [3], automatic negotiation is not a trivial task. Most of the negotiation systems proposed so far have an overly limited scope: they run a particular kind of negotiation – typically a bargain or an auction – in a restricted market place. The produced contracts are signed by only two negotiators. Several bilateral contracts must be produced when the agreement comprises more than two partners. In a collaborative multi-partner settlement, this may cause semantic loss. A single contract signed by several partners can express a common goal shared by them by means of a rich set of complex relationships. Splitting this contract into a number of bilateral contracts can make unclear some of these relationships, and even destroy others. This paper aims at both automatic negotiation and multi-party contracts. It shows how the main parts of the SPICA negotiation protocol [4] can be modeled and simulated by means of Petri nets. The main contributions are: a) the paper describes a negotiation protocol that combines different negotiation styles — namely: bargain, auction, ballot — to produce an e-contract that can be signed by several partners; b) it shows how such a protocol can be modeled as a colored Petri net (CPN) and simulated using CPN Tools [5]; c) it also shows how the capabilities of CPN Tools assisted in the identi?cation of design ?aws and how these were addressed. The paper is organized as follows. Section 2 overviews some related work. Section 3 brie?y introduces various negotiation protocols, presents a running example that is used throughout the paper, and illustrates the SPICA negotiation protocol through short examples. Section 4 shows how the main parts of the SPICA protocol were modeled in terms of colored Petri nets and presents some of its subnets (the total model is composed of 31 subnets). Section 5 describes how the model was adjusted to simulate the running example. Section 6 discusses what we have learnt by modeling and simulating the protocol using CPN Tools, which problems we have encountered, and how they were addressed. Finally, Section 7 concludes the paper.

29

2

Related Work

This section reviews related work on negotiation processes and the use of CPN Tools to model and validate protocols. There are a number of mechanisms that guide the negotiation process. Bartolini [6] constructs negotiation templates that specify di?erent negotiation parameters. Chiu [7] also uses contract templates as a reference document for negotiation. Similarly, [8] uses a contract template that describes the negotiation parameters, how they are interrelated, along with meta-level rules about the negotiation. In contrast, [9] uses a set of examples of good agreements and it is up to the negotiator to try to get as close as possible to one of the examples. Like most of the related work, our negotiation process is guided by a contract model. Thus, broadly speaking, the negotiation process concerns determining values for unbound properties. Our negotiation process is developed through the exchange of messages among the negotiators that comply with a speci?c protocol. This is a common approach, like the ones based on FIPA’s standards [10], e.g., [11]. Governatori and others [12] use a di?erent approach. They propose a negotiation process that uses Defeasible Logic. Whatever the basis of the negotiation process, all negotiators must understand concepts and names used during the negotiation. The work of [11] combines the use of ontologies and agent technologies to help in solving naming problems in car assembly supply chain negotiations. Our approach also uses ontologies (see [4]) According to Angelov [3], automatic negotiation is a di?cult task. Tools that help in the design and implementation of negotiation protocols are needed. Jensen and others [5] present CPN Tools. It builds on Coloured Petri Nets [13] and provides a rich set of resources for modeling, simulating and validating systems where concurrency, communication, and synchronisation play an important role. CPN Tools has been used to analyse both experimental protocols and also well-established ones. Chen and others [14] use CPNs to model a multi-agent system for supply chain management based on agent negotiation. They describe their negotiation protocol and explain how they formally modeled the negotiation process by using CPNs. The negotiation protocol presented is similar to our auction and bargain negotiation styles. Liu and Billington [15] analysed the Capability Exchange Signalling (CES) protocol using CPN Tools and found it may fail in some speci?c circumstances.

3
3.1

Negotiation: A Particular Protocol
Overview of Negotiation Protocols

Negotiation is a process by which autonomous entities communicate and compromise to reach an agreement on matters of mutual interest while maximizing their individuals utilities [16]. Automated negotiation (e-negotiation) is done by software rather than people and organizations, in general in the form of software agents, and their agreement is stated in e-contracts. A negotiation process involves a number of issues. To begin with, the number of negotiators involved is typically one-to-one (bargaining), one-to-many (bidding), or many-to-many (doubleauction). In bargains, one seller deals with one buyer. Bidding also has a broad range of ?avors, which involve request for proposals and interactions among seller(s) and buyer(s). The so-called English or Dutch auctions have many buyers competing for a product sold by an auctioneer. In English auctions, the auctioneer de?nes a start price and the bidders increase continuously the item’s value until the last bid cannot be beaten. Dutch auctions start with a high value and the auctioneer decreases this value until a buyer agrees to pay the proposed value. A many-to-many negotiation can occur through a so-called double auction. In this case, several sellers o?er their products on a “shared space” and several buyers submit their bids. There is a mechanism that matches o?ers and bids. A second issue that needs to be addressed by the negotiation process is related to the number of items. The negotiation process may be restricted to a single product or to a bundle of items. In the latter case, the buyer may be interested in buying all items or none of them [8].

30

A third issue refers to the negotiation strategy. According to [12], techniques for designing negotiation strategies can be classi?ed into three categories: (i) game-theoretic, (ii) heuristic, and (iii) argumentation. The ?rst approach models a negotiation situation as a game and attempts to ?nd dominant strategies for each participant by applying game theory techniques. In heuristicbased approaches, a strategy consists of a family of tactics (i.e., a method for generating countero?ers), and a set of rules for selecting a particular tactic depending on the stage of the negotiation. Argumentation-based approaches extend heuristic ones by introducing communication patterns such as threats (e.g., “that is my last o?er”), rewards, etc. The fourth issue concerns how the negotiation process is ?nished: either by agreement or by withdrawal. In [6], agreement formation rules determine which proposals are matched. In [9], a negotiation is aborted if agreement is not reached in a prede?ned number of rounds. Finally, the last issue concerns how to renegotiate an existing contract due to some external change. This includes discovering which contracts were a?ected by the change, which clauses should be modi?ed, who should modify the contract, and so forth. 3.2 Running Example

This section presents the running example that will be used throughout the remainder of the paper. Milkyway Dairy is a ?ctitious dairy industry that produces milk derivatives, especially lowfat yoghurt. The farms in its region mainly produce milk and fruits. Periodically, Milkyway Dairy negotiates contracts with nearby farmers for future delivery of milk, blueberries and peaches. Thus, they can plan their future production. Because of governmental regulations, the dairy and the farmers must agree upon maximum milk quota each one will be allowed to deliver. However, the dairy will seek the cheapest supplier for each fruit. The price of the milk is de?ned at delivery by an o?cial price list, but Milkway negotiates with the farmers a minimum price that will be payed at delivery. In turn, the farmers guarantee that they will deliver at least 500 liters of milk each week. The prices and quantities of di?erent fruits are established during the negotiation. Milkyway has a prede?ned draft (or model) for this contract. The negotiation process consists of ?lling some gaps in this model. The gaps, denominated properties, are identi?ed by names preceded by # (e.g., #MINPRICE, #PRICEBERRY). A simpli?ed version of this contract model is shown in plain English in Figure 1. Thus, the parties will agree upon, for instance, a value for the minimum price (#MINPRICE in Clause 3) and which farm will provide berries (#Fa). Note that this contract is a multi-party contract signed by the dairy and by several farmers.
Clause 1: Milkyway Dairy, herein named Dairy, and farms Farm 1, Farm 2, Farm 3, Farm 4, herein respectively named F1, F2, F3 and F4, agree that the amount of milk Dairy may buy each week from any of the stated farms is at most #QMAX liters. Clause 2:F1,F2,F3 and F4 will deliver altogether at least 500 liters of milk per week to Dairy. Clause 3:The price of milk is de?ned by the O?cial Price List at the moment of delivery. However, the Dairy agrees to pay at least #MINPRICE per liter of delivered milk. Clause 4:If farms F1, F2, F3 and F4 do not succeed to ful?ll clause 2, they must pay Dairy a ?ne worth 10000*#MINPRICE. Clause 5:Farm #Fa agrees to deliver #QBERRY Kg of blueberries at e#PRICEBERRY a kilogram weekly. Clause 6: Farm #Fb agrees to deliver #QPEACH Kg of peaches at e#PRICEPEACH a kilogram weekly. Fig. 1. Simpli?ed multi-party contract with six properties that need to be negotiated

31

3.3

The SPICA Protocol

This section describes the negotiation process. In this paper, we focus on our SPICA protocol [4]. SPICA (SuPply chain Integration, Coordination, contracting and Auditing framework) is the Latin term for the ear of some grains (e.g., as in ear of corn, or wheat). It is the main star in the Virgo constellation. This constellation is associated to a few myths related to agriculture. In this protocol, the negotiation process is orchestrated by a leader negotiator and is guided by a contract model. The contract model is a prede?ned contract template which is ?lled in with values agreed upon by the negotiators. After a successful negotiation, a new contract is created from the model and the negotiated values. Subsequent sections detail the negotiation process itself. Organization of the Negotiation. A negotiation process involves two or more negotiators. One of them is the leader. There is a notary responsible for bureaucratic chores (e.g., constructing the ?nal contract) or acting as a trusted third-party (e.g., to control ballots). These players exchange information within a negotiation process through asynchronous messages. The messages may be peer-to-peer or broadcasted. A contract negotiation has several phases, including leader election, objective and restriction announcement, property negotiation, commit attempt, and contract construction. These phases are described in [4], the core being property negotiation. This is the focus of this paper and is presented in the following sections. Core Negotiation. There are three generic styles of negotiation: ballots, auctions and bargains. Ballots are used when the negotiators have to reach consensus on a property’s value. In our example, most of the farms must agree upon a value for QMAX. Auctions are used when there is competition among di?erent negotiators in order to bind a property to a value. This is the case of property PRICEBERRY. Bargains are used when there are two negotiators and they want to interact to reach a value that is convenient for both. For instance, in our example the dairy and Farm 4 interact to ?nd a consensual value for PRICEPEACH. All these styles may be used to negotiate a single contract. The negotiation styles are built on a few negotiation primitives, i.e., types of messages exchanged among the participants. These primitives rely on two basic mechanisms: request for proposals (RFP) and o?ers. The following paragraphs describe RFPs and o?ers. Subsequently, the negotiation primitives and the negotiation styles are shown in a few short examples. An RFP is an invitation. A negotiator A sends an RFP to a negotiator B asking for a value for one or more properties. An RFP may prescribe some restrictions on the expected answer and may also bind the value of other properties. For instance, the dairy intends to buy 100kg of peaches from Farm 4. Thus, it sends an RFP to Farm 4 assigning the value 100 to QPEACH and asking a value for PRICEPEACH. An o?er is a promise. A negotiator who wants to assign a value to one or more properties sends an o?er to another negotiator. The o?er indicates the properties the ?rst negotiator is interested in and the values it proposes for them. If the other negotiator accepts such o?er, both negotiators are committed to the proposed values. A negotiator can answer to an RFP by sending back an o?er that proposes values for the desired properties and that complies with the restrictions indicated in the RFP. If a negotiator is not interested in a RFP, it replies to the RFP by indicating that it will not send an o?er. Conversely, a negotiator who receives an o?er agrees upon it, disagrees, or proposes a counter-o?er. Thus, two negotiators may engage in a cycle of counter-o?ers until they reach an agreement or give up. To sum up, o?ers and RFPs have two distinguishing di?erences. First, all properties included in an o?er must have their values de?ned in advance, the other party may only agree or disagree on those values. In contrast, an RFP may have properties with prede?ned values, but also, at least, one unbound property, whose value is subject to negotiation. Second, the party that issues an o?er is committed to it, i.e., if the other party agrees upon, the issuer must honor it. In contrast, the party that issues an RFP is neither obliged to keep the RFP valid nor to accept any o?er in response to it. That is, an RFP does not imply any level of commitment. The following describes how RFPs and o?ers are exchanged by means of speci?c messages, and how such messages are organized into the three negotiation styles mentioned before (bargains,

32

ballots and auctions). In these examples, any text enclosed by triangles represents an RFP, and text enclosed by squares represents an o?er. They do not show all the information they carry, but only the information relevant for the examples. Messages are numbered and show the sender (e.g., dr:) for convenience. Figure 2 shows the dairy (dr) and Farm 4 (f4) bargaining the price of a certain amount of peaches. In the ?rst message (1), the dairy sends an RFP to farm f4 asking for a proposal for property PRICEPEACH, considering that property QPEACH has value 100. Next, (2) f4 o?ers 108 for that property. However, the dairy does not agree upon such value and (3) sends a counter-o?er proposing 92. Finally, (4) f4 agrees upon the proposed value. This sequence of counter-o?ers may be arbitrarily long and may also be ?nished without agreement by sending a proposal no agree message.
new rfp ?PRICEPEACH?; QPEACH=100? new o?er PPRICEPEACH=108; QPEACH=100P new o?er PPRICEPEACH=92; QPEACH=100P proposal agree PPRICEPEACH=92; QPEACH=100P Fig. 2. Bargain

1. 2. 3. 4.

dr: f4: dr: f4:

send send send send

f4 dr f4 dr

The next two examples show how the notary cooperates in the negotiation process. Figure 3 presents the negotiation of property QMAX. This property requires that most of the farms agree on a value, thus a ballot is performed under control of the notary. First, the dairy asks the notary to conduct the ballot. It informs the issue to be voted and the possible votes. In the example, the issue is an o?er proposing the value 187 to property QMAX and the alternatives are agree (VOK) or disagree (VNOK). Next, (2) the notary (nt) acknowledges to the leader (i.e., dr) that it will conduct that ballot. The notary (3) broadcasts the issue to be voted to the negotiators. Each negotiator (47) sends its vote to the notary. Finally, the notary counts the votes and (8) broadcasts the result informing that the issue was approved and the number of votes each alternative has received. There are other messages to inform that the issue was not approved or that a tie has happened.
send nt control ballot PQMAX=187P VOK,VNOK send dr will conduct PQMAX=187P VOK,VNOK broadcastvoting PQMAX=187P VOK,VNOK send nt vote VOK send nt vote VOK send nt vote VNOK send nt vote VOK broadcastbal res BAPPROVED VOK:3, VNOK:1 Fig. 3. Ballot

1. 2. 3. 4. 5. 6. 7. 8.

dr: nt: nt: f1: f2: f3: f4: nt:

The scenario shown in Figure 4 follows a variant of an English auction that aims at minimizing the value of PRICEBERRY. The maximum price is 180. Thus, (1) the dairy asks the notary to advertise an auction for an RFP and wants the notary to collect at most four answers within 30 seconds. The notary (2) broadcasts the RFP and waits as requested. The farms receive the RFP and (3-6) send o?ers to the notary in response. A negotiator may decline an RFP by returning a no offer answer. The notary collects the answers and (7) sends them to the dairy. The labels O1 ,...,O4 stand for the o?ers from f1,...,f4, respectively. Now, the leader chooses the best o?er (PRICEBERRY=112) and (8) asks the notary to start a new auction round, restricting the expected price. This process is repeated (9-12). Eventually none of the negotiators is interested in o?ering a lower price and all of them answer no offer. Now, the dairy (13) agrees upon the best o?er of

33

the previous round. The dairy also sends a proposal no agree message to all defeated o?ers (not shown in the ?gure).
1. dr: send nt ?rst answers 4 30 ?PRICEBERRY?≤180; QBERRY=100? 2. nt: broadcastnew rfp ?PRICEBERRY?<180; QBERRY=100? 3. f1: send nt new o?er PPRICEBERRY=160; QBERRY=100P 4. f2: send nt new o?er PPRICEBERRY=112; QBERRY=100P 5. f3: send nt new o?er PPRICEBERRY=130; QBERRY=100P 6. f4: send nt new o?er PPRICEBERRY=170; QBERRY=100P 7. nt: send dr collected answers O1 ,O2 ,O3 ,O4 8. dr: send nt ?rst answers 4 30 ?PRICEBERRY?<112; QBERRY=100? 9. nt: broadcastnew rfp ?PRICEBERRY?<112; QBERRY=100? 10. f2: send nt no o?er 11. f3: send nt new o?er PPRICEBERRY=98; QBERRY=100P 12. ... 13. dr: send f1 proposal agree PPRICEBERRY=47; QBERRY=100P Fig. 4. Auction

The examples given in this section show how the properties of our running example (Figure 1) can be negotiated using di?erent styles of negotiation. However, the style of negotiation has only been described in plain English and can be interpreted in di?erent ways. Therefore, we formalize the di?erent styles and primitives in terms of CPNs.

4

Modeling the SPICA Negotiation Protocol in CPNs

This section describes how the protocols presented in Section 3.3 can be modeled as Colored Petri Nets (CPNs) using CPN Tools. The Petri net model is composed of 31 subnets (19 if replicated instances are not counted). The top-level page is presented in Figure 5. In total there are about 300 places and 200 transitions. This model assumes the absence of exceptions (e.g., communication infrastructure is reliable) and the diligence and fairness of the negotiators. Thus, the negotiators will always receive and answer properly any message from the leader or the notary. The model also makes some simpli?cations. For instance, RPFs and O?ers can be used to announce an auction, however, the model only accepts RFPs. Section 4.1 presents the most important color sets used in the model. Section 4.2 shows a model for the overall negotiation process. Section 4.3 details the subnets for bargains. Finally, the models for ballots and auctions are only brie?y described because of space limitations (Section 4.4). 4.1 Color Sets

This section presents the main color sets used in the model. The names of the properties in the contract model are represented by the PropertyName color set. The color set NegId is used to identify and to address negotiators: L stands for the leader and F1...F4 refer to the farms; EVERYBODY stands for all farms; NO BODY is an invalid value for initialization purposes.
colset PropertyName = with QMAX | MINPRICE | QBERRY | PRICEBERRY |QPEACH |PRICEPEACH; colset NegId = with L | F1 | F2 | F3 | F4 | EVERYBODY | NO BODY;

The Property color set represents the properties being negotiated. It consists of a property name (PropertyName), a status code that indicates if it was agreed upon (PropAgreement), the Value agreed upon (if any), and the list of the negotiators who had agreed upon this value LstNegId. PropAgreement is set to AGREED to indicate that the property was negotiated and the partners have agreed upon a value; NOT AGREED is the opposite, and IN NEGOTIATION indicates that the property was not negotiated.

34

colset colset colset colset

LstNegId = listNegId; PropAgreement = with AGREED | NOT AGREED | IN NEGOTIATION; Value = INT; Property = product PropertyName * PropAgreement * Value * LstNegId;

The leader builds a negotiation plan (NegoPlan) before it starts negotiating the contract’s properties (Section 4.2). A negotiation plan is a table whose entries describe which properties will be negotiated together (PropertyNameLst) and the style of negotiation to be used (TypeNego). For instance, in our example, properties QBERRY and PRICEBERRY are negotiated together using an auction (AUC). Other styles of negotiation are ballots (BLT) and bargains (BARG).
colset colset colset colset TypeNego = with BLT | AUC | BARG; PropertyNameLst = list PropertyName; NegoPlanItem = product TypeNego * PropertyNameLst; NegoPlan = list NegoPlanItem;

Negotiators exchange RFPs and o?ers within a negotiation. An RFP has a unique identi?er (RfpId), and references to the originator (From) and recipient (To) of the request. The recipient may be a single negotiator (e.g., F1) or EVERYBODY which causes the RFP to be broadcasted.
colset colset colset colset colset colset colset RfpId = MessageId; From = NegId; To= NegId; Operator = with GE | LE | EQ | OM | NEQ; Restriction = product PropertyName * Operator * Value; LstRestriction = list Restriction; Rfp = product RfpId * From * To * LstRestriction * AuctId;

The RFP also has a list of restrictions (LstRestriction) on the properties values. For instance, the list of restrictions for the RFP of the initial message in Figure 4 should be:
[ (QBERRY,EQ,100), (PRICEBERRY,LE,180), (PRICEBERRY,OM,0) ]

Note that OM stands for “o?er me”, and the value after it is meaningless.4 Thus the negotiator is expecting an o?er for PRICEBERRY, provided that it is less or equal (LE) than 180. The other operators are great or equal (GE), equal (EQ), and not equal (NEQ). The value for QBERRY is already bound by the RFP and the recipient must agree on it. An RFP may be used in an auction. If so, the auction identi?er (AuctId) is also set. An o?er may be an answer to a previous RFP or to another previous o?er. Thus, ParentId relates the o?er to the previous RFP. The answer to an RFP can be a No O?er. This means that the negotiator is not interested in sending an o?er for such RFP. In this case, NoOffer is set. The o?er identi?es its originator and recipient to be an RFP (From and To). When a negotiator receives an o?er, it evaluates it. If the negotiator agrees upon the received o?er, it assigns the value OK to ?eld Eval; otherwise, it assigns the value X to it. In an auction, the best o?er of the current round is marked with NR (New Round), indicating that a new auction round should start. When an o?er is created, the Eval ?eld is set to NE (Not Evaluated). PropertyLst has all the properties being negotiated. This list must contain all properties referenced by a previous RFP (if any). The negotiator that issued the o?er may accept a subsequent counter-o?er by setting CounterOfferAllowed to true. Note that in an auction (Section 4.4) it is always set to false. ParentIsRfp is set to true whenever the o?er answers an immediate previous RFP. Finally, an o?er has a unique identi?er (OfferId).
colset ParentId = MessageId; colset Eval= with OK | X | NE | NR; colset NoO?er = int with 1..0; colset PropertyLst = listProperty; colset CounterO?erAllowed = BOOL; colset O?er = product ParentId * NoO?er * From * To * Eval * PropertyLst * CounterO?erAllowed * ParentIsRfp * O?erId;
4

Note that the union type could be used here. However, for reasons of simplicity we did not do so.

35

Other colors used in the model that are speci?c to di?erent negotiation styles will be described when needed. 4.2 The Overall Negotiation Process

Figure 5 shows the main net of our model. The negotiation process aims at assigning values to properties. The properties to be negotiated are in the place ToNegotiate. Broadly speaking, the leader builds a negotiation plan (see transition PlanHowToNegotiate). Then, the leader follows this plan and coordinates the negotiation. At the end, properties are grouped based on whether they were agreed on or not (see places Agreed and NotAgreed). Some properties may fail to be negotiated, e.g., when no negotiator is interested in an auction. Such properties are put in the place NotNegotiated. If all properties were successfully negotiated, a new contract can be built. This last step is out of the scope of this paper.

Separate ToNegotiate PropertyNameLst propts 1`[QMAX,MINPRICE,QBERRY,PRICEBE 1`[QMAX,MINPRICE,QBERRY, RRY,QPEACH,PRICEPEACH] PRICEBERRY,QPEACH,PRICEPEACH] 1 [ni_type(negit)=BLT] ByBallot ni_ro(negit) PlanHowToNegotiate negit NegotItem build_nplan(propts) [ni_type(negit)=AUC] Ready to negit ByAuction negotiate ni_ro(negit) negit [ni_type(negit)=BARG] ByBargaing ni_ro(negit) PrepareNegotiation b 1`() New Negotiation 1 Item 1`() UNIT new_try(ns) np_prepare_neg(plnit) [try_new_strategy(ns)] TryNewStrategy NewStrategy ns NewStrategy ns [not (try_new_strategy(ns))] giveup givenup_offer(ns) ToBargaing RfpOrOffer negit Bargain Proces Bargain ReevaluateStrategy [offer_disagreed(or)] NotNegotiated np_reeval(or) Property ToBallot RfpOrOffer negit Ballot Process ToBallot () np2 or () or or [offer_agreed(or)] ToAuction RfpOrOffer negit Auction Process Auction NegotiatedOffer NotAgreed Offer or Property Offer np1 or Offers Agreed Property SeparateProperties

[of_nooffer(or)]

PlanedNegotiation NegoPlan plnit::negpln negpln

()

Fig. 5. Negotiation Process (NegotiateProperty page)

The negotiation plan for our example is shown in Figure 6. It shows that the leader will ?rst negotiate property QMAX using a ballot, then MINPRICE. In the third step, it will negotiate properties QBERRY and PRICEBERRY by an auction. Finally, QPEACH and PRICEPEACH will be negotiated through a bargain. Note that each step uses one negotiation item and starts after the previous one has ended (notice place NewNegotiationItem). Each negotiation style (bargain, ballot, or auction) is started by sending the ?rst RFP or o?er to the corresponding subnets (substitution transitions BallotProcess, AuctionProcess and BargainProcess). To enable reuse, a new color set (RfpOrOffer) is introduced and used in places where tokens represent RFPs or o?ers. The negotiation is carried out by the three subnets shown in Figure 5. These subnets deliver back the o?ers that were agreed upon and those that were not. In the latter case, the leader may change the negotiation strategy (transition ReevaluateStrategy), even changing the negotiation style, and submit them again to be negotiated.
Style BLT BLT AUC BARG Properties [QMAX] [MINPRICE] [QBERRY,PRICEBERRY] [QPEACH,PRICEPEACH]

1. 2. 3. 4.

Fig. 6. Negotiation plan for the running example

36

Figure 7, shows the tree view of all subpages. Figure 7.a depicts the topmost net and the three main subnets. Figures 7.b to 7.d detail these subnets. The nodes are named after the page names, and a number in front of the name denotes the number of replications of this page (if any). For instance, there are four replications of ProcessRfp within page AuctionNegotiators (Figure 7.b). Each node is annotated with a pair P:X T:Y. The ?rst stands for the number (X) of places (P) in that page and the latter, the number (Y) of transitions (T), e.g., the page BargainNegotiators has 10 places and 6 transitions ((Figure 7.d)). The paper only shows the underlined pages.

Fig. 7. Tree view: (a) topmost page and its main subpages; (b)-(d) subpages are detailed

4.3

Modeling Bargains

A bargain is characterized by a cycle of o?ers and counter-o?ers. The negotiators end up agreeing upon an o?er or they give up. Figure 8 shows the subnet that models the bargaining process. The RFP or o?er to be bargained enters the subnet via place ToBargain. The leader directs this RFP (or o?er) to the other negotiators by putting it in place RfpToNegotiators (or OfferToNegotiators). The negotiators can make counter-o?ers by putting o?ers in the place OfferToLeader. Leader and negotiators may engage in a cycle of counter-o?ers until one of them agrees upon the o?er or gives up the bargain. In both cases, the partner places an acceptance noti?cation in the place NotificationToNegotiators or NotificationToLeader. An acceptance noti?cation is an o?er with special settings, which is denoted by the Eval ?eld. At the end, the leader puts the negotiated o?ers in the place OfferNeg. Figures 9 and 10 detail the substitution transitions Leader and Negotiators, respectively. Figure 9 shows how the leader develops the bargain and Figure 10 shows how the negotiators react to it. The latter ?gure also shows how RFPs and o?ers are processed in a bargain. Figure 9 shows a few design directives used in the model. First of all, the messages were modeled as transitions. The ?ring of such transitions means that a message is sent, broadcasted, or received. The transitions are named after the message. Pre?xes are used to identify whether the data was sent (s ), broadcasted (b ) or received (r ). For instance, the transition named b new rfp (Figure 9) means that the message new rfp was broadcasted to the negotiators. There are transitions not related to exchange of messages. The second design decision that should be noted is that data conveyed by messages are modeled as tokens, e.g., the place ToBarg (Figure 9) stores the RFP or o?er that starts the bargaining process. When there is an RFP to be negotiated in place ToBarg (Figure 9), the leader sends or broadcasts a new rfp message that conveys such RFP. This is represented by transitions s new rfp and b new rfp, respectively. After a few ?rings, such an RFP will be available to the other negotiators in the place RFP (Figure 10). Similarly, when there is an o?er to be negotiated, the leader sends or broadcasts it. It will be available to the negotiators via place OFFER fr LEADER (Figure 10).

37

RfpToNegotiators Rfp OfferToLeader ToBargain In RfpOrOffer Leader Offer OfferToNegotiators Offer NotificationTo Negotiators Offer OfferNeg Out Offer NotificationToLeader Offer BargainNegotiators Negotiators

BargainLeader

OffersNegotiated Offer

Fig. 8. Bargain subnet. Cycle of counter-o?ers is emphasized.

[is_rfp_to_broadcast(ro)] b_new_rfp ro ro ToBarg In RfpOrOffer ro ro s_new_offer1 [is_offer_to_send(ro)] [is_offer_to_broadcast(ro)] b_new_offer or [is_no_offer(or)] or or OfferReceived In Offer or r_no_offer f_leader_anl_of(or) or analyze ResAnalysis or OffersRcvd s_proposal_no_agree Offer [offer_disagreed(or)] or AgreementNotification In or Offer [offer_agreed(or)] r_proposal_agree r_proposal_no_agree or or OfferNegot Out Offer [offer_disagreed(or)] or Offer or or [offer_agreed(or)] s_proposal_agree or get_offer(ro) [offer_not_eval(or)] s_new_offer2 or get_offer(ro) NewOffer Out Offer s_new_rfp [is_rfp_to_send(ro)] get_rfp(ro) get_rfp(ro) NewRfp Out Rfp

[not(is_no_offer(or))] r_new_offer3 or

or

NotifyAgreement Out Offer

Fig. 9. BargainLeader subnet

When the other negotiator(s) receive(s) an RFP (in the place RFP, Figure 10), the answer to the leader is put in the out-port OFFER to LEADER. The negotiator(s) receive(s) o?ers from the leader through the in-port OFFER fr LEADER. Such an o?er may be a response to a directly preceding RFP. In this case, the o?er passes through the Process RFP (Bargain) subnet, but is handled by the Process Offer (Bargain) subnet. The arriving o?er should also be a new o?er or a counter-o?er from the leader. In both cases, the o?er goes directly to the Process Offer (Bargain) subnet. An agreement noti?cation from the leader arrives via the port AgrNotfFrLeader and may follow two paths: (a) it is directed to Process RFP (Bargain) subnet, when the leader immediately agreed upon the ?rst o?er sent by the negotiator, or (b) the noti?cation is directed to the Process Offer (Bargain) subnet. Figure 10 shows neither individual negotiators nor makes a distinction whether the messages were sent or broadcasted. These details are presented in Figure 11. An RFP is directed to the corresponding receiver or broadcasted to all negotiators. Note that the answers of each negotiator are joined in one respective single place. The subnet for Process Offer (Bargain) is designed in a similar way.

38

RFP In Rfp [parent_is_rfp(or)] RelatedToRfp1 or CounterOffer1 Offer

Process RFP (Bargain)

OFFER_to_LEADER Out Offer

ProcessRfpBarg

Offer Offer

or or

AgreementNotification Offer

Process Offer (Bargain)

NOTIFYLEADER Out Offer

OFFER_fr_LEADER In Offer AgrNotfFrLeader In Offer

NotRelatedToRfp1 [not (parent_is_rfp(or))] or or RelatedToRfp2 [parent_is_rfp(or)]

or ProcessOfferBarg

AgreementNotifification Offer OFFERSNEGOTIATED Out or Offer

[not (parent_is_rfp(or))] or NotRelatedToRfp2

Fig. 10. BargainNegotiators subnet

Figure 12 presents the elementary ProcessRFP. It shows the messages that are received and sent by the negotiator and the function it uses to assess the received RFP (f analyze rfp). Recall that this subnet is used by several negotiators and each negotiator evaluates the RFP di?erently. Thus, the f analyze rfp function actually dispatches the RFP to speci?c functions. For this reason, the token in RFP place is of color RfpXNegId and contains the RFP and the identi?cation of the negotiator it is meant for. Finally, Figure 13 shows the elementary ProcessOffer. New o?ers arrive in the place Offer. Function f analyze offer dispatches it to the correct negotiator. The (dis)agreed o?ers are made available to the partner negotiator through the place AgreeDisagree. They are collected in the OffersNegotiated place. Conversely, the negotiator decides to make a counter-o?er, which is placed in CounterOffer. A No Offer message is just collected (transition r no offer). Agreement noti?cations related to previous o?ers are received in through port AgreementNotification and are also collected. Note that the same patterns of ProcessRfp and ProcessOffer were applied to subpages at di?erent levels. For instance, Figures 10 and 11 have the same structure of Figure 12.

4.4

Modeling Ballots and Auctions

Figure 14 details the BallotProcess subnet referred to in Figure 5. It shows the leader, the notary and the negotiators interacting in a ballot process. The leader role is detailed in Figure 15. Note that the leader asks the notary to conduct the ballot (transition s control ballot), receives the notary’s acknowledgment (transition r will conduct) and, eventually, receives the result of the ballot (r bal res). The notary role is detailed in Figure 16. First, the notary receives a message from the leader to conduct a ballot (transition r control ballot). It accepts the job (transition s will conduct) and broadcasts the issue to the negotiators (b voting). The notary receives votes (r vote) or vetoes (r veto). In case it does not receive any veto, the notary counts the votes and broadcasts the result (b bal res). Otherwise, the notary informs all participants that a veto has occurred. However, none of the farms in the running example has veto power. Thus, the veto scenario does not occur. The BallotNegotiators subnet (not shown) directs the issue to be voted to each negotiator, collects their votes and, eventually, sends them the ballot result. Figure 17 shows how a negotiator reacts when it receives a vote request. Basically, it analyzes the issue and decides either to vote or to veto (see function vrr analyze). Its choice is sent to the notary (s vote or s veto). Eventually, the negotiator receives the ballot result (r bal res).

39

[rfp_to(rfp)=EVERYBODY] broadcast rfp RFP In Rfp rfp s1r (rfp,F1) (rfp,F1) r1 RfpXNegId co1 Offer an1 Offer (rfp,F2) r2 RfpXNegId co2 Offer or an2 Offer (rfp,F3) r3 RfpXNegId or co3 Offer or an3 Offer (rfp,F4) [rfp_to(rfp)=F4] s4r (rfp,F4) r4 RfpXNegId s4rco [of_to(or)=F4] AGREEMNOTIF In Offer or s4ran [of_to(or)=F4] or or co4 Offer an4 Offer ProcessRfp OFFERNEGOT Out Offer Proc Rfp 4 Proc Rfp 3 ProcessRfp EVALCO Out Offer Proc Rfp 2 ProcessRfp Proc Rfp 1 OFFER Out Offer

[rfp_to(rfp)=F1] or s1rco or

[of_to(or)=F1] or s1an [of_to(or)=F1] rfp or (rfp,F2)

s2r

[rfp_to(rfp)=F2] or or s2rco [of_to(or)=F2]

COUNTEROFFER In Offer

or

s2ran [of_to(or)=F2] s3r

rfp

(rfp,F3)

[rfp_to(rfp)=F3] or s3rco [of_to(or)=F3] or s3ran [of_to(or)=F3] or rfp

ProcessRfp

Fig. 11. ProcessRfpBarg subnet

The notary also collaborates in an auction. Figure 18 shows an auction step being directed to negotiators. Each negotiator uses ProcessRfp subnet to react to a negotiation step. Note that this is the same subnet used in bargains. The other subnets are not presented for the sake of brevity.

5

Implementing the Negotiator’s Strategies

To simulate the model, we con?gured the CPN for the scenario presented in Section 3.2. For each property, each negotiator (including the dairy) has a value (or a range of values) it considers a “good deal” and for which it will always agree upon. There are also values the negotiator will never agree upon. Values in-between will be accepted with speci?c probabilities: the nearer to the expected value, the higher the acceptance probability. Each farm has also distinctive characteristics, mainly its production capability for each product (Figure 19). These characteristics in?uence its decision. For instance, Farm 1 weekly produces a large amount of milk (400 liters). Thus, it tends to agree upon high values for QMAX. However, Farm 2 has a low production capacity (50 liters). It will not agree upon high values for QMAX for fear that the week quota should be ful?lled by the other farms. According to the model presented in Figure 5, the leader may have several strategies to negotiate the value of a property. When a negotiation fails, the leader can try again negotiating that property using a di?erent strategy. The simulation uses this capability to negotiate properties QMAX and MINPRICE. For instance, the leader has a lower and an upper limit to QMAX (QMAX min and QMAX max). It starts in the middle point between these values and submits increasing values to successive ballots. If the proposed values reach unsuccessfully the upper limit, the leader submits successive decreasing values starting from the middle point.

40

[not(is_no_offer(or))] rfp_neg RFP In RfpXNegId f_analyze_rfp(rfp_neg) r_new_rfp Answer Offer or or s_new_offer or OfferOrNoOffer or Out Offer

[is_no_offer(or)] s_no_offer

CounterOffer In Offer

or

CounterOfferReceived

or

EvaluateCounterOffer Out Offer

[offer_agreed(or)] or r_proposal_agree or

AgreementNotification In Offer or

[offer_disagreed(or)] r_proposal_no_agree or

Negotiated Out Offer

Fig. 12. Elementary Process RFP (ProcessRfp subnet)

[is_no_offer(or)] (or,neg) Offer (or,neg) In OfferXNegId [not(is_no_offer(or))] r_new_offer Answer r_no_offer or NoOffer Offer

[offer_not_eval(or)] s_new_offer or [offer_agreed(or)] or s_proposal_agree or or or AgreeDisagree Out Offer or CounterOffer Out

Offer

Offer

(or,neg)

s_proposal_nagree [offer_disagreed(or)] f_analyze_offer(ofr_neg) or or

OfferReceived

ofr_neg

AnalyzeOffer

OfferXNegId [offer_agreed(or)] or AgreementNotification In Offer or r_proposal_no_agree [offer_disagreed(or)] r_proposal_agree or or OffersNegotiated Out Offer

Fig. 13. Elementary Process O?er (ProcessO?er subnet)

The dairy is interested in buying 100kg of peaches weekly. Only Farm 4 can a?ord such amount. Thus, they engage in a bargain that comprises two properties: QPEACH (bound by the leader) and PRICEPEACH. The dairy has two parameters that guide the negotiation. PEACH PRICE GD LD is a threshold value, i.e., values lesser or equal to it are considered a good deal (cheap enough) and are always accepted. PEACH PMAX LD is the opposite, values higher than it are refused. The dairy starts the bargain by sending an RFP to Farm 4 assigning the value of 100Kg to QPEACH and requesting a value for PRICEPEACH. Eventually, the dairy receives an o?er from Farm 4. The closer the o?ered price is to the “good deal”, the higher the probability of being accepted. If not accepted, the dairy will choose (by chance) between refusing the o?er or making a counter-o?er. If it chooses to make a counter-o?er, the value for a future counter-o?er uses the value of PEACH PRICE GD LD (e.g., 10) as a reference point: if the proposed value (e.g., 14) is at a “distance” d (i.e. 4), beyond the “good deal”, the counter-o?er will be exactly at the same “distance” before the “good deal” (i.e., 6). Similarly, Farm 4 has two parameters to negotiate PRICEPEACH. The value it considers a good deal is PEACH PRICE GD F4. Values higher than it are always accepted. PEACH PMIN F4 is the opposite (too cheap), values lower than it are always rejected. The diagram in Figure 20 depicts Farm 4’s decision table. GD stands for PEACH PRICE GD F4; MP, for PEACH PMIN F4; numbers above the line are fractions (in percentage) of GD; and numbers below the line are acceptance probabili-

41

AskNotary Ballot Leader Controls Ballot NotaryAck Notary Controls Ballot

BallotBroadcasted Ballot VoteRecvd Vote ResltBroadcstd Negotiators Vote

ToBallot In RfpOrOffer

BallotLeader br BR4 BallotResult

Ballot

BallotNotary BallotResult br br tb6 br_offer(br) OfferVoted Out Offer br

BallotNegotiators

BallotResult BallotResult

Fig. 14. BallotProcess subnet

ro ToVote In RfpOrOffer

s_control_ballot

bl_control_ballot(ro)

AskedNotary Out Ballot

bl_control_ballot(ro) bal1 bal2

AckfromNotary In Ballot

r_will_conduct bal1 WaitingResult Ballot bal

WaitingAck Ballot

br BallotResult r_bal_res In BallotResult

br

Result BallotResult

Fig. 15. BallotLeader subnet

ties. For instance, if Farm 4 receives an o?er whose value is at least 90% of GD, but no bigger than GD, it will accept the o?er with probability 0.8. Other negotiators use similar approaches, but with di?erent parameter values. They are not described here for brevity. Recall Figure 5. One execution of the model should produce as a result of a negotiation the markings shown in Figure 21. Note the agreed values for properties MINPRICE, QMAX and PRICEBERRY. There was no agreement on the value for PRICEPEACH.

6

Discussion

This section discusses what we have learnt from the modeling process and some results obtained from simulations and state space analysis. The construction of the model led us to new insights into the modeling process and into our negotiation protocol. We followed a top-down approach to model the protocol. At the end, we noticed that there were di?erent subnets to handle RFPs in auctions and in bargains. This also happened to o?ers. Thus, we updated our model using a bottom-up approach: we focused on the handling of RFPs and o?ers and how to combine them to allow di?erent styles of negotiation (ballots, auctions, and bargains), e.g., compare Figures 11 and 18. This gave us a better understanding about the role of RFPs and o?ers within our protocol. This allowed us to replicate elementary structures in higher subnets. For instance, compare Figures 10, 11 and 12. Note that they have identical interfaces, and the ?ow of information is the same.

42

ToVote In Ballot AcceptConduct Out Ballot BroadcastBallot Out Ballot

bal

r_control_ballot bal

bal

AcceptedBal Ballot

bal

s_will_conduct

bal

Announce Ballot

bal bal b_voting (bal,[]) [not(is_veto(vt))] vt Vote In Vote vt [is_veto(vt)] r_veto r_vote (bal1,vt::vlst) bb BallotBox BallotResult ReceivedVeto br (bal1,vlst) ExpectingVotes UNIT () CanCount

b b b b

votes_counted

bb bn_count(bb)

bn_ballot_vetoed(bb,vt) br

BallotResult BallotResult br b_bal_res

Ballot Out BallotResult br

b_bal_res_vetoed

Fig. 16. BallotNotary subnet

vrr_analyze(balneg) VoteRequest In BallotXNegId Vote balneg r_voting

[not(is_veto(vt))] vt s_vote vt ()

Out Vote Vote

IssueAnalyzed vt s_veto [is_veto(vt)] vt () WaitingResult UNIT ()

ReceivedResult In BallotResult

br

r_bal_res br BallotResult Ballot Result

Fig. 17. VotingRequestReceive subnet

The modeling process also helped us to improve the SPICA protocol. It showed that the protocol lacked negotiation plans and also that it should allow alternative strategies to negotiate a property. We used CPN Tools to build the model. CPN Tools helped us in several ways. First, calculating the model’s state space was a hard job. Several simpli?cations and processing hours would be needed to produce a full state space. This made clear that the protocol’s implementation will demand extreme care. Second, it helped us to assess the correctness of the model, especially by indicating some unexpected dead markings. Third, it allowed to simulate the running example presented in Section 3.2. State space analysis. The calculation of the state space was a non-trivial task for several reasons. The model’s ?rst version aimed at producing actual values for the properties, e.g., a negotiation should come out with the value 187 for property QMAX in our running example. This easily produces a huge state space. We tried several alternatives to calculate a full state space. First, we created a new model version with some simpli?cations. The allowed values for properties were restricted (e.g., -1..+1) and the decisions were not based on the o?ered values, but taken by chance. However, these restrictions did not make possible the calculation of a full state space, even spending several processing hours of a Pentium 4 (3GHz, 1Gb). Then, we split the model

43

RFP In Rfp

rfp

aun1

(rfp,F1)

Rfp1 RfpXNegId

ProcessRfp Process Rfp 1 n1 co1 Offer ec1 ng1 Offer

Answers Out Offer

Offer Offer Process Rfp 2

or

ProcessRfp (rfp,F2) Rfp2 RfpXNegId

n2 ng2 Offer

or

co2 Offer

ec2

(rfp,F3)

Rfp3 RfpXNegId

Offer Offer ProcessRfp Process Rfp 3 n3 ec3 ng3 Offer or aun2 or or

co3 Offer (rfp,F4)

Offer Offer

Rfp4 RfpXNegId co4

ProcessRfp Process Rfp 4 n4 ec4 Offer Offer

Offer

ng4 Offer

Notifications In Offer

Fig. 18. AuctionNegotiators subnet

Production Capacity Milk (liters) Blueberry (kg) Peach (kg)

F1 400 100 50

F2 50 200 30

F3 200 150 80

F4 150 300 100

Fig. 19. Production capacity

into tree distinct models – one for auctions, another for ballots and another for bargains – and deleted unneeded places and transitions of the main net (Figure 5). For the bargain sub-model, we managed to calculate the full state space. However, this was not possible for the ballot sub-model. Thus, we tried to reduce the number of negotiators by dropping two negotiators, i.e., only the other two remaining negotiators took part in ballots. We succeeded in obtaining a full state space for the reduced ballot sub-model (Figure 22). This analysis showed a few dead transitions, which are caused by two factors: (a) the model’s reduction and (b) some possibilities allowed by the model were not used by the running example. The dead transitions SeparateProperties’not negotiated and SeparateProperties’sp3 are examples for the ?rst factor. A property can be not negotiated only when a negotiator is not interested in an RFP and sends back a No O?er answer. This cannot happen in a ballot. The other transitions are related to the veto power a negotiator may have in a ballot. The farms in our running example do not have such a power.

MP 0

80% 0.2

90% 0.5

GD 0.8

v

v

v

v

1

Fig. 20. F4’s PRICEPEACH decision table

44

Agreed NotAgreed

1‘(QMAX,AGREED,202,[ ]) ++ 1‘(MINPRICE,AGREED,15,[ ]) ++ 1‘(QBERRY,AGREED,100,[F3]) ++ 1‘(PRICEBERRY,AGREED,39,[F3]) 1‘(QPEACH,NOT AGREED,100,[L] ++ 1‘(PRICEPEACH,NOT AGREED,57,[L]) Fig. 21. A negotiation result

Statistics State Space Nodes: 6387 Scc Graph Nodes: 6387

Arcs: 22816 Arcs: 22816

Secs: 26 Secs: 2

Status: Full

Boundedness Properties (Omitted) Home Properties Home Markings None Liveness Properties Dead Markings 8 [6387,6386,6385,6380,6372,...] Dead Transition Instances BallotNotary’b bal res vetoed 1 SeparateProperties’not negotiated 1 VotingRequestReceived’s veto 1 Live Transition Instances None

BallotNotary’r veto 1 SeparateProperties’sp3 1 VotingRequestReceived’s veto 2

Fig. 22. State space report for the ballot sub-model (excerpt).

For the auction sub-model, even making such reductions, it was not possible to produce a full state space.
Statistics State Space Nodes: 241569 Scc Graph Nodes: 241569

Arcs: 1134868 Arcs: 1134868

Secs: 43000 Secs: 190

Status: Partial

Fig. 23. State space report for the auction sub-model (excerpt).

Model correctness. CPN tools helped us to assess the correctness of the model. It showed a few expected dead markings (e.g., in those states that collect negotiated o?ers), but also unexpected ones. For instance, one con?guration did not replace the token in NewNegotiationItem (Figure 5) hindering the execution of the next negotiation round. CPN Tools also highlighted another synchronization problem. It may happen when a negotiation fails and the convenience of a new strategy is evaluated. The solution found is based in speci?c characteristics of the running example and cannot be generalized. Thus, such synchronization issues must be better addressed in future versions of the model. Simulation. We used CPN tools to run simulations and to produce performance reports. The generated performance report helped us to assess the correctness of the model. We wanted that: (a) new strategies were tried, (2) distinct simulation produced di?erent outputs, (3) all properties reached the ?nal places Agreed, NotAgreed or NotNegotiated (Figure 5), (4) eventually, some auction failed (this guarantees that a property is put in the NotNegotiated place). Figure 24 shows a performance report. Recall Figure 5. Regarding the ?rst concern, a new

45

strategy is tried when transition TryNewStrategy ?res. According to the performance report, this happens, in average, 1.74 times in each simulation run (see line count iid of monitor Count trans occur NegotiateProperty’TryNewStrategy 1). To assess the second concern, three marking size monitors were assigned to the ?nal places (see columns Min and Max of monitors Marking size NegotiateProperty’Agreed 1, Marking size NegotiateProperty’NotAgreed 1 and Marking size NegotiateProperty’NotNegotiated 1). Note that the maximum numbers of tokens observed in each place is greater than zero. This means that eventually a token reached such places. Note also that the minimum number of tokens di?ers from the maximum. It means that the outputs can vary in each simulation. To assess the third concern, we grouped the ?nal places and assigned a monitor (Final places) that counted the total number of tokens in these places. For the running example, the number of tokens in the ?nal places at the end of a simulation must be ever 6. Note that the measures Min and Max for max iid are both 6. This does not guarantee the correctness of the model, however the opposite would show that the model was incorrect. Finally, a transition occurrence monitor was assigned to np2 transition (Figure 5) in order to verify the fourth concern. If an auction fails, this transition ?res. The performance report showed that this transition eventually ?res.

Fig. 24. Performance report

46

7

Conclusion

The paper presented the initial steps aiming at the implementation of our negotiation protocol. First, we modeled the core part of this negotiation protocol using CPN Tools. The goal was to simulate a negotiation for the running example presented in Section 3.2. We used the simulation capabilities of CPN Tools to assess the correctness and the adequacy of the model. Although such simulations cannot prove the correctness of the model, they can, at least, show ?aws in the model. In fact, the simulations helped us to identify problems that could be repaired. Some weaknesses were also identi?ed and will be taken into consideration in the actual implementation of the model. The simulation also helped us in ascertaining that the protocol is suitable to the purposes it is intended for. Although each negotiator used a simple strategy, the negotiation process provided by/observed during the simulation corresponded to our expectations, and reasonable values were produced. We also desired to have a stronger con?dence about the model’s correctness. Thus, we tried to perform state space analysis. We had to simplify the model and even to split it into three distinct sub-models. We managed to obtain full state spaces for the bargain and ballot sub-models, but not for the auction sub-model. Although we did not fully succeed, this process also helped us to identify ?aws in the model. We tried to correct them both in the original model and in the sub-models.

Acknowledgment
This paper is partially supported by CAPES/Brazil under grant 4635/06-0, CNPq WebMaps II Project, and FAPESP.

References
1. Weigand, H., Heuvel, W.: Cross-organizational work?ow integration using contracts. Decision Support Systems 33(3) (July 2002) 247–265 2. Krishna, R., Karlapalem, K., Chiu, D.: An ERec framework for e-contract modeling, enactment and monitoring. Data & Knowledge Engineering 51(1) (oct 2004) 31–58 3. Angelov, S.: Foundations of B2B Electronic Contracting. PhD thesis, Technische Universiteit Eindhoven (2005) 4. Bacarin, E., Madeira, E., Medeiros, C.: Contract e-negotiation in agricultural supply chains. Intl. Journal of Electronic Commerce (2007) http://www.gvsu.edu/business/ijec (to appear). 5. Jesen, K., Kristensen, L., Wells, L.: Coloured petri nets and cpn tools for modelling and validation of concurrent systems. Intl. J. on Software Tools for Technology Transfer 9(3-4) (2007) 213–254 6. Bartolini, C., Preist, C., Jennings, N.: A software framework for automated negotiation. In: SELMAS. (2004) 213–235 7. Chiu, D., Cheung, S., Hung, P., Chiu, S., Chung, A.: Developing e-negotiation support with a metamodeling approach in a web services environment. Decision Support Systems 40(1) (July 2005) 51–69 8. Reeves, D., Wellman, M., Grosof, B.: Automated negotiation from declarative contract descriptions. In: Proc. of the 5th International Conference on Autonomous Agents, Canada, ACM Press (2001) 51–58 9. Henderson, P., Crouch, S., Walters, R., Ni, Q.: Comparison of some negotiation algorithms using a tournament-based approach. In: Agent Technologies, Infrastructure, Tools and Applications for E-Services. Volume 2592 of Lecture Notes in Arti?cial Intelligence. Springer (Jan 2003) 137–150 10. FIPA: Fipa abstract architecture speci?cation. Available at www.?pa.org (2000) 11. Malucelli, A., Palzer, D., Oliveira, E.: Ontology-based services to help solving the heterogeneity problem in e-commerce negotiations. Electronic Commerce Research and Applications 5(1) (2006) 29–43 12. Governatori, G., Dumas, M., ter Hofstede, A., Oaks, P.: A formal approach to protocols and strategies for (legal) negotiation. In: ICAIL. (2001) 168–177 13. Jensen, K.: Coloured Petri Nets. Basic Concepts, Analysis Methods and Practical Use. Springer-Verlag (1997)

47

14. Chen, Y., Peng, Y., Finin, T., Labrou, Y., Cost, S.: A negotiation-based multi-agent system for supply chain management. In Working Notes of the Agents ’99 Workshop on Agents for Electronic Commerce and Managing the Internet-Enabled Supply Chain., Seattle, WA, April 1999. (1999) 15. Liu, L., J, B.: Enhancing the CES Protocol and its Veri?cation. Sixth Workshop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools (2005) 16. Dang, J., Huhns, M.: Concurrent Multiple-Issue Negotiation for Internet-Based Services. IEEE Internet Computing 10(6) (2006) 42–49

48

E?ectiveness of Coloured Petri nets for Modelling and Analysing the Contract Net Protocol
Jonathan Billington and Amar Kumar Gupta
Computer Systems Engineering Centre School of Electrical and Information Engineering University of South Australia Mawson Lakes Campus, SA 5095, AUSTRALIA Email: jonathan.billington@unisa.edu.au, gupay003@students.unisa.edu.au Abstract. The Contract Net Protocol was developed to facilitate contract negotiation in MultiAgent Systems, between an auctioneer and many bidders. It is therefore important to analyse the protocol to ensure that it terminates correctly and satis?es other important properties. There have been few attempts to model and analyse this protocol in the literature. The main paper on its veri?cation, published in 2004, suggests that Coloured Petri nets are inadequate for this task. This seems to be due to a misunderstanding of what Coloured Petri Nets are. The main aim of this paper is therefore to show how Coloured Petri nets can be used e?ectively to model and analyse this protocol. We present a model of the protocol implemented in CPN Tools. The level of abstraction excludes details of the messages communicated between the agents and processing that does not a?ect the operation of the protocol. We analyse the protocol and show that it terminates correctly (there are no deadlocks or livelocks, and the terminal states show that the auctioneer and bidders have consistent states)and that there is no dead code (all procedures are executable). We also demonstrate that the channel bounds and number of terminal states depend linearly on the number of bidder agents participating in the negotiations for up to 6 bidders and conjecture that this is true in general.

1
1.1

Introduction
Background

Planning and task allocation are important activities for most organizations. Task allocation may involve the distribution of tasks among di?erent subcontracting companies. The design and use of protocols to aid the above process is still of great interest to both business and government organizations. In this paper, we attempt to analyse one such protocol, called the Contract Net Protocol [17], which is used in Multi-Agent Systems (MAS) [4] to facilitate agent interaction. This work was motivated by discussions with researchers at the Australian Defence Science and Technology Organisation (DSTO), who are working on the application of multi-agent systems to transport logistics [16]. The Contract Net Protocol involves contracting between agents comprising an auctioneer (the service requesting agent) and a set of bidders (service providing agents). The auctioneer initiates the negotiation process by sending a Task Announcement to a number of bidders, who bid to provide the service or respond with a refusal. After all bids are received, the auctioneer selects the most suitable one (if present) and rejects all the others. The ?rst speci?cation of the Contract Net Protocol was developed by Smith [17]. The protocol has also been adopted by the Foundation for Intelligent Physical Agents (FIPA) [8] and speci?ed using the Uni?ed Modelling Language (UML) [3], but with a minor modi?cation to the one proposed by Smith [17]. The use of the Foundation for Intelligent Physical Agents Agent Communication Language (FIPA-ACL) [7] for message interaction is quite complicated. To overcome this, Perugini [16] presents a new protocol representation, called the Protocol Flow Diagram, and uses it to describe the Contract Net Protocol. We believe it is important to verify the properties of a protocol before implementation [2]. This is very important for the Contract Net Protocol as it is being used as the basis for developing more complex negotiation protocols [16]. Thus we see this work as a necessary ?rst step for analysing more complex agent negotiation protocols.

49

1.2

Related Work

A lot of work has been reported regarding the application of the Contract Net Protocol in di?erent domains (see for example [10, 18]), but there is little work on verifying the properties of the protocol. Nowostawski et al [13] advocate the use of Coloured Petri nets (CPNs) [11, 12] as a modelling technique for agent interaction protocols, using the Contract Net Protocol as an example. Unfortunately, they present an incomplete ‘Coloured Petri Net model for 3 bidders/contractors (their Fig. 7), which is not clear because no net annotations nor declarations are included, so that the CPN just looks like a Petri Net model. Hence it does not specify the behaviour of the protocol. This model re?ects similar behaviour for three di?erent contractors by repeating net structure, which does not take advantage of the power of coloured Petri nets in modelling similar behaviour by using the same net structure with di?erent tokens. Further, there is no discussion of analysis, let alone veri?cation of properties. Paurobally et al [15] represent the Contract Net Protocol (when its messages are expressed in FIPA-ACL) formally in extended Propositional Dynamic Logic and graphically in extended statecharts and prove properties like termination and consistency in beliefs. Based on the (Coloured) Petri net model of [13], Paurobally et al [15] argue that Petri nets are not suited to modelling and analyzing the Contract Net Protocol. The inadequacy of Petri nets for modelling agent interactions has also been discussed in [14]. We believe this is due to a misunderstanding of Petri nets and CPNs in particular, as demonstrated in Chapter 5 of [14]. This has further stimulated us to show that the Contract Net Protocol can be modelled and analysed using Coloured Petri Nets. 1.3 Contribution

In this paper, we present a Coloured Petri Net model of the Contract Net Protocol, based on the Protocol Flow Diagram representation of it in Chapter 4 of [16], and analyse it using state spaces. This paper has a threefold contribution. Firstly, we present, for the ?rst time, an abstract model of the Contract Net Protocol using Coloured Petri Nets that is suited to analysis. Secondly, we analyse the Contract Net Protocol and con?rm the results in [15]. Further, we prove some additional properties of the protocol, including absence of livelocks, and obtain expressions for the number of terminal states and channel bounds, as a function of the maximum number of bidders. We thus demonstrate that Coloured Petri Nets are suited to the modelling and analysis of interaction protocols contrary to the claims made by Paurobally et al [15]. 1.4 Organization

The rest of the paper is organized as follows. Section 2 discusses the main features of the Contract Net Protocol [16], leading to the development of our model in Section 3, which further explains the operation of the protocol. We analyse this model in Section 4. Lastly, Section 5 presents conclusions along with a discussion of future work.

2
2.1

Contract Net Protocol
Time Sequence Diagram Representation

The Contract Net Protocol is illustrated by the three time sequence diagrams shown in Figs. 1 to 3. These diagrams just represent the interactions between the auctioneer and one bidder. The time sequence diagrams use the terminology of Perugini [16] which is di?erent from FIPA’s representation [9]. For instance, the auctioneer replaces the initiator, bidder replaces the participant, and Task Announcement the cfp (call for proposals). The agents (auctioneer and bidder agents) involved in the negotiations are represented by two vertical lines, where

50

Auctioneer
States READY WAIT

Messages

Bidder
States W_TA

Task Announcement

TEBP Bid W_RES BID_RCVD Grant Bid EXIT_C exit_c

Fig. 1. Bidding Process ending in a Contract.

Auctioneer
States READY WAIT

Messages

Bidder
States W_TA

Task Announcement

TEBP Bid W_RES BID_RCVD Reject Bid EXIT_NC exit_nc

Fig. 2. Bidding Process ending Without a Contract.

Auctioneer
States READY WAIT

Messages

Bidder
States W_TA

Task Announcement

TEBP Refuse EXIT_NC exit_nc

Fig. 3. Refusing Process.

51

time increases downwards. The so called ‘speech acts’ (messages communicated between the agents) are represented by arrows between the two vertical lines. The states for the auctioneer and the bidders are given in Table 1. There are ?ve possible states for the auctioneer and for each bidder. The table also de?nes the meaning of each state. READY and W TA correspond to initial states, while (EXIT NC, EXIT C) and (exit nc, exit c) represent the set of terminal states of the auctioneer and bidders respectively. Terminal states of the auctioneer are represented by uppercase letters, whereas the bidders use lowercase. The terminology for terminal states is that used by Perugini [16].
Table 1. Representation of States. Auctioneer Bidders READY (READY to send a Task Announcement) W TA (Waiting for a Task Announcement) WAIT (WAITing for bids) TEBP (Task Evaluation and Bid Preparation) BID RCVD (BID ReCeiVeD) W RES (Waiting for RESult) EXIT NC (EXIT with No Contract) exit nc (exit with no contract) EXIT C (EXIT with Contract) exit c (exit with contract)

2.2

Operation

The auctioneer initiates the negotiation process by broadcasting a Task Announcement to a number of bidders. The Task Announcement contains the details of the tasks to be performed and the deadline for the submission of the bids. On receipt of the Task Announcement, the bidders evaluate the task and then decide whether to bid or refuse. Each bidder must either Bid or Refuse (to bid). The Bid may contain information concerning the price that must be paid to carry out the task, the time required to complete the task and any other aspect that the auctioneer might have asked for in the Task Announcement. The Refuse signi?es that the bidder is not willing to perform the task. As the auctioneer is dealing with a number of bidders, it may receive both Bid and Refuse messages but can only receive one of either from each bidder. In case of a Refuse, the bidder exits the process without a contract, which the auctioneer records. Once a message (Bid or Refuse) is received from all the bidders, the auctioneer starts processing the bids (if any). After the selection of a bid, it sends a Grant Bid message to the concerned bidder and sends a Reject Bid message to the rest of the bidders. The auctioneer may also reject all the bids by sending a Reject Bid to those that have bid. The bidders exit the process with or without a contract on receipt of the Grant Bid or Reject Bid respectively. The three possible scenarios of the negotiation process are illustrated by the time sequence diagrams in Figs. 1 to 3. The ?gures also show the sequence of messages exchanged between the auctioneer and the bidder and the state resulting from their receipt. For instance, the auctioneer changes state from READY to WAIT after broadcasting a Task Announcement, while a bidder that is waiting for a Task Announcement in the state W TA, would change state to Task Evaluation and Bid Preparation (TEBP) on receipt of the Task Announcement. Figure 1 corresponds to the case in which the bidder sends a Bid in response to the Task Announcement. After considering all the bids (not shown in Fig. 1), the auctioneer grants this bid (and no others) by sending a Grant Bid message, resulting in a contract at the end of the negotiation process. This is also re?ected by the terminal states, EXIT C (for auctioneer) and exit c (for bidder). Figure 2 represents a similar scenario where the auctioneer rejects the bid by sending a Reject Bid message and changes state to EXIT NC. At the other end, the bidder in the state W RES changes state to exit nc on receipt of the message. The negotiation ends without a contract as is evident from the terminal states. The third scenario depicted by

52

Fig. 3 is the case when a bidder refuses to bid for the task by sending a Refuse message in response to the Task Announcement sent by the auctioneer. Without communication of any further messages, the negotiation ends without a contract. Since the auctioneer is dealing with a number of bidders simultaneously, the auctioneer may be in several di?erent states (but with respect to di?erent bidders) during the negotiation. Even though the negotiation process with some bidders may come to an end (on submission of a Refuse in response to the Task Announcement), the process would still continue with respect to other bidders.

3

CPN Model of the Contract Net Protocol

In this section we ?rstly detail the assumptions made when creating the model and then de?ne its data structures, before discussing the model’s structure. Then using an equivalent ?at model we describe all the procedures and the operation of the protocol. This allows visualisation of the message ?ows between the auctioneer and the bidders. 3.1 Assumptions

1. All the bidders are known to the auctioneer before the negotiation takes place. This is appropriate for software agents, or a list of preferred suppliers. 2. All the speech acts (Task Announcement, Bid, Refuse, Grant Bid and Reject Bid) are just represented by their names, as other information contained in these messages does not a?ect the protocol’s actions. 3. All the bids are received before the process of selecting a bid occurs. This means that we do not have to model a deadline, and is reasonable for software agents and preferred suppliers. 4. The communication channel is reliable i.e. messages do not get lost but the receipt of messages is concurrent. This could correspond to a Task Announcement being placed on a website, and accessed by the bidders independently. 5. We only consider task allocation, and not any further interaction that may occur after the task has been allocated [16]. 3.2 Declarations

Figure 4, taken directly from CPN Tools, shows the declarations for the CPN model of the Contract Net Protocol. The protocol facilitates interaction between a single auctioneer and multiple bidders. The identity of the bidders is represented by the colour set BDR as can be seen in the declarations (Fig. 4). Its value ranges from 1 to the maximum number of bidders (MaxBdrs). Hence MaxBdrs is a parameter of the model. The e?ect of varying this parameter on the analysis of the model is presented in Section 4. The states of the auctioneer and the bidders are de?ned by the colour sets STauc and STbdr respectively according to Table 1. The state READY (for auctioneer) and W TA (for bidders) corresponds to the initial state of the negotiation process in which the auctioneer is ready to broadcast a Task Announcement and the bidders are waiting for it. EXIT NC and EXIT C represent terminal states of the negotiation process for the auctioneer. EXIT NC indicates that the negotiation has ended without a contract and EXIT C that a contract has been awarded. The same applies for the bidders where the set of terminal states are represented by exit nc and exit c. The colour sets MESauc and MESbdr de?ne the messages communicated from the auctioneer to the bidders (TA, GB, RB) and from the bidders to the auctioneer (BID, REFUSE) respectively. They are de?ned in Table 2.

53

Fig. 4. Declarations for the CPN model of the Contract Net Protocol. Table 2. Messages and their representation in the CPN Model. Message Value in Colour Set MESauc or MESbdr Task Announcement TA Bid BID Refuse REFUSE Grant Bid GB Reject Bid RB

The auctioneer negotiates with a number of bidders simultaneously. Thus we need to associate the auctioneer’s states and messages with the bidder’s identity. This has been achieved by the declaration of the colour sets BDR STauc and BDR MESauc. Because all the bidders are stored in one place, their states and messages are also associated with the bidder’s identity as de?ned by colour sets BDR STbdr and BDR MESbdr respectively. The colour set RESP (RESPonse) is de?ned as an integer which keeps track of the number of responses received. This is needed to detect when all the responses from the bidders have been received. Lastly, the singleton colour set GR1 (GRant only 1) is de?ned to ensure that only one bidder is granted the contract. 3.3 Model Structure and CPN Diagrams

Figure 5 shows the main page of the CPN model of the Contract Net Protocol. It contains 5 places and 4 substitution transitions and provides the main structure for the protocol. The auctioneer’s and the bidders’ states are modelled by the places Auctioneer’s State and Bidders State respectively. They communicate with each other via the abstract communication channel represented by the places AUCTIONEER 2 BIDDERS and BIDDERS 2 AUCTIONEER as seen in the middle of Fig. 5. The place Responses records the number of responses received from the bidders, so that the auctioneer knows when all bids are in. The main actions of the protocol are modelled by the 4 substitution transitions, Send Messages, Receive Messages, Bidding OR Refusing and Receive Responses. The auctioneer’s procedures for sending messages to the bidders are hidden by the substitution transition Send Messages which is expanded in Fig. 6. The transitions Broadcasting TAs,

54

? ?% #???)B??  ! D # ? )28 012 3( 4?0) 33456 ?§?? @5 "  ? " )28 28( '¤ ??? &9? ()(? ?§¨ ??  ??? ?¤ ????

  !???   ??

? ?)28 "#

??8? 'A? #???)B?? ?C D # ?  $% &012 3( 4?0) 33456 ?§7 5 "  $% & " ? " '%%? &? ()(?

??8? 'A? ??? ?¤ ???? ?C ?? 

 ??    !???

? ? $% & "#

'%% '?B ? ??E2? '?B   ??F "

Fig. 5. Main Page of the CPN Model

2 ? § 22? 45 8) §H § @( ? ?¨ $A EFA ? ?E$ ¤ ? 2 ? § 22? 45G)?( § @( ? ?¨ $A EFA ? ?E$ ¤

? ?  ? '$ $  ()

2 ? § 22? 45() § 8@ ? ?¨ # $A EFA ? ?E$ ¤

45 ?4 & 4 ? & ' 23 4 ?

§ @( ? ?¨ $A )A '  ?B @$ ?01

 ?4 ??? ? ? §  § ¤? ¨? ??? ? 8D?(  ¤ ¨ ? ! ??? ? &  ¤ ? 1A

§ 8@ ? ?¨ # $A ) 6(?1 788 9 ? §§8 @? ? ?

& ?$   ? !"#$% ? ? ?

?  !'   ? ?01 ? ! ??? ? 8D?( 7 ¤ ¨ ??? ? ? §  § ¤? ¨?   ?

8@ C

? !"#$% ? ? ?

??? ?  ¤ ??

Fig. 6. Send Messages

55

2!? "34#'5 2!? "3 §  ?06 5  "??  §? '&??  #??$ ¨ ?? "%? $&$?   "??  2!? "3 7' 105   2!? "34#'5

??? §¨?

2!? "3 § 5

"?? 89 ? @ 

???  ???  "?? 89 2!? "3 ? ) 5 A 

§  ? ( 1 ? # )0' 

!? " §?  

??? ??¤???

Fig. 7. Receive Responses

Granting and Rejecting de?ne the rules for broadcasting a Task Announcement, and Grant and Reject Bid speech acts respectively. Receive Responses, shown in Fig. 7, details the process of receiving Bid and Refuse messages from the bidders in response to the Task Announcement, modelled by the transitions Rcv Bid and Rcv Refuse respectively. Similarly, Fig. 8 models the actions taken by the bidders on reception of messages from the auctioneer and Fig. 9 details their bidding and refusing procedures. This structure allows the individual procedures used by the di?erent parties to be de?ned in separate blocks, which makes each individual diagram easier to read. However, the disadvantage is that it is no longer readily apparent how the bidders and auctioneer interact, which is important for understanding how the protocol works. Now that we have introduced the main procedures we would like to describe the model in detail with respect to a ?at model that is equivalent to combining Figs. 6 to 9. This will make it easier to understand the operation of the protocol as described in Section 3.4. Figure 10 shows the CPN diagram for the Contract Net Protocol in a single page which makes it easier to visualise message ?ow while relating it to the protocol’s procedures. With reference to Fig. 10, the auctioneer is modelled on the left, the bidders on the right, and they communicate via two places, AUCTIONEER 2 BIDDERS and BIDDERS 2 AUCTIONEER, which represent a reliable (but not ordered) channel for each direction of communication. The auctioneer is modelled with 3 places, which represent its state (Auctioneer’s State), the number of responses received (Responses) and if a bid has been granted (GRonly1). In contrast, the bidders are modelled with only a single place, (Bidders State), representing the states of each of the bidders. The signi?cance of each place is very brie?y discussed below. Auctioneer’s State: This place stores the states of the auctioneer with respect to all the bidders. It is typed by the colour set BDR STauc (product of BDR and STauc) to identify the state of the auctioneer in relation to a particular bidder. The initial marking of this place is: BDR STauc.mult(BDR.all(),1‘READY). BDR.all is a prede?ned function that returns a multi-set comprising the set of all bidders. BDR STauc.mult is another prede?ned function that returns a product based on the multi-sets speci?ed in its argument, i.e. one appearance of all the bidders and 1‘READY. For this argument, the function returns a multi-set with one appearance of all the bidders in the READY

56

??? ? § ¤4%  ?2 ??? ?  ?3§ ¤

??? ? § ¤

?" ?)??? ?0 #'? 1

# ?? ? ?% ??? ? ?5 ) § ¤ % ??? ? #§ ¤4% ? ¨ ?' $?? ??? ? ?§ ¤¨ $

?"    ? ! ? "" # ?

?% &

#'(

??? ? ?5 ) $§ ¤ %   ? ?? ? ? ??? ? #§ ¤4% ? ??? ? ?§ ¤?

Fig. 8. Receive Messages

($? %) ¨21 ($? %)0 ?1 "

¨??? ??§

($? %) ¨ 1

¨???? %¤ !&!? '

¨?  $? % " ?! ($? %)?3 ?! ?41 " ($? %) ¨21

¨ ?    ?

¨?  $? % "#

????¤ ??§

($? %) ?5 1

Fig. 9. Bidding OR Refusing

57

¨§ ¤? ! 1§¨ @2 540 1D?§ ?2 540 C! 1% )B A2 540 1D?§ ?2 540 CB $I¨ 1§ ?7§¨ 2 540 ¨§§? ?¤??? ? R ¨§ ¤?  54 §" !¨? CB 55B? 1 ¤? 2 540

§?? ? ?

¨§§? ?¤??? ?

! 1 9?¨  ¤? 2 540 1 ¤? 2 540 5B? H%¨

1?¤?@2 540

  $I¨ H%¨ 1§ ?7§¨ 2 540       

  

! 1?? ?¤8§ 2 540

1?¤?@2 540

C P ¨  5? A#"G  C 5) # 6 1? 62 540 1? 62 540 CB )C # 6

 

! 1% )B A2 540 ! 1§¨ @2 540

! 1? ?¤8§ 2 540

D §¨

T3

Fig. 10. CPN Diagram of the Contract Net Protocol.

! 1 9?¨  ¤? 2 540

  C! 1% )B A2 540 ! 1§¨ @2 540 1D?§ ?2 540 ! 1?? @2 540  5? A#"G  5)%F¨ 1?¨ 2 540 ¨§ ¤? R ¨§§? ?¤??? ? %$#§" !¨? ?? H%¨ "! 1??3 210(( #&¨?0 )( $'& %$#§ ¨? 1??2 540 ?? CB )#%5#P? 1?¨ 2 540 CB )%F¨

C  Q( P¨ 6

¨ 6  3 ! 1?? ?¤8§ 2 540

! 1 9?¨  ¤? 2 540

)#)  55B?  54 ?!¨? ! ! 1?? @3 210(( #&¨?0 )( $'& 54 ? ¨?

! 1?¤?@3 210(( #&¨?0 )( $'& %$#? ¨?

! 1E ?§¨3 210(( #&¨?0 )( $'& %$#? ¨?

)#) S C PB )%$?

%$#?!¨? ! 1E ?§¨3 210(( #&¨?0 )( $'& %$#? ¨?

58

state. For example for MaxBdrs=3, the function would evaluate to: 1‘(B(1),READY)++ 1‘(B(2),READY)++1‘(B(3),READY). Bidders State: This place stores the states of all the bidders. Typed by the colour set BDR STbdr (product of BDR and STbdr), the initial marking of this place corresponds to the multi-set evaluated by the function: BDR STbdr.mult(BDR.all(),1‘W TA), which returns a multi-set with one appearance of all the bidders in the state W TA. AUCTIONEER 2 BIDDERS: This place represents an abstract communication channel used by the auctioneer to broadcast messages to the bidders. Only the messages of the auctioneer (TA, GB and RB) would be available at this place along with the identity of the bidder to which it is destined and hence it is typed by the colour set BDR MESauc. The place is initially empty. BIDDERS 2 AUCTIONEER: Similar to AUCTIONEER 2 BIDDERS, this place contains only the bidder’s messages (BID, REFUSE) along with their identity as de?ned by BDR MESbdr. This place is also empty initially. Responses: This place records the number of messages received (whether BID or REFUSE) from the bidders, so that the auctioneer knows when all responses to the Task Announcement have been received. It thus contains the token 0 at the start of the negotiation process. GRonly1: (GRant only 1) This place ensures that a maximum of one bid is granted. 3.4 Operation of the model

Initially, the auctioneer is ready to broadcast a Task Announcement to all bidders (in the state READY with respect to all bidders) and all the bidders are in the state W TA (Waiting for Task Announcement). The auctioneer initiates the negotiation process by sending a Task Announcement to each of the bidders via the occurrence of the transition Broadcasting TAs (Broadcasting Task Announcements). After Broadcasting TAs ?res, the auctioneer is in the state WAIT for each of the bidders. At this point, the transition Rcv TA (Receive Task Announcement) is enabled as the bidders are in the state W TA and the TA has arrived. As the bidders are all di?erent entities and in general geographically distributed, we model all the activities of the bidders to be concurrent. When the transition Rcv TA ?res, a bidder removes its Task Announcement from the channel and changes state to TEBP (Task Evaluation and Bid Preparation). Once any bidder is in the state TEBP, it ?rst evaluates the task (by considering its resources and any other criteria needed for the execution of the task). After the evaluation of the task, the bidder decides whether to bid or refuse. If the bidder opts to bid, then it prepares the bid. The bid contains details such as the price to be paid, the time it would take to complete the task and any other details that the auctioneer might have asked for. We neither consider the details of the Task Announcement nor the details of the bid in the model. The decision to bid or refuse is modelled as a non-deterministic choice, by transitions Bidding and Refusing. The occurrence of the transition Bidding changes the state of the bidder to W RES (a state where it would be waiting for a decision on its submitted bid), while the occurrence of the transition Refusing changes the state of the bidder to exit nc (a state of the bidder where the negotiation has ended without any contract). After the message from the bidder gets through the communication channel and reaches the auctioneer (in the state WAIT for that bidder), the transition Rcv Bid or Rcv Refuse is enabled depending on the message BID and REFUSE respectively. The occurrence of Rcv Bid causes the auctioneer to change state (with respect to that particular bidder) from WAIT to BID RCVD while the occurrence of Rcv Refuse causes the auctioneer to change state to EXIT NC (the negotiation process is complete and no contract is formed). In addition, the number of responses received is increased by one each time Rcv Bid or Rcv Refuse occurs. The purpose of this mechanism is to keep track of the number of bidders who have replied to the

59

Task Announcement to determine when all replies have been received, which would be equal to the value of MaxBdrs. When this happens, the transitions Granting and Rejecting are enabled provided the auctioneer receives at least one bid in response to the Task Announcement. If all bidders refuse to bid, the protocol terminates with the auctioneer in the EXIT NC state and all the bidders in exit nc. Given that there was at least one bid received, the auctioneer could grant any one of the bids or reject all the bids (in case none of the bids received are suitable). We model this process of selection or rejection of a bid non-deterministically. When all the responses are received, the guard on transitions Granting and Rejecting evaluates to true. When the auctioneer receives at least one bid, the transitions Granting and Rejecting would both be enabled. The place GRonly1 ensures that only a single bid is granted (if at all). The absence of a token at the place GRonly1 signi?es that a bid has been granted and the auctioneer’s objective achieved. On occurrence of Granting, the auctioneer changes state from BID RCVD to EXIT C with respect to the chosen bidder and sends a GB (Grant Bid) message to that bidder. All the other bids received must then be sent a RB (Reject Bid) message via Rejecting. It may also be possible that the auctioneer chooses to reject all the bids in which case the transition Granting would not occur. The transition Rejecting operates in a similar way except that it causes the auctioneer to change its state from BID RCVD to EXIT NC (with respect to the bid that is being rejected) and sends a RB (Reject Bid) to the bidder of the rejected bid, when ?red. Once the messages reach the bidders, the transition Granted or Rejected is enabled depending on the message GB and RB respectively. The occurrence of Granted causes the bidder to change its state from W RES to exit c while the occurrence of Rejected causes the transition in state of the bidder from W RES to exit nc. This process continues until all the bidders reach a terminal state (exit c or exit nc). We expect that when the negotiations have terminated, the bidder that has received the contract (in exit c) will be the same as the bidder that the auctioneer believes has the contract (i.e. is in state EXIT C).

4

State Space Analysis Results

The state space analysis results are presented in Table 3. It shows the properties of the state space as a result of varying the parameter MaxBdrs from 1 to 6.
Table 3. State space analysis results as a function of the parameter MaxBdrs. Properties/MaxBdrs 1 2 3 4 5 State Space Nodes 10 54 290 1578 8798 State Space Arcs 10 93 721 5185 36181 Time (hh:mm:ss) 00:00:00 00:00:00 00:00:00 00:00:03 00:02:02 Scc Graph Nodes 10 54 290 1578 8798 Scc Graph Arcs 10 93 721 5185 36181 Dead Markings 2 3 4 5 6 Home Space (Dead Markings) true true true true true Dead Transition Instances none none none none none Live Transition Instances none none none none none Channel Bound 1 2 3 4 5 6 50238 248833 01:08:11 50238 248833 7 true none none 6

4.1

Absence of Deadlocks and Consistency in Beliefs

The state space is illustrated for MaxBdrs = 1 in Fig. 11. We can observe from the table that the number of dead markings is one more than MaxBdrs: No. of Dead Markings = MaxBdrs + 1.

60

 4 ? ?? ?? ? ?§¨ !EAA2B )782 ?  $ ? ? ? ??? ?¤ ? ?§¨ ? ?    !"# $ ¤ ?? ¤ ?¤? ?% ? ?§¨ ?1562 )78 ?    !"# $ % ? ?%? ?' ? ?§¨ ? ?15621 ?    !"#0 12 3 4 $ & % ?¤? ? ? ?§¨ !) )78 ?    !"# $ &

? & ' ? ? ?( ? ?§¨ ? !) ?    !"#0 12 3 4 $ & ( ?? 9 ?(? ?C ? ?§¨ ?1D1B )78 ?  12 3 0   !"# $ C ? 4 ?C? ?' ? ?§¨ ?1D1B1 ?    !"# $ ' ? ?4 ( ?(? ?9 ? ?§¨@ A 7B )78 ?  12 3 0   !"# $ 9 ? C ?9? ?4 ? ?§¨@ A 7B1 ?    !"# $ 4 ?4

Fig. 11. Reachability Graph (MaxBdrs=1)

For any value of MaxBdrs, one of the dead markings corresponds to a contract not being established at the end of the negotiations. This marking consists of all the bidders in the state exit nc and the auctioneer in the state EXIT NC with respect to all the bidders. This is marking 6 in Fig. 11. This situation can be reached in two ways. Firstly, all the bidders could have submitted a REFUSE message (not willing to bid for the task) in response to the Task Announcement and changed state to exit nc. The auctioneer on receipt of the REFUSE messages would change state to EXIT NC. When the auctioneer receives all the messages (all REFUSE), the auctioneer would be in the state EXIT NC with respect to all the bidders. The negotiations thus terminate with no contract being awarded. This corresponds to path 3,4,6 in Fig. 11. The second way in which the above scenario could occur would be after the receipt of all the replies from the bidders, with the number of bids ranging from at least one to a maximum of MaxBdrs. The auctioneer rejects all the bids by sending a RB message to each of the bidders that bid and changes state to EXIT NC in each case. It would already be in this state for those bidders that submitted a REFUSE message. At the other end, those bidders waiting for a response to their bid (state W RES) on receipt of the RB message, would change state to exit nc. Other bidders who had submitted a REFUSE message would already be in this state. This corresponds to path 3,5,7,9,6 in Fig. 11. The places (AUCTIONEER 2 BIDDERS and BIDDERS 2 AUCTIONEER) representing the communication channel are empty, signifying

61

no unprocessed messages from either the auctioneer or any of the bidders. The value of the token on the place Responses is equal to MaxBdrs, since the auctioneer has received all the responses. The place GRonly1 contains the gr1 token indicating that the transition Granting wasn’t ?red, and hence no bid had been granted. Though the protocol would end without a contract being formed, this particular dead marking is acceptable, because the auctioneer may not receive any bids or may reject all the bids if none of the received bids are acceptable. The additional MaxBdr dead markings comprise for each of the MaxBdrs bidders, one bidder in the state exit c with the rest of the bidders in the state exit nc and the auctioneer in state EXIT C with respect to the same bidder (who is in the state exit c), and EXIT NC with respect to the rest of the bidders. This signi?es that a contract has been formed at the end of the negotiations with one bidder while the negotiations with the rest of the bidders have ended without a contract. The places representing the communication channel are empty signifying that all the messages of the auctioneer and the bidders have been processed. The place Responses contains a token whose value equals MaxBdrs indicating that all the responses have been received. Lastly, the place GRonly1 is empty, signifying the grant of a bid which is also corroborated by the auctioneer and one of the bidders only, being in the state EXIT C and exit c respectively. These dead markings are desired terminal states of the protocol. When MaxBdrs=1, there is only one of these markings, corresponding to marking 10 in Fig. 11.

Fig. 12. Node Descriptors for the dead markings (MaxBdrs=3)

This is illustrated further with the help of Fig. 12 from CPN Tools, which shows the node descriptors for the dead markings for three bidders. Node 210 corresponds to the dead marking where no contract is formed at the end of the negotiations. The multi-set of tokens on the place Auctioneer’s State shows that the auctioneer is in the state EXIT NC with respect to all the three bidders. The place Bidders State shows all three bidders are in the state exit nc. The channel places are empty which is also true for the rest of the dead markings (242, 243 and 249). The place Responses contains a single 3 token indicating that the responses from all three bidders have been received, which is also the case for all the dead markings. The place GRonly1 contains one gr1 token indicating that no bid has been granted. Node Descriptors of the remaining three dead markings (242, 243 and 249) in Fig. 12 reveal that a contract is formed between the auctioneer and the bidders B(3), B(2) and B(1) respectively. This is

62

consistent with the absence of a token at the place GRonly1 in these three cases. The total number of dead markings is 4 (3 + 1) as given by the generalized expression, of which one case corresponds to no contract being formed and the remaining three cases correspond to a contract being formed as described above. The above discussions also justify the consistency in beliefs between the auctioneer and the bidders. It is clear from Fig. 12 that the bidder that has been awarded the contract (in state exit c) is the same as the bidder that the auctioneer believes has the contract (in state EXIT C with respect to that bidder). Similarly, the bidders that have not been awarded a contract (in state exit nc) are the same as the bidders that the auctioneer believes haven’t received the contract (in state EXIT NC with respect to those bidders). This belief is consistent as can be seen in each of the dead markings in Fig. 12 and would hold in general. 4.2 Absence of Livelocks and Proper Termination

As can be seen from Table 3, the size of the state space increases exponentially with the number of bidders. Also, the number of nodes and arcs in the Scc Graph always remain the same as that of the State Space for all values of MaxBdrs that we have examined. This leads us to the conclusion that there is no cyclic behavior in the system, which is expected. This indicates that there are no livelocks, further corroborated by the fact that all the dead markings (MaxBdrs + 1) form a home space for all the values of MaxBdrs speci?ed in Table 3. We conjecture that this would be true for any value of MaxBdrs. Since all the dead markings are desirable and they form a home space (for the cases examined), this implies that the system will always terminate correctly. The presence of dead markings excludes the possibility of live transition instances, as is con?rmed in Table 3. 4.3 Absence of Dead Code

There are no instances of dead transitions for any value of MaxBdrs examined, revealing that all transitions are required (no dead code). This means that all the speci?ed actions are executed. 4.4 Channel Bound

Table 3 also shows the bounds (upper integer bounds) on the communication channel which is the same for both AUCTIONEER 2 BIDDERS and BIDDERS 2 AUCTIONEER. As can be seen, this limit is equal to MaxBdrs for all the cases considered.

5

Conclusions and Future Work

In this paper, we have presented the ?rst complete CPN model of the Contract Net Protocol. We claim the level of abstraction of the model is appropriate for analysing important properties of the protocol. For the values of MaxBdrs considered (1 to 6), we have proved a number of properties using state space analysis. Firstly, if the protocol terminates, then the protocol terminates correctly (partial correctness). Secondly, the fact that all the dead markings form a home space implies the absence of livelocks in the system. This ensures that the protocol will always terminate in all possible behaviours (progress). The number of terminal states is given by MaxBdrs+1, corresponding to a contract with each of the bidders or no contract being granted. Further we show that both channel bounds are limited to MaxBdrs. We therefore believe that the model and results in this paper refute the claims made by Paurobally [14, 15] that Coloured Petri Nets are not suited to the modelling and analysis of interaction protocols, by illustrating their ability to successfully model and analyse the Contract Net Protocol. We believe our CPN model is complete, non-ambiguous and compact, being able

63

to be drawn on a single page. The CPN models the multithreaded nature of the auctioneer, as it deals with many bidders concurrently. Further it is parametric, modelling the Contract Net Protocol for any number of bidders using the same structure and inscriptions, contrary to the model presented in Fig. 7 of Nowostawski et al [13], which is structurally di?erent, incomplete and ambiguous. Further, the CPN diagram and its declarations provide a semantics for the Protocol Flow Diagram representation of Perugini [16]. In addition to proving correct termination and consistency in beliefs (that the protocol terminates with a common belief between the auctioneer and each of the bidders) as was done in [15], we have also proved the absence of livelocks. Further we have shown how the number of terminal states and channel bounds are related to the parameter MaxBdrs. This work can be extended in many directions. We would like to prove these properties for all values of MaxBdrs and then consider relaxing Assumptions 3 and 5. This would introduce deadlines and allow further interaction between the auctioneer and the successful bidder as the task proceeds. One could then consider relaxing Assumption 1 to extend the model to open multi-agent systems, where the identities of all the bidders are not necessarily known a priori. We believe that Assumption 4 is realistic and that the abstractions made in Assumption 2 do not a?ect the properties we are trying to prove, which do not concern data. We would also like to extend this work to more elaborate negotiation protocols such as the Extended Contract Net Protocol (ECNP) [5,6], the Contract Net Protocol extension (CNP-ext) [1] and the Provisional Agreement Protocol (PAP) [16]. Each of these protocols provides greater ?exibility with planning and task allocation than its preceding ones and is considerably more complex.

Acknowledgements
The authors would like to acknowledge fruitful discussions with their colleagues, Guy Gallasch and Nimrod Lilith, regarding this work. We are also very grateful to the anonymous reviewers for their constructive comments that helped us to improve the paper.

References
1. S. Aknine, S. Pinson, and M. F. Shakun. An Extended Multi-Agent Negotiation Protocol. Autonomous Agents and Multi-Agent Systems, 8(1):5–45, 2004. 2. J. Billington, G. E. Gallasch, and B. Han. A Coloured Petri Net Approach to Protocol Veri?cation. In Lectures on Concurrency and Petri Nets, Lecture Notes in Computer Science, volume 3098, pages 210–290. Springer-Verlag, 2004. 3. G. Booch, J. Rumbaugh, and I. Jacobson. The Uni?ed Modeling Language User Guide. Addison-Wesley, 2nd edition, 2005. 4. J. Ferber. Multi-Agent Systems: An Introduction to Distributed Arti?cial Intelligence. Addison Wesley Longman, 1999. 5. K. Fischer and N. Kuhn. A DAI Approach to Modelling the Transportation Domain, DFKI Research Report RR-93-25. German Research Centre for Arti?cial Intelligence (DFKI), Saarbr¨ ucken, 1993. 6. K. Fischer, J. P. M¨ uller, I. Heimig, and A. W. Scheer. Intelligent Agents in Virtual Enterprises. In Proceedings of the 1st International Conference on the Practical Application of Intelligent Agents and MultiAgent Technology, London, UK, pages 205–223, 1996. 7. Foundation for Intelligent Physical Agents-Agent Communication Language speci?cation (FIPA-ACL). http://www.?pa.org. 8. Foundation for Intelligent Physical Agents (FIPA). http://www.?pa.org. 9. Foundation for Intelligent Physical Agents (FIPA). http://www.?pa.org/specs/?pa00029/SC00029. 10. F. S. Hsieh. Modelling and Analysis of Contract Net Protocol. In Lecture Notes in Computer Science, volume 3140, pages 142–146. Springer-Verlag Berlin Heidelberg, 2004. 11. K. Jensen. Coloured Petri Nets: Basic Concepts, Analysis Methods and Practical Use. Volumes 1 to 3, Basic Concepts, Analysis Methods and Practical Use. Monographs in Theoretical Computer Science. SpringerVerlag, 2nd edition, 1997. 12. K. Jensen, L. M. Kristensen, and L. Wells. Coloured Petri Nets and CPN Tools for Modelling and Validation of Concurrent Systems. International Journal on Software Tools for Technology Transfer, 9(3-4):213–254, Springer–Verlag, 2007.

64

13. M. Nowostawski, M. Purvis, and S. Crane?eld. A Layered Approach for Modelling Agent Conversations. In Proceedings of the 2nd International Workshop on Infrastructure for Agents, MAS, and Scalable MAS, a satellite workshop of the 5th International Conference on Autonomous Agents, Montreal, pages 163–170, 2001. 14. S. Paurobally. Rational Agents and the Processes and States of Negotiation. PhD thesis, Imperial College, London, UK, 2002. 15. S. Paurobally, J. Cunningham, and N. R. Jennings. Verifying the Contract Net Protocol: A Case Study in Interaction Protocol and Agent Communication Language Semantics. In Proceedings of 2nd International Workshop on Logic and Communication in Multi-Agent Systems, Nancy, France, pages 98–117, 2004. 16. D. Perugini. Agents for Logistics: A Provisional Agreement Approach. PhD thesis, The University of Melbourne, Victoria, Australia, 2006. 17. R.G. Smith. The Contract Net Protocol: High-Level Communication and Control in a Distributed Problem Solver. IEEE Transactions On Computers, C-29(12):1104–1113, 1980. 18. P. Ulam, Y. Endo, A. Wagner, and R. Arkin. Integrated Mission Speci?cation and Task Allocation for Robot Teams-Design and Implementation. In Proceedings of the IEEE International Conference on Robotics and Automation, Roma, Italy, pages 4428–4435, 2007.

65

66

Modeling Grid Work?ows with Colored Petri Nets?
Carmen Bratosin, Wil van der Aalst, and Natalia Sidorova
Department of Mathematics and Computer Science Eindhoven University of Technology P.O. Box 513, 5600 MB Eindhoven, The Netherlands c.c.bratosin@tue.nl, w.m.p.v.d.aalst@tue.nl, n.sidorova@tue.nl

Abstract. Grid computing refers to the deployment of a widely distributed architecture for the execution of computationally challenging tasks. The grid provides a set of distributed resources which can be used for “computing on demand” or for constructing a “virtual supercomputer”. Recently, several researchers started to look at the relation between work?ow management and grid computing. The ?ow of work through a grid can be seen as a classical “work?ow”. However, as opposed to the classical work?ows, the resources are not humans and are not managed by some centralized client-server architecture. Instead, the grid is highly distributed and the resources are computing power, memory, etc. Currently, there is no conceptual framework for grid computing and the role of work?ows in grids is unclear. This paper provides initial steps towards a conceptual framework expressed in terms of Colored Petri Nets. CPN Tools is used to model grids while focusing on the work?ow aspects. The resulting model can be analyzed to detect deadlocks, etc. The framework is illustrated using process mining as an application. Keywords: Colored Petri nets; grid computing; modeling.

1

Introduction

Grid computing [21] is concerned with the development and advancement of technologies that provide seamless and scalable access to wide-area distributed resources. Currently, many researchers and practitioners are developing software to support grid computing. A well-known example is the Globus Toolkit which provides an open source software toolkit for building grids [17]. Within the grid community several research groups have made attempts to adopt ideas from work?ow management and apply them in a grid context [15, 18, 19, 23, 25]. For many grid applications the work?ow-paradigm is quite natural, e.g., complex scienti?c computations can be modeled as work?ows. However, unlike classical work?ows the control is decentralized and resources are computing power, memory, etc. rather than people.
?

This research is supported by the GLANCE NWO project “Work?ow Management for Large Parallel and Distributed Applications”.

67

Despite the current interest in grids and work?ow, a good conceptual model of grids is missing and most researchers are focusing on the practical realization of grids. Terms like “resource”, “job”, and “work?ow” are subject to multiple interpretations. Therefore, in this paper, we model the basic grid concepts in terms of Colored Petri Nets (CPNs, [20]). The main purpose is to clarify the basic concepts. Moreover, we also show that the mapping of grids onto CPNs allows for all kinds of analysis. Given the fact that the allocation and deallocation of resources in grids is done in a distributed manner and that multiple resources may be involved in some task, a grid work?ow may easily deadlock. Therefore, this paper will focus on the use of state-space analysis to discover deadlocks. Grids are often used in areas where there is a need for a lot of (preferably inexpensive) computing power. Examples can be found in scienti?c computing, e.g., SETI@home searches for possible evidence of radio transmissions from extraterrestrial intelligence using data from radio telescopes. SETI@home uses CPU-scavenging for this, i.e., a grid of unused desktop computers is exploited to analyze the radio transmissions. This particular form of grid use is also called “voluntary computing” because the resources are made available without a clear economic motive for the participants. Another interesting application domain is the use of grids for data mining to analyse the large volumes of data generated today (cf. the DataMiningGrid project [2]). In this paper, we will focus on a particular application: the utilization of grid computing for process mining. The goal of process mining is to extract models (e.g. Petri nets) from event logs [9]. This is possible because many systems ranging from enterprise information systems and web applications to embedded and high-tech systems are collecting enormous volumes of audit trails. To deal with these large amounts of data and computationally expensive process mining algorithms, grids are particularly useful. High-level process mining tasks can easily be described as work?ows where the activities correspond to the execution of particular process mining algorithms. Therefore, process mining is an interesting application domain for grid computing. The remainder of the paper is organized as follows. In Section 2 we present a running example and motivate the utilization of grid computing for process mining. Section 3 introduces the basic grid concepts which are mapped onto CPNs in Section 4. Related work is discussed in Section 6 and Section 7 concludes the paper.

2

Running Example: Applying Grid Technology to Process Mining

As indicated in the introduction, in this paper we focus on using grid technology for large process mining tasks. In recent years, process mining has emerged as a way to analyze systems and their actual use based on the event logs they produce [11]. Note that, unlike classical data mining, the focus of process mining is on concurrent processes and not on static or mainly sequential structures. A

68

classical example is the α-algorithm [11] which automatically constructs a Petri net based on a set of observed system traces. Process mining is applicable to a wide range of systems. These systems may be pure information systems (e.g., ERP systems) or systems where the hardware plays a more prominent role (e.g., embedded systems). The only requirement is that the system produces event logs, thus recording (parts of) the actual behavior. Information systems such as classical work?ow management systems (e.g. Sta?ware) case handling systems (e.g. FLOWer), PDM systems (e.g. Windchill), middleware (e.g., IBM’s WebSphere), hospital information systems (e.g., Chipsoft) record detailed information about the activities that have been executed. Other systems recording events are medical systems (e.g., X-ray machines), production systems (e.g., wafer steppers), copiers, sensor networks, etc. An example is the “CUSTOMerCARE Remote Services Network” of Philips Medical Systems (PMS). This is a worldwide internet-based private network that links PMS equipment to remote service centers. An event that occurs within an X-ray machine (e.g., moving the table, setting the de?ector, etc.) is recorded and analyzed. The logging capabilities of the machines of PMS illustrate that event logs are widely available. The goal of process mining is to extract information (e.g., process models) from these logs, i.e., process mining describes a family of a-posteriori analysis techniques exploiting the information recorded in the event logs. Simple algorithms such as the α-algorithm [11] are linear in the size of the event log. However, such algorithms do not perform well on real-life data and their simplicity is misleading for two reasons: (1) more advanced process mining algorithms are needed that require lots of computing power and parameter tuning and (2) the “process of process mining” consists of additional pre- and post-processing steps (?ltering, cleaning, merging, conformance checking, etc.). It should be noted that event logs may be huge, e.g., there may be thousands of di?erent cases and there may be thousands of events per case. Logs such as the ones produced by the machines of PMS illustrate the computational challenges. Moreover, some process mining techniques require lots of computing power. Consider for example the genetic process mining algorithms described in [24]. All of the more advanced algorithms have lots of parameters that need to be set. Typically, the algorithms are run with di?erent parameter settings to achieve acceptable results. Hence, di?erent process mining experiments are run iteratively or in parallel. Besides running the core process mining algorithms several preand post-processing steps need to conducted. The main goal of grid computing is to o?er wide distributed computing and storage facilities for complex applications. From the observations just made, process mining process can require challenging computational executions, and also has to deal with a large amount of data. Therefore, process mining is an interesting application domain for grid computing. On the one hand, there are clear computational challenges that can be addressed through grid computing. On the other hand, the “process of process mining” can be seen as a work?ow

69

alpha miner

+

-

start

prepare log

analyze log

select algorithm

heuristic miner

check conformance

return results

end

genetic miner

1

+
2

-

start

set parameters

partition log for 10 fold checking

check results
10

return results

end

run algorithm

Fig. 1. The process mining work?ow expressed in terms of YAWL [6]

consisting of activities ranging from data preparation and ?ltering to discovery and conformance checking. To illustrate the application of grid computing to process mining, we use a rather simple and abstract example as shown in Figure 1. It is kept simple so that it is understandable by non-process mining experts and to allow for understandable CPN models later in this paper. Figure 1 describes a typical process mining scenario in terms of the work?ow language YAWL [6]. YAWL extends Petri nets with notations useful for representing work?ows. The work?ow at the top of Figure 1 shows that a high-level process mining job starts with the preparation of the log (task prepare log ). It includes the scanning of the log for inconsistencies (e.g., descending timestamps, missing event types, etc.) and the addition of dummy start and end events if needed. Then the log is analyzed (task analyze log ) and several characteristics are collected, e.g., size, completeness, number of event types, distribution of activities, etc. Based on this task select algorithm chooses a particular algorithm that is expected to perform well given the characteristics of the log. If characteristics indicate that the log is highly structured and has no noise, the α-algorithm may be selected. If it contains some noise and is large, the heuristic miner [22] may be selected. The genetic miner may be selected if the structure of the model is complicated, there is noise, and the log is not too large. After running one of the process mining algorithms, the quality of the result is checked (task check conformance ). If the quality is acceptable or there are no more alternatives,

70

the results are returned. Otherwise, another algorithm is selected and the process is repeated. Each of the process mining algorithms corresponds to a YAWL subprocess. In Figure 1 only the subprocess genetic miner is described. The genetic miner starts by setting the parameters. Genetic algorithms typically have many di?erent parameters that one can experiment with. The genetic miner has parameters such as population size, number of generations, seed, elitism, mutation rate, ?tness function, crossover type, etc. Although not shown in Figure 1 di?erent instances of the same algorithm could run in parallel with di?erent parameters to improve response time. After task set parameters, the log is split and replicated for 10-fold checking. k -fold cross validation divides the data set into k subsets. Each time, one of the k subsets is used as the test set and the other k ? 1 subsets are put together to form a training set. Then the average error across all k trials is computed. In this work?ow the cases in the logs are split over 10 sets and each of the 10 parallel branches in Figure 1 takes 9 of these 10 sets to construct a process model based on the genetic algorithm. After applying the algorithm the result is evaluated using the remaining test set. Task check results collects these results and decides whether a new experiment is needed, i.e., the subprocess returns to task set parameters or ends with task return results. Figure 1 also shows some annotations describing the use of resources. For this simpli?ed example, we assume that there are only two types of required properties for task execution: CPU and disk space. Disk space is denoted by the small tube and CPU power is denoted by a small hexagon. Disk space is typically allocated for multiple subsequent tasks while CPUs are typically released after each task. Task prepare log claims space for storing the entire log and the overall results. This space is only returned at the end of the work?ow. Since the genetic algorithm is a more complex process, the algorithm has its own private data space. In the remainder of this paper, we will use process mining and in particular the example shown in Figure 1 to illustrate our approach.

3

Grid Work?ows

This section introduces the basic grid concepts relevant for the remainder of this paper. As indicated, we will model grids in terms of CPNs and emphasize the work?ow aspect of grid computing. The standard grid architecture [16] is composed of several layers: (1) the infrastructure layer composed of resources (e.g. databases, cluster computers), (2) the application layer, where the grid user describes the processes to be submitted to the grid, and (3) the middleware layer, which is in charge of ?nding a resource for the user requirements and other management issues (e.g. monitoring, fault recovery). Infrastructure layer The grid infrastructure is a widely distributed infrastructure, composed of di?erent resources, linked via the Internet. The resources allow for the execution of di?erent tasks. Examples of typical resources in a grid infrastructure are computing elements

相关文章:
...molding training system using Petri nets and vir...
J.B. Coloured Petri Nets... 暂无评价 20页 免费 Model Driven Development...Presented in this paper are an architecture of VPIMTS, a practical ...
Extended Petri Net Based Formal Modeling and Verifi...
Extended Petri Net Based Formal Modeling and Verification of WTB-TeN Device ... "An Introduction to the Theoretical Aspects of Coloured Petri Nets," In:...
密钥管理技术研究综述
Jensen, Coloured Petri Nets: Basic Concep ts, AnalysisMethods and Practical Use,Vol. 1. Sp ringer2Verlag, 1992. [ 2 ] G. Bucci and E. Vicario, ...
更多相关标签: