Laws of mission-based programming
| LEADER | caa a22 4500 | ||
|---|---|---|---|
| 001 | 605516456 | ||
| 003 | CHVBK | ||
| 005 | 20210128100714.0 | ||
| 007 | cr unu---uuuuu | ||
| 008 | 210128e20150301xx s 000 0 eng | ||
| 024 | 7 | 0 | |a 10.1007/s00165-014-0317-8 |2 doi |
| 035 | |a (NATIONALLICENCE)springer-10.1007/s00165-014-0317-8 | ||
| 245 | 0 | 0 | |a Laws of mission-based programming |h [Elektronische Daten] |c [Frank Zeyda, Ana Cavalcanti] |
| 520 | 3 | |a 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. | |
| 540 | |a British Computer Society, 2014 | ||
| 690 | 7 | |a SCJ |2 nationallicence | |
| 690 | 7 | |a Models |2 nationallicence | |
| 690 | 7 | |a Refinement |2 nationallicence | |
| 690 | 7 | |a Laws |2 nationallicence | |
| 690 | 7 | |a Patterns |2 nationallicence | |
| 690 | 7 | |a Automation |2 nationallicence | |
| 690 | 7 | |a Proof |2 nationallicence | |
| 690 | 7 | |a Circus |2 nationallicence | |
| 700 | 1 | |a Zeyda |D Frank |u Department of Computer Science, Deramore Lane, University of York, YO10 5GH, Heslington, York, UK |4 aut | |
| 700 | 1 | |a Cavalcanti |D Ana |u Department of Computer Science, Deramore Lane, University of York, YO10 5GH, Heslington, York, UK |4 aut | |
| 773 | 0 | |t Formal Aspects of Computing |d Springer London |g 27/2(2015-03-01), 423-472 |x 0934-5043 |q 27:2<423 |1 2015 |2 27 |o 165 | |
| 856 | 4 | 0 | |u https://doi.org/10.1007/s00165-014-0317-8 |q text/html |z Onlinezugriff via DOI |
| 898 | |a BK010053 |b XK010053 |c XK010000 | ||
| 900 | 7 | |a Metadata rights reserved |b Springer special CC-BY-NC licence |2 nationallicence | |
| 908 | |D 1 |a research-article |2 jats | ||
| 949 | |B NATIONALLICENCE |F NATIONALLICENCE |b NL-springer | ||
| 950 | |B NATIONALLICENCE |P 856 |E 40 |u https://doi.org/10.1007/s00165-014-0317-8 |q text/html |z Onlinezugriff via DOI | ||
| 950 | |B NATIONALLICENCE |P 700 |E 1- |a Zeyda |D Frank |u Department of Computer Science, Deramore Lane, University of York, YO10 5GH, Heslington, York, UK |4 aut | ||
| 950 | |B NATIONALLICENCE |P 700 |E 1- |a Cavalcanti |D Ana |u Department of Computer Science, Deramore Lane, University of York, YO10 5GH, Heslington, York, UK |4 aut | ||
| 950 | |B NATIONALLICENCE |P 773 |E 0- |t Formal Aspects of Computing |d Springer London |g 27/2(2015-03-01), 423-472 |x 0934-5043 |q 27:2<423 |1 2015 |2 27 |o 165 | ||