References

  1. J. R. Abrial (2010): Modeling in Event-B. Cambridge University Press, Cambridge, CB2 8BS, UK, doi:10.1017/CBO9781139195881.
  2. R. J. R. Back (1990): Refinement Calculus, Part II: Parallel and Reactive Programs. In: Stepwise Refinement of Distributed Systems Models, Formalisms, Correctness, LNCS 430. Springer, pp. 67–93, doi:10.1007/3-540-52559-9\voidb@x 0.06emwidth0.5em61.
  3. R. J. R. Back & R. Kurki-Suonio (1983): Decentralization of Process Nets with Centralized Control. In: Proceedings of PODC '83. ACM, pp. 131–142, doi:10.1145/800221.806716.
  4. R. J. R. Back & J. von Wright (2003): Compositional Action System Refinement. Formal Aspects of Computing 15, pp. 103–117, doi:10.1007/s00165-003-0005-6.
  5. A. Burns (1999): The Ravenscar Profile. ACM SIGAda Ada Letters XIX, pp. 49–52, doi:10.1145/340396.340450.
  6. M. Butler (2009): Decomposition Structures for Event-B. In: Proceedings of IFM 2009, LNCS 5423. Springer, Düsseldorf, Germany, pp. 20–38, doi:10.1007/978-3-642-00255-7\voidb@x 0.06emwidth0.5em2.
  7. D. Cansell, D. Méry & J. Rehm (2006): Time Constraint Patterns for Event B Development. In: Proceedings of B 2007, LNCS 4355. Springer, Besançon, France, pp. 140–154, doi:10.1007/11955757\voidb@x 0.06emwidth0.5em13.
  8. A. Cavalcanti (1997): A Refinement Calculus for Z. University of Oxford, UK, Oxford, OX1 3QD, UK. Available at http://www.cs.ox.ac.uk/files/3451/PRG123.pdf.
  9. A. Cavalcanti, A. Sampaio & J. Woodcock (2003): A Refinement Strategy for Circus. Formal Aspects of Computing 15, pp. 146–181, doi:10.1007/s00165-003-0006-5.
  10. A. Cavalcanti, A. Sampaio & J. Woodcock (2005): Unifying classes and processes. Software and Systems Modeling 4(3), pp. 277–296, doi:10.1007/s10270-005-0085-2.
  11. A. Cavalcanti, A. Wellings & J. Woodcock (2011): The Safety-Critical Java Memory Model: A Formal Account. In: Proceedings of FM 2011, LNCS 6664. Springer, Limerick, Ireland, pp. 246–261, doi:10.1007/978-3-642-21437-0\voidb@x 0.06emwidth0.5em20.
  12. A. Cavalcanti, F. Zeyda, A. Wellings, J. Woodcock & K. Wei (2012): Safety-Critical java programs from Circus models. Real-time Systems, doi:10.1007/s11241-013-9182-4. Under publication..
  13. A. Dalsgaard, R. Hansen & M. Schoeberl (2012): Private Memory Allocation Analysis for Safety-Critical Java. In: Proceedings of JTRES 2012. ACM, pp. 9–17, doi:10.1145/2388936.2388939.
  14. L. Groves (2002): Refinement and the Z Schema Calculus. Electronic Notes in Theoretical Computer Science 70, pp. 70–93, doi:10.1016/S1571-0661(05)80486-4.
  15. G. Haddad & G. Leavens (2011): Specifying Subtypes in SCJ Programs. In: Proceedings of JTRES 2011. ACM, pp. 40–46, doi:10.1145/2043910.2043917.
  16. T. Henties, J. Hunt, D. Locke, K. Nilsen, M. Schoeberl & J. Vitek (2009): Java for Safety-Critical Applications. In: Proceedings of SafeCert 2009, York, UK, pp. 1–11. Available at http://www.vmars.tuwien.ac.at/php/pserver/extern/download.php?fileid=1641.
  17. C. A. R. Hoare & H. Jifeng (1998): Unifying Theories of Programming. Prentice Hall Series in Computer Science. Prentice Hall, Upper Saddle River, NJ, USA.
  18. T. Kalibera, J. Hagelberg, F. Pizlo, A. Plsek, B. Titzer & J. Vitek (2009): CD_x: A Family of Real-time Java Benchmarks. In: Proceedings of JTRES 2009. ACM, pp. 41–50, doi:10.1145/1620405.1620412.
  19. C. C. Morgan (1990): Programming from Specifications. Prentice Hall International Series in Computer Science. Prentice Hall, Upper Saddle River, NJ, USA.
  20. M. Oliveira (2005): Formal Derivation of State-Rich Reactive Programs using Circus. University of York, York, YO10 5GH, UK. Available at http://www.cs.york.ac.uk/circus/publications/papers/06-oliveira.pdf.
  21. M. Oliveira, A. Cavalcanti & J. Woodcock (2009): A UTP semantics for Circus. Formal Aspects of Computing 21, pp. 3–32, doi:10.1007/s00165-007-0052-5.
  22. A. W. Roscoe (1997): The Theory and Practice of Concurrency. Prentice Hall Series in Computer Science. Prentice Hall, Upper Saddle River, NJ, USA.
  23. A. Sherif, A. Cavalcanti, H. Jifeng & A. Sampaio (2009): A process algebraic framework for specification and validation of real-time systems. Formal Aspects of Computing 22, pp. 153–191, doi:10.1007/s00165-009-0119-6.
  24. H. Søndergaard, B Thomsen & A. P. Ravn (2006): A Ravenscar-Java Profile Implementation. In: Proceedings of JTRES 2006. ACM, Paris, France, pp. 38–47, doi:10.1145/1167999.1168008.
  25. D. Tang, A. Plsek & J. Vitek (2010): Static Checking of Safety Critical Java Annotations. In: Proceedings of JTRES 2010. ACM, pp. 148–154, doi:10.1145/1850771.1850792.
  26. The Open Group (2011): Safety Critical Java Technology Specification. Technical Report JSR-302. Java Community Process. Available at http://jcp.org/en/jsr/detail?id=302.
  27. A. Wellings (2004): Concurrent and Real-Time Programming in Java. Wiley, West Sussex, PO19 8SQ, UK.
  28. J. Woodcock & J. Davies (1996): Using Z: Specification, Refinement and Proof. Prentice Hall International Series in Computer Science. Prentice Hall, Upper Saddle River, NJ, USA.
  29. F. Zeyda, A. Cavalcanti & A. Wellings (2011): The Safety-Critical Java Mission Model: A Formal Account. In: Proceedings of ICFEM 2011, LNCS 6991. Springer, Durham, UK, pp. 49–65, doi:10.1007/978-3-642-24559-6\voidb@x 0.06emwidth0.5em6.
  30. F. Zeyda, A. Cavalcanti, A. Wellings, J. Woodcock & K. Wei (2012): Refinement of the Parallel CD_x. Technical Report. University of York, York, UK. Available at http://www.cs.york.ac.uk/circus/publications/techreports/.
  31. F. Zeyda, M. Oliveira & A. Cavalcanti (2012): Mechanised support for sound refinement tactics. Formal Aspects of Computing 24(1), pp. 127–160, doi:10.1007/s00165-011-0218-z.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org