×

zbMATH — the first resource for mathematics

Laws of mission-based programming. (English) Zbl 1331.68054
Summary: 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.
MSC:
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)
Software:
ArcAngelC; Circus; CirCUs; Z; ZRC
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Abrial JR (2010) Modeling in Event-B. Cambridge University Press, Cambridge · Zbl 1213.68214
[2] Abrial, J-R; Hallerstede, S, Refinement, decomposition, and instantiation of discrete models: application to event-B, Fundamenta Informaticae, 77, 1-28, (2007) · Zbl 1118.68392
[3] 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
[4] 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
[5] Burns, A, The ravenscar profile, ACM SIGAda Ada Lett XIX, 4, 49-52, (1999)
[6] Butler M (2009) Decomposition structures for Event-B. In: Proceedings of IFM 2009, integrated formal methods. LNCS, vol 5423. Springer, Berlin, pp 20-38 · Zbl 0934.68062
[7] Back, RJR; Wright, J, Compositional action system refinement, Formal Aspects Comput, 15, 103-117, (2003) · Zbl 1093.68007
[8] Cavalcanti A (1997) A refinement calculus for Z. PhD thesis, University of Oxford, Oxford
[9] Cavalcanti, A; Clayton, P; O’Halloran, C, From control law diagrams to ada via circus, Formal Aspects Comput, 23, 465-512, (2011) · Zbl 1226.68028
[10] 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 · Zbl 0655.68031
[11] Cavalcanti, A; Sampaio, A; Woodcock, J, A refinement strategy for circus, Formal Aspects Comput, 15, 146-181, (2003) · Zbl 1093.68555
[12] Cavalcanti, A; Sampaio, A; Woodcock, J, Unifying classes and processes, Softw Syst Model, 4, 277-296, (2005)
[13] Cavalcanti, A; Woodcock, J, ZRC—a refinement calculus for Z, Formal Aspects Comput, 10, 267-289, (1998) · Zbl 0934.68062
[14] 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
[15] 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 · Zbl 1285.68037
[16] Cavalcanti, A; Zeyda, F; Wellings, A; Woodcock, J; Wei, K, Safety-critical Java programs from circus models, Real-time Syst, 49, 614-667, (2013) · Zbl 1285.68037
[17] 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 · Zbl 0655.68031
[18] Groves, L, Refinement and the Z schema calculus, In: Proceedings of REFINE, 2002, the bcs facs refinement workshop-entcs 7037093, (2002)
[19] 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 · Zbl 1218.68101
[20] Hoare CAR, Jifeng H (1998) Unifying theories of programming. Prentice Hall Series in Computer Science. Prentice Hall, Upper Saddle River
[21] 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 · Zbl 1093.68555
[22] Hayes, IJ; Utting, M, A sequential real-time refinement calculus, Acta Informatica, 37, 385-448, (2001) · Zbl 0970.68107
[23] 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 · Zbl 1226.68028
[24] Morgan CC (1994) Programming from specifications. Prentice Hall International Series in Computer Science. Prentice Hall, Upper Saddle River · Zbl 0829.68083
[25] 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 · Zbl 1279.68292
[26] Oliveira, M; Cavalcanti, A; Woodcock, J, A UTP semantics for circus, Formal Aspects Comput, 21, 3-32, (2009) · Zbl 1165.68048
[27] Oliveira M (2005) Formal derivation of state-rich reactive programs using Circus. PhD thesis, University of York, York
[28] Oliveira, M; Zeyda, F; Cavalcanti, A, A tactic language for refinement of state-rich concurrent specifications, Sci Comput Program, 76, 792-833, (2011) · Zbl 1218.68101
[29] 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
[30] Roscoe AW (1997) The theory and practice of concurrency. Prentice Hall Series in Computer Science. Prentice Hall, Upper Saddle River
[31] Roscoe AW (2011) Understanding concurrent systems. Texts in Computer Science. Springer, Berlin
[32] Reed, GM; Roscoe, AW, A timed model for communicating sequential processes, Theor Comput Sci, 58, 249-261, (1988) · Zbl 0655.68031
[33] RTCA/EUROCAE joint committee (2011) Software considerations in airborne systems and equipment certification. Technical Report DO-178C, RTCA Inc.
[34] Sherif, A; Cavalcanti, A; Jifeng, H; Sampaio, A, A process algebraic framework for specification and validation of real-time systems, Formal Aspects Comput, 22, 153-191, (2010) · Zbl 1214.68224
[35] Schneider, S; Treharne, H, CSP theorems for communicating B machines, Formal Aspects Comput, 17, 390-422, (2005) · Zbl 1103.68599
[36] 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
[37] 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
[38] 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
[39] 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
[40] Wilhelm, R; etal., The worst-case execution-time problem—overview of methods and survey of tools, ACM Trans Embed Comput Syst, 7, 36-13653, (2008)
[41] Woodcock J, Davies J (1996) Using Z: specification, refinement and proof. Prentice Hall International Series in Computer Science. Prentice Hall, Upper Saddle River · Zbl 0855.68060
[42] Wellings A (2004) Concurrent and real-time programming in Java. Wiley, West Sussex
[43] 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
[44] 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
[45] 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
[46] 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/
[47] Zeyda, F; Lalkhumsanga, L; Cavalcanti, A; Wellings, A, circus models for safety-critical Java programs, Comput J, 57, 1046-1091, (2013)
[48] Zeyda, F; Oliveira, M; Cavalcanti, A, Mechanised support for sound refinement tactics, Formal Aspects Comput, 24, 127-160, (2012) · Zbl 1242.68077
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.