Abstract
Safety-Critical Java (SCJ) is a recent technology that changes the execution and memory model of Java in such a way that applications can be statically analysed and certified for their real-time properties and safe use of memory. Our interest is in the development of comprehensive and sound techniques for the formal specification, refinement, design, and implementation of SCJ programs, using a correct-by-construction approach. As part of this work, we present here an account of laws and patterns that are of general use for the refinement of SCJ mission specifications into designs of parallel handlers, as they are used in the SCJ programming paradigm. Our refinement notation is a combination of languages from the Circus family, supporting state-rich reactive models with the addition of class objects and real-time properties. Starting from a sequential and centralised Circus specification, our laws permit refinement into Circus models of SCJ program designs. Automation and proof of the refinement laws is examined here, too. Our work is an important step towards eliciting laws of programming for SCJ and fits into a refinement strategy that we have developed previously to derive SCJ programs from specifications in a rigorous manner.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Abrial JR (2010) Modeling in Event-B. Cambridge University Press, Cambridge
Abrial J-R, Hallerstede S (2007) Refinement, decomposition, and instantiation of discrete models: application to Event-B. Fundamenta Informaticae 77(1–2): 1–28
Back RJR (1989) Refinement calculus, Part II: parallel and reactive programs. In: Stepwise refinement of distributed systems models, formalisms, correctness. LNCS, vol 430. Springer, Berlin, pp 67–93
Back RJR, Kurki-Suonio R (1983) Decentralization of process nets with centralized control. In: Proceedings of PODC ’83, second ACM symposium on principles of distributed computing. ACM, New York, pp 131–142
Burns A (1999) The Ravenscar profile. ACM SIGAda Ada Lett XIX 4: 49–52
Butler M (2009) Decomposition structures for Event-B. In: Proceedings of IFM 2009, integrated formal methods. LNCS, vol 5423. Springer, Berlin, pp 20–38
Back RJR, von Wright J (2003) Compositional action system refinement. Formal Aspects Comput 15(2–3): 103–117
Cavalcanti A (1997) A refinement calculus for Z. PhD thesis, University of Oxford, Oxford
Cavalcanti A, Clayton P, O’Halloran C (2011) From control law diagrams to Ada via Circus. Formal Aspects Comput 23(4): 465–512
Cansell D, Méry D, Rehm J Time constraint patterns for Event B development. In: Proceedings of B 2007: formal specification and development in B. LNCS, vol 4355. Springer, Berlin, pp 140–154
Cavalcanti A, Sampaio A, Woodcock J (2003) A refinement strategy for Circus. Formal Aspects Comput 15(2–3): 146–181
Cavalcanti A, Sampaio A, Woodcock J (2005) Unifying classes and processes. Softw Syst Model 4(3): 277–296
Cavalcanti A, Woodcock J (1998) ZRC—a refinement calculus for Z. Formal Aspects Comput 10(3): 267–289
Cavalcanti A, Wellings A, Woodcock J (2011) The Safety-Critical Java memory model: a formal account. In: Proceedings of FM 2011: formal methods. LNCS, vol 6664. Springer, Berlin, pp 246–261
Cavalcanti A, Wellings A, Woodcock J, Wei K, Zeyda F (2011) Safety-Critical Java in Circus. In: Proceedings of JTRES 2011, 9th international workshop on java technologies for real-time and embedded systems. ACM, New York, pp 20–29
Cavalcanti A, Zeyda F, Wellings A, Woodcock J, Wei K (2013) Safety-Critical Java programs from Circus models. Real-time Syst 49: 614–667
Dalsgaard AE, Hansen RR, Schoeberl M (2012) Private memory allocation analysis for Safety-Critical Java. In: Proceedings of JTRES 2012, 10th international workshop on java technologies for real-time and embedded systems. ACM, New York, pp 9–17
Groves L (2002) Refinement and the Z schema calculus. In: Proceedings of REFINE 2002: The BCS FACS refinement workshop–ENTCS 7037093
Henties T, Hunt JJ, Locke D, Nilsen K, Schoeberl M, Vitek J (2009) Java for safety-critical applications. In: Proceedings of SafeCert 2009, pp 1–11
Hoare CAR, Jifeng H (1998) Unifying theories of programming. Prentice Hall Series in Computer Science. Prentice Hall, Upper Saddle River
Haddad G, Leavens GT (2011) Specifying subtypes in SCJ programs. In Proceedings of JTRES 2011, 9th international workshop on java technologies for real-time and embedded systems. ACM, New York, pp 40–46
Hayes IJ, Utting M (2001) A sequential real-time refinement calculus. Acta Informatica 37(6): 385–448
Kalibera T, Hagelberg J, Pizlo F, Plsek A, Titzer B, Vitek J (2009) CD x : A family of real-time Java benchmarks. In: Proceedings of JTRES 2009, 7th international workshop on Java technologies for real-time and embedded systems. ACM, New York, pp 41–50
Morgan CC (1994) Programming from specifications. Prentice Hall International Series in Computer Science. Prentice Hall, Upper Saddle River
Norrish M (2003) Complete integer decision procedures as derived rules in HOL. In: Proceedings of TPHOLs 2003, theorem proving in higher order logics. LNCS, vol 2758. Springer, Berlin, pp 71–86
Oliveira M, Cavalcanti A, Woodcock J (2009) A UTP semantics for Circus. Formal Aspects Comput 21(1–2): 3–32
Oliveira M (2005) Formal derivation of state-rich reactive programs using Circus. PhD thesis, University of York, York
Oliveira M, Zeyda F, Cavalcanti A (2011) A tactic language for refinement of state-rich concurrent specifications. Sci Comput Program 76(9): 792–833
Pizlo F, Fox JM, Holmes D, Vitek J (2004) Real-time Java scoped memory: design patterns and semantics. In Proceedings of the seventh IEEE international symposium on object-oriented real-time distributed computing. IEEE, New York, pp 101–110
Roscoe AW (1997) The theory and practice of concurrency. Prentice Hall Series in Computer Science. Prentice Hall, Upper Saddle River
Roscoe AW (2011) Understanding concurrent systems. Texts in Computer Science. Springer, Berlin
Reed GM, Roscoe AW (1988) A timed model for communicating sequential processes. Theor Comput Sci 58(1–3): 249–261
RTCA/EUROCAE joint committee (2011) Software considerations in airborne systems and equipment certification. Technical Report DO-178C, RTCA Inc.
Sherif A, Cavalcanti A, Jifeng H, Sampaio A (2010) A process algebraic framework for specification and validation of real-time systems. Formal Aspects Comput 22(2): 153–191
Schneider S, Treharne H (2005) CSP theorems for communicating B machines. Formal Aspects Comput 17(4): 390–422
Søndergaard H, Thomsen B, Ravn AP (2006) A Ravenscar-Java profile implementation. In: Proceedings of JTRES 2006, 4th international workshop on Java technologies for real-time and embedded systems. ACM, New York, pp 38–47
Schneider S, Treharne H, Wehrheim H (2010) A CSP approach to control in Event-B. In: Proceedings of IFM 2010, integrated formal methods. LNCS, vol 6396. Springer, Berlin, pp 260–274
The Open Group (2011) Safety Critical Java technology specification—Version 0.94. Technical Report JSR-302, Java Community Process. http://jcp.org/en/jsr/detail?id=302
Tang D, Plsek A, Vitek J (2010) Static checking of Safety Critical Java annotations. In: Proceedings of JTRES 2010, 8th international workshop on Java Technologies for real-time and embedded systems. ACM, New York, pp 148–154
Wilhelm R et al (2008) The worst-case execution-time problem—overview of methods and survey of tools. ACM Trans Embed Comput Syst 7(3): 36–13653
Woodcock J, Davies J (1996) Using Z: specification, refinement and proof. Prentice Hall International Series in Computer Science. Prentice Hall, Upper Saddle River
Wellings A (2004) Concurrent and real-time programming in Java. Wiley, West Sussex
Woodcock J (2013) CML definition 4. Technical Report COMPASS Deliverable 23.5, Seventh framework programme: comprehensive modelling for advanced systems of systems, Grant Agreement 287829. http://www.compass-research.eu/deliverables.html
Zeyda F, Cavalcanti A (2013) Refining SCJ mission specifications into parallel handler designs. In: Proceedings of REFINE 2013: 16th BCS FACS refinement workshop–EPTCS 1155267
Zeyda F, Cavalcanti A, Wellings A (2011) The Safety-Critical Java mission model: a formal account. In: Proceedings of ICFEM 2011, 13th international conference on formal engineering methods. LNCS, vol 6991. Springer, Berlin, pp 49–65
Zeyda F, Cavalcanti A, Wellings A, Woodcock J, Wei K (2012) Refinement of the parallel CD x . Technical report, University of York, York. http://www.cs.york.ac.uk/circus/publications/techreports/
Zeyda F, Lalkhumsanga L, Cavalcanti A, Wellings A (2013) Circus Models for Safety-Critical Java programs. Comput J 57(7): 1046–1091
Zeyda F, Oliveira M, Cavalcanti A (2012) Mechanised support for sound refinement tactics. Formal Aspects Comput 24(1): 127–160
Author information
Authors and Affiliations
Corresponding author
Additional information
Eerke Boiten, John Derrick, Steve Reeves and Cliff Jones
Rights and permissions
About this article
Cite this article
Zeyda, F., Cavalcanti, A. Laws of mission-based programming. Form Asp Comp 27, 423–472 (2015). https://doi.org/10.1007/s00165-014-0317-8
Received:
Revised:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00165-014-0317-8