J. R. Abrial (2007):
The Event-B Book.
Cambridge Univ. Press,
Cambridge.
Jean-Raymond Abrial (1996):
The B-book: assigning programs to meanings.
Cambridge Univ. Press,
Cambridge,
doi:10.1017/CBO9780511624162.
R.J. Back & J. von Wright (1998):
Refinement Calculus: A Systematic Introduction.
Graduate Texts in Computer Science.
Springer-Verlag,
doi:10.1007/978-1-4612-1674-2.
T. Bolognesi & E. Brinksma (1987):
Introduction to the ISO Specification Language LOTOS.
Computer Networks and ISDN Systems 14(1),
pp. 25–59,
doi:10.1016/0169-7552(87)90085-7.
M. Butler (1999):
csp2B : A Practical Approach to Combining CSP and B.
In: FM'99,
LNCS 1708.
Springer-Verlag,
Toulouse, France,
pp. 490–508,
doi:10.1007/3-540-48119-2_28.
J. Davies & J.C.P. Woodcock (1996):
Using Z: Specification, Refinement, and Proof.
Prentice-Hall.
John Derrick & Heike Wehrheim (2005):
Non-atomic Refinement in Z and CSP.
In: ZB 2005: Formal Specification and Development in Z and B, 4th International Conference of B and Z Users,
LNCS 3455.
Springer-Verlag,
Guildford, UK,
pp. 24–44.
Available at http://dx.doi.org/10.1007/11415787_3.
M. Embe Jiague, M. Frappier, F. Gervais, P. Konopacki, J. Milhau, R. Laleau & R. St-Denis (2010):
Model-Driven Engineering of Functional Security Policies.
In: International Conference on Enterprise Information Systems 3,
pp. 374–379.
T. Fayolle (2014):
Specifying a Train System Using ASTD and the B Method.
Technical Report.
Available at www.lacl.fr/~tfayolle.
Http://www.lacl.fr/~ tfayolle.
Alessio Ferrari, GiorgioO. Spagnolo, Giacomo Martelli & Simone Menabeni (2014):
From commercial documents to system requirements: an approach for the engineering of novel CBTC solutions.
International Journal on Software Tools for Technology Transfer,
pp. 1–21.
Available at http://dx.doi.org/10.1007/s10009-013-0298-6.
M. Frappier, F. Gervais, R. Laleau, B. Fraikin & R. St-Denis (2008):
Extending Statecharts with Process Algebra Operators.
Innovations in Systems and Software Engineering 4(3),
pp. 285–292,
doi:10.1007/s11334-008-0064-1.
M. Frappier, F. Gervais, R. Laleau & J. Milhau (2014):
Refinement patterns for ASTDs.
Formal Aspects of Computing 26(5),
pp. 919–941,
doi:10.1007/s00165-013-0286-3.
Marc Frappier, Frédéric Gervais, Régine Laleau & Benoît Fraikin (2008):
Algebraic State Transition Diagrams.
Technical Report.
Université de Sherbrooke.
D. Harel (1987):
Statecharts: A Visual Formalism for Complex Systems.
Science of Computer Programming 8,
pp. 231–274,
doi:10.1016/0167-6423(87)90035-9.
C.A.R. Hoare & H. Jifeng (1998):
Unifying Theories of Programming.
Prentice-Hall.
Alexei Iliasov, Elena Troubitsyna, Linas Laibinis, Alexander Romanovsky, Kimmo Varpaaniemi, Dubravka Ilic & Timo Latvala (2010):
Supporting Reuse in Event B Development: Modularisation Approach.
In: Abstract State Machines, Alloy, B and Z, Second International Conference, ABZ 2010,
LNCS 5977.
Springer-Verlag,
pp. 174–188.
Available at http://dx.doi.org/10.1007/978-3-642-11811-1_14.
J. Milhau, A. Idani, R. Laleau, M. Labiadh, Y. Ledru & M. Frappier (2011):
Combining UML, ASTD and B for the formal specification of an access control filter.
Innovations in Systems and Software Engineering 7(4),
pp. 303–313,
doi:10.1007/s11334-011-0166-z.
MVM Oliveira (2005):
A refinement calculus for Circus.
Department of Computer Science, The University of York.
A. Pnueli (1981):
The Temporal Semantics of Concurrent Programs.
Theoretical Computer Science 13,
pp. 45–60,
doi:10.1016/0304-3975(81)90110-9.
A.W. Roscoe (1997):
The Theory and Practice of Concurrency.
Prentice-Hall.
Steve Schneider & Helen Treharne (2005):
CSP theorems for communicating B machines.
Formal Asp. Comput. 17(4),
pp. 390–422.
Available at http://dx.doi.org/10.1007/s00165-005-0076-7.
Steve Schneider & Helen Treharne (2011):
Changing system interfaces consistently: A new refinement strategy for CSP||B.
Sci. Comput. Program. 76(10),
pp. 837–860.
Available at http://dx.doi.org/10.1016/j.scico.2010.08.001.
Renato Silva (2012):
Thesis, chapter Chapter 6 : Case Study,
pp. 121–160.
H. Treharne & S. Schneider (1999):
Using a Process Algebra to Control B operations.
In: IFM'99.
Springer-Verlag,
York, United Kingdom,
pp. 437–457,
doi:10.1007/978-1-4471-0851-1_23.
J.C.P. Woodcock & A.L.C. Cavalcanti (2002):
The Semantics of Circus.
In: ZB 2002,
LNCS 2272.
Springer-Verlag,
Grenoble, France,
pp. 184–203,
doi:10.1007/3-540-45648-1_10.