Remember Me
Or use your Academic/Social account:


Or use your Academic/Social account:


You have just completed your registration at OpenAire.

Before you can login to the site, you will need to activate your account. An e-mail will be sent to you with the proper instructions.


Please note that this site is currently undergoing Beta testing.
Any new content you create is not guaranteed to be present to the final version of the site upon release.

Thank you for your patience,
OpenAire Dev Team.

Close This Message


Verify Password:
Verify E-mail:
*All Fields Are Required.
Please Verify You Are Human:
fbtwitterlinkedinvimeoflicker grey 14rssslideshare1
Miyazawa, Alvaro; Cavalcanti, Ana (2016)
Publisher: Open Publishing Association
Journal: Electronic Proceedings in Theoretical Computer Science
Languages: English
Types: Article
Subjects: Computer Science - Programming Languages, Mathematics, Electronic computers. Computer science, Computer Science - Logic in Computer Science, Computer Science - Software Engineering, QA1-939, QA75.5-76.95

Classified by OpenAIRE into

ACM Ref: GeneralLiterature_MISCELLANEOUS
Safety-Critical Java (SCJ) is a version of Java whose goal is to support the development of real-time, embedded, safety-critical software. In particular, SCJ supports certification of such software by introducing abstractions that enforce a simpler architecture, and simpler concurrency and memory models. In this paper, we present SCJ-Circus, a refinement-oriented formal notation that supports the specification and verification of low-level programming models that include the new abstractions introduced by SCJ. SCJ-Circus is part of the family of state-rich process algebra Circus, as such, SCJ-Circus includes the Circus constructs for modelling sequential and concurrent behaviour, real-time and object orientation. We present here the syntax and semantics of SCJ-Circus, which is defined by mapping SCJ-Circus constructs to those of standard Circus. This is based on an existing approach for modelling SCJ programs. We also extend an existing Circus-based refinement strategy that targets SCJ programs to account for the generation of SCJ-Circus models close to implementations in SCJ.
  • The results below are discovered through our pilot algorithms. Let us know how we are doing!

    • [1] 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.
    • [2] 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.
    • [3] A. L. C. Cavalcanti, P. Clayton & C. O'Halloran (2005): Control Law Diagrams in Circus. In J. Fitzgerald, I. J. Hayes & A. Tarlecki, editors: FM 2005: Formal Methods, LNCS 3582, Springer-Verlag, pp. 253-268, doi:10.1007/11526841 18.
    • [4] 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.
    • [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.
    • [6] 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.
    • [7] C. A. R. Hoare & J. He (1998): Unifying Theories of Programming. Prentice-Hall.
    • [8] 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.
    • [9] 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.
    • [10] C. Marriott & A. L. C. Cavalcanti (2014): SCJ: Memory-safety checking without annotations. In: Formal Methods, LNCS 8442, Springer, pp. 465-480, doi:10.1007/978-3-319-06410-9 32.
    • [11] A. Miyazawa (2012): Formal verification of implementations of Stateflow charts. Ph.D. thesis, Department of Computer Scinece, The University of York, York, UK.
    • [12] A. Miyazawa & A. Cavalcanti (2015): Refinement of Circus models into SCJ-Circus. http://www-users. cs.york.ac.uk/~alvarohm/report2015a.pdf.
    • [13] 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.
    • [14] 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.
    • [15] M. V. M. Oliveira (2006): Formal Derivation of State-Rich Reactive Programs Using Circus. Ph.D. thesis, University of York.
    • [16] A. W. Roscoe (2011): Understanding Concurrent Systems. Texts in Computer Science, Springer.
    • [17] 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.
    • [18] 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 3.
    • [19] Andrew Wellings (2004): Concurrent and Real-Time Programming in Java. John Wiley & Sons.
    • [20] J. C. P. Woodcock & J. Davies (1996): Using Z-Specification, Refinement, and Proof. Prentice-Hall.
    • [21] 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.
  • No related research data.
  • No similar publications.

Share - Bookmark

Funded by projects

Cite this article