@article(JML, author = {L. Burdy and Y. Cheon and D. R. Cok and M. D. Ernst and J. R. Kiniry and G. T. Leavens and K. R. M. Leino and E. Poll}, year = {2005}, title = {An Overview of JML Tools and Applications}, journal = {Int. J. Softw. Tools Technol. Transf.}, volume = {7}, number = {3}, pages = {212--232}, doi = {10.1007/s10009-004-0167-4}, ) @article(OhCircus, author = {A. Cavalcanti and A. Sampaio and J. Woodcock}, year = {2005}, title = {Unifying classes and processes}, journal = {{Software ~ \zamp~ Systems Modeling}}, volume = {4}, number = {3}, pages = {277--296}, doi = {10.1007/s10270-005-0085-2}, ) @inproceedings(CCO05, author = {A. L. C. Cavalcanti and P. Clayton and C. O'Halloran}, year = {2005}, title = {{Control Law Diagrams in \textsf{\emph{Circus}}}}, editor = {J. Fitzgerald and I. J. Hayes and A. Tarlecki}, booktitle = {{FM 2005:~ Formal Methods}}, series = {LNCS}, volume = {3582}, publisher = {Springer-Verlag}, pages = {253--268}, doi = {10.1007/11526841\unhbox\voidb@x \kern0.06em\vbox{\hrule width0.5em}18}, ) @article(Circus, author = {A. L. C. Cavalcanti and A. C. A. Sampaio and J. C. P. Woodcock}, year = {2003}, title = {{A Refinement Strategy for \textsf{\emph{Circus}}}}, journal = {Formal Aspects of Computing}, volume = {15}, number = {2 - 3}, pages = {146--181}, doi = {10.1007/s00165-003-0006-5}, ) @article(Cavalcanti2013, author = {A. L. C. Cavalcanti and F. Zeyda and A. Wellings and J. C. P. Woodcock and K. Wei}, year = {2013}, title = {{Safety-critical Java programs from \textsf{\emph{Circus}} models}}, journal = {{Real-Time Systems}}, volume = {49}, number = {5}, pages = {614--667}, doi = {10.1007/s11241-013-9182-4}, ) @inproceedings(Haddad, author = {G. Haddad and F. Hussain and G. T. Leavens}, year = {2010}, title = {The Design of SafeJML, a Specification Language for SCJ with Support for WCET Specification}, booktitle = {Proceedings of the 8th International Workshop on Java Technologies for Real-Time and Embedded Systems}, series = {JTRES '10}, publisher = {ACM}, pages = {155--163}, doi = {10.1145/1850771.1850793}, ) @book(UTP, author = {C. A. R. Hoare and J. He}, year = {1998}, title = {{Unifying Theories of Programming}}, publisher = {Prentice-Hall}, ) @inproceedings(Kalibera, author = {T. Kalibera and P. Parizek and M. Malohlava and M. Schoeberl}, year = {2010}, title = {Exhaustive Testing of Safety Critical Java}, booktitle = {Proceedings of the 8th International Workshop on Java Technologies for Real-Time and Embedded Systems}, series = {JTRES '10}, publisher = {ACM}, pages = {164--174}, doi = {10.1145/1850771.1850794}, ) @techreport(SCJ, author = {D. Locke and B. S. Andersen and B. Brosgol, M. Fulton and T. Henties and J. J. Hunt and J. O. Nielsen and K. Nielsen and M. Schoeberl and J. Vitek and A. Wellings}, title = {{}Safety-Critical Java Technology Specification}, type = {Technical Report}, ) @inproceedings(MC14a, author = {C. Marriott and A. L. C. Cavalcanti}, year = {2014}, title = {{SCJ: Memory-safety checking without annotations}}, booktitle = {Formal Methods}, series = {LNCS}, volume = {8442}, publisher = {Springer}, pages = {465--480}, doi = {10.1007/978-3-319-06410-9\unhbox\voidb@x \kern0.06em\vbox{\hrule width0.5em}32}, ) @phdthesis(Miyazawa2012, author = {A. Miyazawa}, year = {2012}, title = {{Formal verification of implementations of Stateflow charts}}, school = {{Department of Computer Scinece, The University of York, York, UK}}, ) @misc(MiyazawaReport2015, author = {A. Miyazawa and A. Cavalcanti}, year = {2015}, title = {Refinement of {\sf\slshape Circus}\ models into \textsf{\slshape SCJ-Circus}.}, note = {\url{http://www-users.cs.york.ac.uk/~ alvarohm/report2015a.pdf}}, ) @article(MC12, author = {A. Miyazawa and A. L. C. Cavalcanti}, year = {2012}, title = {{Refinement-oriented models of Stateflow charts}}, journal = {Science of Computer Programming}, volume = {77}, number = {10-11}, pages = {1151--1177}, doi = {10.1016/j.scico.2011.07.007}, ) @article(Miyazawa2013, author = {A. Miyazawa and A. L. C. Cavalcanti}, year = {2013}, title = {Refinement-based verification of implementations of Stateflow charts}, journal = {{Formal Aspects of Computing}}, volume = {26}, number = {2}, pages = {367--405}, doi = {10.1007/s00165-013-0291-6}, ) @phdthesis(Oli06, author = {M. V. M. Oliveira}, year = {2006}, title = {{Formal Derivation of State-Rich Reactive Programs Using {\sf\textsl {Circus}}}}, school = {University of York}, ) @book(Ros11, author = {A. W. Roscoe}, year = {2011}, title = {{Understanding Concurrent Systems}}, series = {Texts in Computer Science}, publisher = {Springer}, ) @inproceedings(Tang, author = {D. Tang and A. Plsek and J. Vitek}, year = {2010}, title = {Static Checking of Safety Critical Java Annotations}, booktitle = {Proceedings of the 8th International Workshop on Java Technologies for Real-Time and Embedded Systems}, series = {JTRES '10}, publisher = {ACM}, pages = {148--154}, doi = {10.1145/1850771.1850792}, ) @inproceedings(WWC12, author = {K. Wei and J. C. P. Woodcock and A. L. C. Cavalcanti}, year = {2012}, title = {{\textsf{\emph{Circus Time}} with Reactive Designs}}, booktitle = {4th International Symposium on Unifying Theories of Programming}, series = {LNCS}, doi = {10.1007/978-3-642-35705-3\unhbox\voidb@x \kern0.06em\vbox{\hrule width0.5em}3}, ) @book(RTSJ, author = {Andrew Wellings}, year = {2004}, title = {Concurrent and Real-Time Programming in Java}, publisher = {John Wiley ~ \zamp~ Sons}, ) @book(WD96, author = {J. C. P. Woodcock and J. Davies}, year = {1996}, title = {{Using Z---Specification, Refinement, and Proof}}, publisher = {Prentice-Hall}, ) @article(ZLCW13, author = {F. Zeyda and L. Lalkhumsanga and A. L. C. Cavalcanti and A. Wellings}, year = {2013}, title = {{\textsf{\emph{Circus}} Models for Safety-Critical Java Programs}}, journal = {{The Computer Journal}}, doi = {10.1093/comjnl/bxt060}, )