References

  1. J. R. Abrial (2007): The Event-B Book. Cambridge Univ. Press, Cambridge.
  2. Jean-Raymond Abrial (1996): The B-book: assigning programs to meanings. Cambridge Univ. Press, Cambridge, doi:10.1017/CBO9780511624162.
  3. 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.
  4. Eerke A. Boiten (2014): Introducing extra operations in refinement. Formal Asp. Comput. 26(2), pp. 305–317. Available at http://dx.doi.org/10.1007/s00165-012-0266-z.
  5. 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.
  6. 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.
  7. J. Davies & J.C.P. Woodcock (1996): Using Z: Specification, Refinement, and Proof. Prentice-Hall.
  8. 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.
  9. 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.
  10. 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.
  11. 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.
  12. 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.
  13. 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.
  14. Marc Frappier, Frédéric Gervais, Régine Laleau & Benoît Fraikin (2008): Algebraic State Transition Diagrams. Technical Report. Université de Sherbrooke.
  15. 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.
  16. C.A.R. Hoare (1985): Communicating Sequential Processes. Prentice-Hall.
  17. C.A.R. Hoare & H. Jifeng (1998): Unifying Theories of Programming. Prentice-Hall.
  18. 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.
  19. Philip James, Faron Moller, Hoang Nga Nguyen, Markus Roggenbach, Steve Schneider, Helen Treharne, Matthew Trumble & David Williams (2013): Verification of Scheme Plans using CSP||B. In: Towards a Formal Methods Body of Knowledge for Railway Control and Safety Systems, pp. 14–20, doi:10.1007/978-3-319-05032-4_15. Available at http://orbit.dtu.dk/fedora/objects/orbit:125733/datastreams/file_555e08e8-0922-4f67-80f1-77cca11b5030/content#page=16.
  20. 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.
  21. MVM Oliveira (2005): A refinement calculus for Circus. Department of Computer Science, The University of York.
  22. A. Pnueli (1981): The Temporal Semantics of Concurrent Programs. Theoretical Computer Science 13, pp. 45–60, doi:10.1016/0304-3975(81)90110-9.
  23. A.W. Roscoe (1997): The Theory and Practice of Concurrency. Prentice-Hall.
  24. 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.
  25. 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.
  26. Renato Silva (2012): Thesis, chapter Chapter 6 : Case Study, pp. 121–160.
  27. 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.
  28. 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.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org