L. Burdy, Y. Cheon, D. R. Cok, M. D. Ernst, J. R. Kiniry, G. T. Leavens, K. R. M. Leino & E. Poll (2005):
An Overview of JML Tools and Applications.
Int. J. Softw. Tools Technol. Transf. 7(3),
pp. 212–232,
doi:10.1007/s10009-004-0167-4.
A. Cavalcanti, A. Sampaio & J. Woodcock (2005):
Unifying classes and processes.
Software Systems Modeling 4(3),
pp. 277–296,
doi:10.1007/s10270-005-0085-2.
A. L. C. Cavalcanti, P. Clayton & C. O'Halloran (2005):
Control Law Diagrams in Circus.
In: J. Fitzgerald, I. J. Hayes & A. Tarlecki: FM 2005: Formal Methods,
LNCS 3582.
Springer-Verlag,
pp. 253–268,
doi:10.1007/11526841\voidb@x 0.06emwidth0.5em18.
A. L. C. Cavalcanti, A. C. A. Sampaio & J. C. P. Woodcock (2003):
A Refinement Strategy for Circus.
Formal Aspects of Computing 15(2 - 3),
pp. 146–181,
doi:10.1007/s00165-003-0006-5.
A. L. C. Cavalcanti, F. Zeyda, A. Wellings, J. C. P. Woodcock & K. Wei (2013):
Safety-critical Java programs from Circus models.
Real-Time Systems 49(5),
pp. 614–667,
doi:10.1007/s11241-013-9182-4.
G. Haddad, F. Hussain & G. T. Leavens (2010):
The Design of SafeJML, a Specification Language for SCJ with Support for WCET Specification.
In: Proceedings of the 8th International Workshop on Java Technologies for Real-Time and Embedded Systems,
JTRES '10.
ACM,
pp. 155–163,
doi:10.1145/1850771.1850793.
C. A. R. Hoare & J. He (1998):
Unifying Theories of Programming.
Prentice-Hall.
T. Kalibera, P. Parizek, M. Malohlava & M. Schoeberl (2010):
Exhaustive Testing of Safety Critical Java.
In: Proceedings of the 8th International Workshop on Java Technologies for Real-Time and Embedded Systems,
JTRES '10.
ACM,
pp. 164–174,
doi:10.1145/1850771.1850794.
D. Locke, B. S. Andersen, M. Fulton B. Brosgol, T. Henties, J. J. Hunt, J. O. Nielsen, K. Nielsen, M. Schoeberl, J. Vitek & A. Wellings:
Safety-Critical Java Technology Specification.
Technical Report.
A. Miyazawa (2012):
Formal verification of implementations of Stateflow charts.
Department of Computer Scinece, The University of York, York, UK.
A. Miyazawa & A. Cavalcanti (2015):
Refinement of Circus models into SCJ-Circus..
http://www-users.cs.york.ac.uk/~ alvarohm/report2015a.pdf.
A. Miyazawa & A. L. C. Cavalcanti (2012):
Refinement-oriented models of Stateflow charts.
Science of Computer Programming 77(10-11),
pp. 1151–1177,
doi:10.1016/j.scico.2011.07.007.
A. Miyazawa & A. L. C. Cavalcanti (2013):
Refinement-based verification of implementations of Stateflow charts.
Formal Aspects of Computing 26(2),
pp. 367–405,
doi:10.1007/s00165-013-0291-6.
M. V. M. Oliveira (2006):
Formal Derivation of State-Rich Reactive Programs Using Circus.
University of York.
A. W. Roscoe (2011):
Understanding Concurrent Systems.
Texts in Computer Science.
Springer.
D. Tang, A. Plsek & J. Vitek (2010):
Static Checking of Safety Critical Java Annotations.
In: Proceedings of the 8th International Workshop on Java Technologies for Real-Time and Embedded Systems,
JTRES '10.
ACM,
pp. 148–154,
doi:10.1145/1850771.1850792.
K. Wei, J. C. P. Woodcock & A. L. C. Cavalcanti (2012):
Circus Time with Reactive Designs.
In: 4th International Symposium on Unifying Theories of Programming,
LNCS,
doi:10.1007/978-3-642-35705-3\voidb@x 0.06emwidth0.5em3.
Andrew Wellings (2004):
Concurrent and Real-Time Programming in Java.
John Wiley Sons.
J. C. P. Woodcock & J. Davies (1996):
Using Z—Specification, Refinement, and Proof.
Prentice-Hall.
F. Zeyda, L. Lalkhumsanga, A. L. C. Cavalcanti & A. Wellings (2013):
Circus Models for Safety-Critical Java Programs.
The Computer Journal,
doi:10.1093/comjnl/bxt060.
eptcs@eptcs.org