University | Computer Science  

    Circus Family hiJaC 




 

                                                             Theses

 
  • C. Marriott. Checking Memory Safety of Level 1 Safety-Critical Java Programs using Static-Analysis without Annotations. PhD Thesis, Department of Computer Science, University of York, UK, 2014. [PDF]
 

                                           Conference and Journal Papers

  • M. Luckcuck, A. L. C. Cavalcanti, and A. Wellings. A Formal Model of the Safety-Critical Java Level 2 Paradigm. In 12th International Conference on Integrated Formal Methods, 2016. (to appear) [PDF]
  • M. Luckcuck. A Formal Model for the SCJ Level 2 Paradigm. In Proceedings of the Doctoral Symposium of Formal Methods 2015, ISBN 978-82-7368-410-3. [PDF | Proceedings]
  • A. Miyazawa, A. L. C. Cavalcanti. Refinement strategy for Safety-Critical Java. In SBMF 2015, Brazilian Symposium on Formal Methods, 2015.
  • A. Miyazawa, A. L. C. Cavalcanti. SCJ-Circus: a refinement-oriented formal notation for Safety-Critical Java. In REFINE Workshop, 2015
  • C. Marriott and A. L. C. Cavalcanti. SCJ: Memory-safety checking without annotations. In Formal Methods, volume 8442 of Lecture Notes in Computer Science, pages 465-480. Springer, 2014
  • F. Zeyda and A. L. C. Cavalcanti. Laws of mission-based programming. In Formal Aspects of Computing, 2014 (Accepted for publication).
  • A. L. .C Cavalcanti, A. Wellings, and J. C. P. Woodcock. The Safety-Critical Java memory model formalised. In Formal Aspects of Computing, 25(1):37-57, 2013. DOI: 10.1007/s00165-012-0253-4.
  • A. L. C. Cavalcanti, F. Zeyda, A. Wellings, J. C. P. Woodcock, and K. Wei. Safety-critical Java programs from Circus models. In Real-Time Systems, 49(5):614-667, 2013.
  • F. Zeyda, A. L. C. Cavalcanti. Refining SCJ Mission Specifications into Parallel Handler Designs. In 16th International Refinement Workshop (J. Derrick, E. A. Boiten, S. Reeves, eds.), vol. 115, pp. 52-67, 2013.
  • F. Zeyda, L. Lalkhumsanga, A. L. C. Cavalcanti, and A. Wellings. Circus Models for Safety-Critical Java Programs. In The Computer Journal, 2013. Online first. DOI: 10.1093/comjnl/bxt060.
  • A. J. Wellings, M. Luckcuck, and A. L. C Cavalcanti. Safety-critical Java level 2: motivations, example applications and issues. In F. Siebert and K. Nilsen, editors, The 11th International Workshop on Java Technologies for Real-time and Embedded Systems, pages 48-57. ACM, 2013.
  • F. Zeyda and A. L. C. Cavalcanti. Higher-Order UTP in Theories of Object-Orientation. In 4th International Symposium on Unifying Theories of Programming, Lecture Notes in Computer Science, 2012.
  • K. Wei, J. C. P. Woodcock, and A. L. C. Cavalcanti.Circus Time with Reactive Designs. In 4th International Symposium on Unifying Theories of Programming, Lecture Notes in Computer Science, 2012.
  • N. K. Singh, A. J. Wellings, and A. L. C. Cavalcanti. The cardiac pacemaker case study and its implementation in safety-critical Java and Ravenscar Ada. In 10th International Workshop on Java Technologies for Real-time and Embedded Systems, pages 62-71. ACM, 2012.
  • F. Zeyda, A. Cavalcanti, and A. Wellings. The Safety-Critical Java Mission Model: A Formal Account. In Formal Methods and Software Engineering, volume 6991 of Lecture Notes in Computer Science, pages 49-65. Springer, October 2011.
  • Ana Cavalcanti, Andy Wellings, Jim Woodcock, Kun Wei, and Frank Zeyda. Safety-critical Java in Circus. In Proceedings of the 9th International Workshop on Java Technologies for Real-Time and Embedded Systems (JTRES '11). ACM, New York, NY, USA.
  • A. L. C. Cavalcanti, A. Wellings, and J. C. P. Woodcock. The Safety-critical Java Memory Model: a formal account. In M. Butler and W. Schulte, editors, Formal Methods, volume 6664 of Lecture Notes in Computer Science, pages 246-261. Springer-Verlag, 2011.

 

                                                          Technical Reports

 
  • Ana Cavalcanti, Wen-ling Huang, Jan Peleska and Jim Woodcock. CSP and Kripke structures. Technical report, Department of Computer Science, University of York, UK, 2015. [Bib | PDF]
  • Kun Wei, Jim Woodcock and Ana Cavalcanti. Operational Semantics for Circus Time. Technical report, Department of Computer Science, University of York, UK, 2013. [Bib | PDF]
  • F. Zeyda, A.L.C. Cavalcanti, A. Wellings, Jim Woodcock and Kun Wei. Refinement of the Parallel CDx. Technical Report. University of York, UK, July 2012. [Bib | PDF]
  • Kun Wei, Jim Woodcock and Ana Cavalcanti. New Circus Time. Technical report, Department of Computer Science, University of York, UK, 2012. [Bib | PDF]
  • F. Zeyda, A.L.C. Cavalcanti, and A. Wellings. Circus Model for the SCJ Mission Framework. Technical Report. University of York, UK, 2011. [Bib | PDF]
  • F. Zeyda, A.L.C. Cavalcanti, and A. Wellings. A Simple Protocol - Safety-Critical Java Program and its Circus Model. Technical Report. University of York, UK, 2011. [Bib | PDF]
  • J. Baxter. Requirements for Safety-Critical Java Virtual Machines. Technical Report. University of York, UK, July 2015. [Bib | PDF]
  • M. Luckcuck. Safety-Critical Java Level 2 Framework Model. Technical Report. University of York, UK, January 2016. [Bib | PDF]
 
 

 

   

       Department of Computer Science

       University of York, Deramore Lane, York, YO10 3TA, UK

       Tel: 01904 325500 | Fax:01904 325599                                                                                                 Last updated on 28 October 2014