@book(Abrial2007,
 author       = {J. R. Abrial},
 year         = {2007},
 title        = {The Event-B Book},
 publisher    = {Cambridge Univ. Press},
 address      = {Cambridge},
)
@book(Abrial1996,
 author       = {Jean-Raymond Abrial},
 year         = {1996},
 title        = {The B-book: assigning programs to meanings},
 publisher    = {Cambridge Univ. Press},
 address      = {Cambridge},
 doi          = {10.1017/CBO9780511624162},
)
@book(actsysback,
 author       = {R.J. Back and J. von Wright},
 year         = {1998},
 title        = {Refinement {C}alculus: {A} {S}ystematic {I}ntroduction},
 series       = {Graduate Texts in Computer Science},
 publisher    = {Springer-{V}erlag},
 doi          = {10.1007/978-1-4612-1674-2},
)
@article(DBLP:journals/fac/Boiten14,
 author       = {Eerke A. Boiten},
 year         = {2014},
 title        = {Introducing extra operations in refinement},
 journal      = {Formal Asp. Comput.},
 volume       = {26},
 number       = {2},
 pages        = {305--317},
 url          = {http://dx.doi.org/10.1007/s00165-012-0266-z},
)
@article(bolognesi,
 author       = {T. Bolognesi and E. Brinksma},
 year         = {1987},
 title        = {Introduction to the {ISO} {S}pecification {L}anguage {LOTOS}},
 journal      = {Computer {N}etworks and {ISDN} {S}ystems},
 volume       = {14},
 number       = {1},
 pages        = {25--59},
 doi          = {10.1016/0169-7552(87)90085-7},
)
@inproceedings(csp2b99,
 author       = {M. Butler},
 year         = {1999},
 title        = {csp2{B} : {A} {P}ractical {A}pproach to {C}ombining {CSP} and {B}},
 booktitle    = {FM'99},
 series       = {{LNCS}},
 volume       = {1708},
 publisher    = {Springer-{V}erlag},
 address      = {Toulouse, France},
 pages        = {490--508},
 doi          = {10.1007/3-540-48119-2\_28},
)
@book(usingz,
 author       = {J. Davies and J.C.P. Woodcock},
 year         = {1996},
 title        = {Using {Z}: {S}pecification, {R}efinement, and {P}roof},
 publisher    = {Prentice-{H}all},
)
@inproceedings(DBLP:conf/zum/DerrickW05,
 author       = {John Derrick and Heike Wehrheim},
 year         = {2005},
 title        = {Non-atomic Refinement in {Z} and {CSP}},
 booktitle    = {ZB 2005: Formal Specification and Development in Z and B, 4th International Conference of B and Z Users},
 series       = {LNCS},
 volume       = {3455},
 publisher    = {Springer-{V}erlag},
 address      = {Guildford, UK},
 pages        = {24--44},
 url          = {http://dx.doi.org/10.1007/11415787_3},
)
@inproceedings(ar:mi-mde-10,
 author       = {Embe Jiague, M. and M. Frappier and F. Gervais and P. Konopacki and J. Milhau and R. Laleau and St-Denis, R.},
 year         = {2010},
 title        = {Model-Driven Engineering of Functional Security Policies},
 booktitle    = {International Conference on Enterprise Information Systems},
 volume       = {3},
 pages        = {374--379},
)
@techreport(Fayolle2014,
 author       = {T. Fayolle},
 year         = {2014},
 title        = {Specifying a {T}rain {S}ystem {U}sing {ASTD} and the {B} {M}ethod},
 type         = {Technical Report},
 url          = {www.lacl.fr/~tfayolle},
 note         = {Http://www.lacl.fr/\textasciitilde tfayolle},
)
@article(Ferrari2014,
 author       = {Alessio Ferrari and GiorgioO. Spagnolo and Giacomo Martelli and Simone Menabeni},
 year         = {2014},
 title        = {From commercial documents to system requirements: an approach for the engineering of novel {CBTC} solutions},
 journal      = {International Journal on Software Tools for Technology Transfer},
 pages        = {1--21},
 url          = {http://dx.doi.org/10.1007/s10009-013-0298-6},
)
@article(FrGeLaFrSt:2008:revueISSE,
 author       = {M. Frappier and F. Gervais and R. Laleau and B. Fraikin and St-Denis, R.},
 year         = {2008},
 title        = {Extending {S}tatecharts with {P}rocess {A}lgebra {O}perators},
 journal      = {Innovations in Systems and Software Engineering},
 volume       = {4},
 number       = {3},
 pages        = {285--292},
 doi          = {10.1007/s11334-008-0064-1},
)
@article(FACS-journal-2014,
 author       = {M. Frappier and F. Gervais and R. Laleau and J. Milhau},
 year         = {2014},
 title        = {Refinement patterns for {ASTD}s},
 journal      = {Formal Aspects of Computing},
 volume       = {26},
 number       = {5},
 pages        = {919--941},
 doi          = {10.1007/s00165-013-0286-3},
)
@techreport(MarcFrappier2008TR,
 author       = {Marc Frappier and Fr\IeC{\'e}d\IeC{\'e}ric Gervais and R\IeC{\'e}gine Laleau and Beno\IeC{\^\i}t Fraikin},
 year         = {2008},
 title        = {Algebraic {S}tate {T}ransition {D}iagrams},
 type         = {Technical Report},
 institution  = {Universit\IeC{\'e} de Sherbrooke},
)
@article(statecharts,
 author       = {D. Harel},
 year         = {1987},
 title        = {Statecharts: {A} {V}isual {F}ormalism for {C}omplex {S}ystems},
 journal      = {Science of {C}omputer {P}rogramming},
 volume       = {8},
 pages        = {231--274},
 doi          = {10.1016/0167-6423(87)90035-9},
)
@book(hoare,
 author       = {C.A.R. Hoare},
 year         = {1985},
 title        = {Communicating {S}equential {P}rocesses},
 publisher    = {Prentice-{H}all},
)
@book(hoarehe,
 author       = {C.A.R. Hoare and H. Jifeng},
 year         = {1998},
 title        = {Unifying {T}heories of {P}rogramming},
 publisher    = {Prentice-{H}all},
)
@inproceedings(DBLP:conf/asm/IliasovTLRVIL10,
 author       = {Alexei Iliasov and Elena Troubitsyna and Linas Laibinis and Alexander Romanovsky and Kimmo Varpaaniemi and Dubravka Ilic and Timo Latvala},
 year         = {2010},
 title        = {Supporting Reuse in Event B Development: Modularisation Approach},
 booktitle    = {Abstract State Machines, Alloy, B and Z, Second International Conference, ABZ 2010},
 series       = {LNCS},
 volume       = {5977},
 publisher    = {Springer-{V}erlag},
 pages        = {174--188},
 url          = {http://dx.doi.org/10.1007/978-3-642-11811-1_14},
)
@inproceedings(James,
 author       = {Philip James and Faron Moller and Hoang Nga Nguyen and Markus Roggenbach and Steve Schneider and Helen Treharne and Matthew Trumble and David Williams},
 year         = {2013},
 title        = {Verification of Scheme Plans using {CSP}$||${B}},
 booktitle    = {Towards a Formal Methods Body of Knowledge for Railway Control and Safety Systems},
 pages        = {14--20},
 doi          = {10.1007/978-3-319-05032-4\_15},
 url          = {http://orbit.dtu.dk/fedora/objects/orbit:125733/datastreams/file_555e08e8-0922-4f67-80f1-77cca11b5030/content#page=16},
)
@article(milhauUMLFM2011,
 author       = {J. Milhau and A. Idani and R. Laleau and M. Labiadh and Y. Ledru and M. Frappier},
 year         = {2011},
 title        = {Combining {{UML}}, {{ASTD}} and {{B}} for the formal specification of an access control filter},
 journal      = {Innovations in Systems and Software Engineering},
 volume       = {7(4)},
 pages        = {303--313},
 doi          = {10.1007/s11334-011-0166-z},
)
@phdthesis(oliveira2005refinement,
 author       = {MVM Oliveira},
 year         = {2005},
 title        = {A refinement calculus for {C}ircus},
 school       = {Department of Computer Science, The University of York},
)
@article(pnueli81,
 author       = {A. Pnueli},
 year         = {1981},
 title        = {The {T}emporal {S}emantics of {C}oncurrent {P}rograms},
 journal      = {Theoretical {C}omputer {S}cience},
 volume       = {13},
 pages        = {45--60},
 doi          = {10.1016/0304-3975(81)90110-9},
)
@book(roscoe97,
 author       = {A.W. Roscoe},
 year         = {1997},
 title        = {The Theory and Practice of Concurrency},
 publisher    = {Prentice-{H}all},
)
@article(DBLP:journals/fac/SchneiderT05,
 author       = {Steve Schneider and Helen Treharne},
 year         = {2005},
 title        = {{CSP} theorems for communicating {B} machines},
 journal      = {Formal Asp. Comput.},
 volume       = {17},
 number       = {4},
 pages        = {390--422},
 url          = {http://dx.doi.org/10.1007/s00165-005-0076-7},
)
@article(DBLP:journals/scp/SchneiderT11,
 author       = {Steve Schneider and Helen Treharne},
 year         = {2011},
 title        = {Changing system interfaces consistently: A new refinement strategy for {CSP}$||${B}},
 journal      = {Sci. Comput. Program.},
 volume       = {76},
 number       = {10},
 pages        = {837--860},
 url          = {http://dx.doi.org/10.1016/j.scico.2010.08.001},
)
@inbook(Silva2012,
 author       = {Renato Silva},
 year         = {2012},
 title        = {Thesis},
 chapter      = {Chapter 6 : Case Study},
 pages        = {121--160},
)
@inproceedings(treharne99using,
 author       = {H. Treharne and S. Schneider},
 year         = {1999},
 title        = {Using a {P}rocess {A}lgebra to {C}ontrol {B} operations},
 booktitle    = {{IFM}'99},
 publisher    = {Springer-{V}erlag},
 address      = {York, United Kingdom},
 pages        = {437--457},
 doi          = {10.1007/978-1-4471-0851-1\_23},
)
@inproceedings(circussem,
 author       = {J.C.P. Woodcock and A.L.C. Cavalcanti},
 year         = {2002},
 title        = {The {S}emantics of {C}ircus},
 booktitle    = {{ZB} 2002},
 series       = {{LNCS}},
 volume       = {2272},
 publisher    = {Springer-{V}erlag},
 address      = {Grenoble, {F}rance},
 pages        = {184--203},
 doi          = {10.1007/3-540-45648-1\_10},
)