Mocenigo, J., and Rogers, A. (2001). Visualizing and
analyzing software infrastructures. IEEE Software,
Sept./Oct. 2001:pp 62–70.
Jensen, K. (1997). Coloured Petri Nets Basic Con-
cepts, Analysis Methods and Practical Use, volume 1.
Springer Verlag, Aarhus University, Denamrk, 2 edi-
tion.
Latella, D., Majzik2, I., and Massink1, M. (1999). Auto-
matic verifcation of a behavioural subset of uml state-
chart diagrams using the spin model-checker1. Formal
Aspects of Computing, 11:pp 637–664.
Lilius, J. and Paltor, I. P. (1999). Formalizing UML state
machines for model checking. In Robert France
and Burnhard Rumpe (Eds.):UML’99, Lecture Notes
in Computer Science (LNCS 1723), pp 430-444,
Springer Verlag Berlin Heidelberg.
Maier, C. and Moldt, D. (2001). Object coloured Petri nets
- a formal technique for object oriented modelling.
In Agha et al.(Eds.):Concurrent OOP and PN, LNCS
2001, pp 406-427, Berlin Heidelberg. Springer Verlag
2001.
Merseguer, J., Campos, J., Bernardi, S., and Donatelli, S.
(2002). A compositional semantics for UML state ma-
chines aimed at performance evaluation. In Proc. 6th
Int. W/S on Discrete Event Systems (WODES’02), pp
295-302, Zaragoza, Spain. IEEE Computer Society.
Nawana, H. (1996). Software agents: An overview. The
Knowledge Engineering Review, 11(3):pp 1–40.
Philippi, S. (2000). Seamless object-oriented software de-
velopment on a formal base. In Proceedings of the
Workshop on Software Engineering and Petri Nets,
21st International Conference on Application and
Theory of Petri Nets.
Rober, G. (1999). An incremental process for software im-
plementation. Sloan Management Review, Winter:pp
39–52.
Rysavy, O. (2003). A survey on approaches to formal
representation of UML, retrieved on june 10, 2005
from:. Technical report, Brno University of Technol-
ogy, Czech Republic, web site.
Saldana, J. A. and Shatz, S. M. (2001). Formalization
of object behavior and interactions from UML mod-
els. International Journal of Software Engineering
and Knowledge Engineering (IJSEKE), 11 No. 6:643–
673.
Singh, M. (2000). Synthesizing coordination requirements
for heterogeneous autonomous agents. Autonomous
agents and multiagent systems, 3(2):pp 107–132.
Tosic, P. and Agha, G. (2004). Towards a hierarchical tax-
onomy of autonomous agents. In Proc. IEEE Int’l
Conference on Systems, Man and Cybernetics (IEEE-
SNC’04), The Hague, The Netherlands.
Varro, D. (2002). A formal semantics of uml statecharts
by model transition systems. In ICGT ’02: Proc. 1st
Int. Conf. on Graph Transformation, pages 378–392,
London, UK. Springer-Verlag.
Venkatraman, N. (1994). IT-enabled business. Sloan Man-
agement Review, Winter:pp 73 – 87.
Wagenhals, L., Haider, S., and Lewis, A. H. (2002). Synthe-
sizing executable models of object oriented architec-
tures. In CRPITS ’12: Proc. Conf. on Application and
Theory of Petri Nets, pages 85–93, Darlinghurst, Aus-
tralia, Australia. Australian Computer Society, Inc.
Wooldridg, M. and Jennings, N. (1995). Intelligent agents:
Theory and practice. The Knowledge Engineering Re-
view, 10(2):pp 115–152.
Wooldridge, M. and Ciancarini, P. (2000). Agent-oriented
software engineering:the sate of the art. In Proc. 1st
Int. W/S (AOSE-2000). Springer-Verlag: Berlin, Ger-
many.
Wooldridge, M., Jennings, N., and Kinny, D. (1999). A
methodology for agent-oriented analysis sand design.
In Proc. 3rd Conf. On Autonomous Agents, Eds, O.
Etzioni, J. P. Mller, J.M. Bradshaw. ACM Press.
Zhao, Y., Fan, Y., Bai, X., Wang, Y., Cai, H., and Ding, W.
(2004). Towards formal verification of UML diagrams
based on graph transformation. In Proc. IEEE Int.
Conf. on E-Commerce Tech. for Dynamic E-Business
(CEC-East’04).
msg_in
MSG
Pin
MSG
Channel
Pout
MSG
Channel
msg_out
MSG
msg_inv
MSG
Pinv
MSG
Channel
msg_rec
MSG
Prec
MSG
idle
AID
{c=c1, ajd=0}
wait
AID
Tin
Trec
Tout
Tinv
creatingIA
created
[#Service rec_msg = aknw]
ReqInfo
[#ajd aic = 1]
my_aijs
AID
my_aijs
Filter
contents
1‘ "X" ++ 1‘ "Y"
free_ids
contents
1‘ "agent1" ++ 1‘ "agent2"
my_aijs
AID
deleting
[#ajd aic =1]
d_mu
UNIT
1‘e
Info
integer
RecInfo
[#Service rec_msg = info]
msg
msg
msg
msg
aic
msg
msg
id
id
aid
aic
aic
aic
#Sender rec_msg
rec_msg
aic
aic
aid
e
#Parameter rec_msg
aic
rec_msg
Figure 5: OCPN Class Model of User Agent Class.
VALIDATION OF INFORMATION SYSTEMS USING PETRI NETS
289