1: \begin{thebibliography}{10}
2:
3: \bibitem{Abr96a}
4: J-R. Abrial.
5: \newblock {Extending B without Changing it (for developping distributed
6: systems)}.
7: \newblock {\em Proc. of the 1st Conference on the {B} method, H. Habrias
8: (editor), France}, pages 169--190, 1996.
9:
10: \bibitem{AbrialCansellMery03}
11: J-R. Abrial, D.~Cansell, and D.~Mery.
12: \newblock {Formal Derivation of Spanning Trees Algorithms}.
13: \newblock In D.~Bert et~al., editor, {\em ZB'2003 -- Formal Specification and
14: Development in {Z} and {B}}, volume 2651 of {\em Lecture Notes in Computer
15: Science}, pages 457--476. Springer-Verlag, 2003.
16:
17: \bibitem{AbrialMussat98}
18: J-R. Abrial and L.~Mussat.
19: \newblock {Introducing Dynamic Constraints in B}.
20: \newblock In {\em Proc. of the 2nd Conference on the {B} method, D. Bert
21: (editor)}, volume 1393 of {\em Lecture Notes in Computer Science}, pages
22: 83--128. Springer-Verlag, 1998.
23:
24: \bibitem{BaKu83}
25: R.J. Back and R.~Kurki-Suonio.
26: \newblock {Decentralisation of Process Nets with Centralised Control}.
27: \newblock In {\em Proc. of the 2nd {ACM SIGACT-SIGOPS} Symposium on
28: {P}rinciples of {D}istributed {C}omputing}, pages 131--142. ACM, 1983.
29:
30: \bibitem{BoultonEtAl92}
31: R.~Boulton, A.~Gorgon, M.J.C. Gordon, J.~Hebert, and J.~van Tassel.
32: \newblock {Experience with Embedding Hardware Description Language in HOL.}
33: \newblock In {\em Proc. of the International Conference on Theorem Provers in
34: Circuit Design: Theory, Practice and Experience}, pages 129--156,
35: North-Holland, 1992. IFIP TC10/WG 10.2.
36:
37: \bibitem{BowenGordon95}
38: J.~P. Bowen and M.~J.~C. Gordon.
39: \newblock {A Shallow Embedding of Z in HOL}.
40: \newblock {\em Information and Software Technology}, 37(5-6):269--276, 1995.
41:
42: \bibitem{ButlerWalden96}
43: M.~Butler and M.~Walden.
44: \newblock {Distributed System Development in B}.
45: \newblock {\em Proc. of the 1st Conference on the {B} method, H. Habrias
46: (editor), France}, pages 155--168, 1996.
47:
48: \bibitem{ZB02-Cansell}
49: Dominique Cansell, Ganesh Gopalakrishnan, Mike Jones, and Dominique Mery.
50: \newblock Incremental proof of the producer/consumer property for the pci
51: protocol.
52: \newblock In {\em ZB'2002 -- Formal Specification and Development in {Z} and
53: {B}}, pages 22--41, 2002.
54:
55: \bibitem{GenrichPrTNets_86}
56: H.~J. Genrich.
57: \newblock {Predicate/Transition Nets}.
58: \newblock In W.~Brauer, W.~Reisig, and G.~Rozenber, editors, {\em {Petri Nets:
59: Central Models and their Properties, Adavneces in Petri Nets(1986)}}, volume
60: 254 of {\em Lecture Notes in Computer Science}, pages 207--247.
61: Springer-Verlag, 1987.
62:
63: \bibitem{GravellPrattenZ_PVS_HOL}
64: A.~W. Gravell and C.~H. Pratten.
65: \newblock {Embedding a Formal Notation: Experiences of Automating the Embedding
66: of Z in the Higher Order Logic of PVS and HOL}.
67: \newblock In {\em \cite{TPHOL98}}, pages 73--84, 1998.
68:
69: \bibitem{TPHOL98}
70: {J. Grundy and M. Newey}, editor.
71: \newblock {\em {Supplementary Proceedings of the 11th International Conference
72: on Theorem Proving in Higher Order Logics: Emerging Trends, (TPHOL'98)}}.
73: \newblock Australian National University, 1998.
74:
75: \bibitem{JensenCPN1}
76: K.~Jensen.
77: \newblock {Coloured Petri Nets and the Invariant Method}.
78: \newblock {\em TCS}, 14:317--336, 1986.
79:
80: \bibitem{Jensen9296}
81: K.~Jensen.
82: \newblock {Coloured Petri Nets Vol. I-III}.
83: \newblock In {\em EATCS Monographs on Theoretical Computer Science}, EATCS.
84: Springer-Verlag, 1992-1996.
85:
86: \bibitem{KristensenPN2004}
87: L.~M. Kristensen and K.~Jensen.
88: \newblock {Specification and Validation of an Edge Router Discovery Protocol
89: for Mobile Ad-hoc Networks}.
90: \newblock In {\em Proceedings of INT'04}, volume 3147 of {\em LNCS}, pages
91: 248--269. Springer-Verlag, 2004.
92:
93: \bibitem{appliPN2004}
94: Lars~Michael Kristensen, Jens~Bæk Jørgensen, and Kurt Jensen.
95: \newblock {Application of Coloured Petri Nets in System Development}.
96: \newblock volume 3098 of {\em LNCS}, pages 626--685. Springer-Verlag, Jan 2004.
97:
98: \bibitem{Munoz&Rushby:FM99}
99: C.~Mu{\~{n}}oz and J.~Rushby.
100: \newblock {Structural Embeddings: Mechanization with Method}.
101: \newblock In {J. Wing and J. Woodcock}, editor, {\em {Proc. of the World
102: Congress in Formal Methods (FM99)}}, volume 1708 of {\em Lecture Notes in
103: Computer Science}, pages 452--471, France, 1999. Springer-Verlag.
104:
105: \bibitem{murata89}
106: T.~Murata.
107: \newblock {Petri-Nets: Properties, Analysis and Applications}.
108: \newblock In {\em Proc. IEEE}, volume~77, pages 541--580. IEEE, 1989.
109:
110: \bibitem{reisig98}
111: W.~Reisig.
112: \newblock {\em {Elements of Distributed Algorithms: Modeling and Analysis with
113: Petri Nets}}.
114: \newblock Springer, 1998.
115:
116: \bibitem{PNET12_1998}
117: W.~Reisig and G.~Rozenberg, editors.
118: \newblock {\em Lectures on Petri nets I: Basic models and II: Applications},
119: volume 1491/1492 of {\em Lecture Notes in Computer Science}. Springer-Verlag,
120: 1998.
121:
122: \bibitem{SekerinskiZurob02}
123: E.~Sekerenski and R.~Zurob.
124: \newblock {Translating Statecharts to B}.
125: \newblock In {\em {Proc. of the Integrated Formal Methods (IFM'2002)}}, volume
126: 2335 of {\em Lecture Notes in Computer Science}, UK, May 2002.
127: Springer-Verlag.
128:
129: \end{thebibliography}
130: