caa a22 4500 605516456 CHVBK 20210128100714.0 cr unu---uuuuu 210128e20150301xx s 000 0 eng 10.1007/s00165-014-0317-8 doi (NATIONALLICENCE)springer-10.1007/s00165-014-0317-8 Laws of mission-based programming [Elektronische Daten] [Frank Zeyda, Ana Cavalcanti] 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. British Computer Society, 2014 SCJ nationallicence Models nationallicence Refinement nationallicence Laws nationallicence Patterns nationallicence Automation nationallicence Proof nationallicence Circus nationallicence Zeyda Frank Department of Computer Science, Deramore Lane, University of York, YO10 5GH, Heslington, York, UK aut Cavalcanti Ana Department of Computer Science, Deramore Lane, University of York, YO10 5GH, Heslington, York, UK aut Formal Aspects of Computing Springer London 27/2(2015-03-01), 423-472 0934-5043 27:2<423 2015 27 165 https://doi.org/10.1007/s00165-014-0317-8 text/html Onlinezugriff via DOI BK010053 XK010053 XK010000 Metadata rights reserved Springer special CC-BY-NC licence nationallicence 1 research-article jats NATIONALLICENCE NATIONALLICENCE NL-springer NATIONALLICENCE 856 40 https://doi.org/10.1007/s00165-014-0317-8 text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Zeyda Frank Department of Computer Science, Deramore Lane, University of York, YO10 5GH, Heslington, York, UK aut NATIONALLICENCE 700 1- Cavalcanti Ana Department of Computer Science, Deramore Lane, University of York, YO10 5GH, Heslington, York, UK aut NATIONALLICENCE 773 0- Formal Aspects of Computing Springer London 27/2(2015-03-01), 423-472 0934-5043 27:2<423 2015 27 165