{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:27:36Z","timestamp":1725488856670},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540403760"},{"type":"electronic","value":"9783540449478"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-44947-7_5","type":"book-chapter","created":{"date-parts":[[2007,8,8]],"date-time":"2007-08-08T02:04:46Z","timestamp":1186538686000},"page":"80-91","source":"Crossref","is-referenced-by-count":5,"title":["Adding Temporal Annotations and Associated Verification to the Ravenscar Profile"],"prefix":"10.1007","author":[{"given":"Alan","family":"Burns","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tse-Min","family":"Lin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2003,6,18]]},"reference":[{"issue":"2","key":"5_CR1","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1145\/334725.334728","volume":"XIX","author":"L. Asplund","year":"1999","unstructured":"L. Asplund and B. Johnson and K. Lundqvist. Session summary: The Ravenscar profile and implementation issues. Ada Letters, XIX(2):12\u201314, 1999.","journal-title":"Ada Letters"},{"key":"5_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"322","DOI":"10.1007\/BFb0032042","volume-title":"ICALP 1990","author":"R. Alur","year":"1990","unstructured":"R. Alur and D. Dill. Automata for modeling real-time systems. In ICALP 1990, volume 443 of LNCS, pages 322\u2013335. Springer-Verlag, 1990."},{"key":"5_CR3","unstructured":"J.G.P. Barnes. High Integrity Ada: The Spark Approach. Addison-Wesley, 1997."},{"issue":"4","key":"5_CR4","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1145\/584417.584432","volume":"XXII","author":"B. Brosgol","year":"2002","unstructured":"B. Brosgol. Session summary: Future of the Ada language and language changes such as the Ravenscar profile. Ada Letters, XXII(4):113\u2013119, 2002.","journal-title":"Ada Letters"},{"issue":"2","key":"5_CR5","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1023\/A:1021758401878","volume":"24","author":"A. Burns","year":"2003","unstructured":"A. Burns. How to verify a safe real-time system: The application of model checking and timed automata to the production cell case study. Real-Time Systems, 24(2):135\u2013151, 2003.","journal-title":"Real-Time Systems"},{"key":"5_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1007\/BFb0055011","volume-title":"Ada-Europe 98","author":"A. Burns","year":"1998","unstructured":"A. Burns, B. Dobbing, and G. Romanski. The Ravenscar tasking profile for high integrity real-time programs. In Ada-Europe 98, volume 1411 of LNCS, pages 263\u2013275. Springer-Verlag, 1998."},{"key":"5_CR7","doi-asserted-by":"crossref","unstructured":"A. Burns, B. Dobbing, and T. Vardanega. Guide for the use of the Ada Ravenscar profile in high integrity systems. Technical Report YCS 348, Department of Computer Science, The University of York, 2003.","DOI":"10.1145\/997119.997120"},{"issue":"2","key":"5_CR8","first-page":"104","volume":"146","author":"C.J. Fidge","year":"1999","unstructured":"C.J. Fidge, I.J. Hayes, and G. Watson. The deadline command. IEEE Software \u2014 Special Issue on Real-Time Systems, 146(2):104\u2013111, 1999.","journal-title":"IEEE Software \u2014 Special Issue on Real-Time Systems"},{"issue":"5","key":"5_CR9","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1109\/32.387469","volume":"21","author":"R. Gerber","year":"1995","unstructured":"R. Gerber and S. Hong. Compiling real-time programs with timing constraint refinement and structure code motion. IEEE Transactions on Software Engineering, 21(5):389\u2013404, May 1995.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"5_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"170","DOI":"10.1007\/3-540-45352-0_15","volume-title":"FTRTFT2000","author":"I.J. Hayes","year":"2000","unstructured":"I.J. Hayes. Real-time program refinement using auxiliary variables. In FTRTFT2000, volume 1926 of LNCS, pages 170\u2013184. Springer-Verlag, 2000."},{"key":"5_CR11","unstructured":"C.B. Jones. Development Methods for Computer Programs Including a Notion of Interference. PhD thesis, Programming Research Group, The University of Oxford, 1981."},{"key":"5_CR12","unstructured":"C.B. Jones. Interference resumed. Technical Report UMCS-91-5-1, Department of Computer Science, The University of Manchester, May 1991."},{"key":"5_CR13","series-title":"Lect Notes Comput Sci","first-page":"1","volume-title":"FME\u201993","author":"C.B. Jones","year":"1993","unstructured":"C.B. Jones. Reasoning about interference in an object-based design method. In FME\u201993, volume 670 of LNCS, pages 1\u201318. Springer-Verlag, 1993."},{"issue":"1+2","key":"5_CR14","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"K.G. Larsen","year":"1997","unstructured":"K.G. Larsen, P. Pettersson, and W. Yi. UPPAAL in a nutshell. Software Tools for Technology Transfer, 1(1+2):134\u2013152, 1997.","journal-title":"Software Tools for Technology Transfer"},{"key":"5_CR15","unstructured":"I. Lee and V. Gehlot. Language constructs for distributed real-time programming. In IEEE Real-Time Systems Symposium, pages 57\u201366. IEEE, 1985."},{"key":"5_CR16","unstructured":"A. Leung, K. Palem, and A. Pnueli. TimeC: A time constraint language for ILP processor compilation. In The 5th Australian Conference on Parallel and Real Time Systems, pages 57\u201371. Springer-Verlag, 1998."},{"key":"5_CR17","unstructured":"T.-M. Lin and A. Burns. Annotations for RavenSPARK. Technical report, Department of Computer Science, The University of York, 2002."},{"issue":"1","key":"5_CR18","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1023\/A:1021701221847","volume":"24","author":"K. Lundqvist","year":"2003","unstructured":"K. Lundqvist and L. Asplund. A Ravenscar-compliant run-time kernel for safetycritical systems. Real-Time Systems, 24(1):29\u201354, 2003.","journal-title":"Real-Time Systems"},{"key":"5_CR19","unstructured":"D. Naydich and D. Guaspari. Timing analysis by model checking. In LFM2000, pages 71\u201382, June 2000."},{"key":"5_CR20","unstructured":"Timing analysis for model checking (working document). Technical report, Odyssey Research Associates, June 2001."},{"key":"5_CR21","unstructured":"P. Pettersson. Modelling and Verification of Real-Time Systems Using Timed Automata: Theory and Practice. PhD thesis, Department of Computer Systems, Uppsala University, February 1999."},{"key":"5_CR22","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"369","DOI":"10.1007\/3-540-16042-6_21","volume-title":"FST & TCS 85","author":"E.W. Stark","year":"1985","unstructured":"E.W. Stark. A proof technique for rely\/guarantee properties. In FST & TCS 85, volume 206 of LNCS, pages 369\u2013391, New Dehli, 1985. Springer-Verlag."},{"key":"5_CR23","unstructured":"K. St\u00f8len. Development of Parallel Programs on Shared Data-Structures. PhD thesis, Department of Computer Science, The University of Manchester, 1990."},{"key":"5_CR24","series-title":"Lect Notes Comput Sci","volume-title":"Ada 95 Reference Manual: Language and Standard Libraries","year":"1997","unstructured":"S.T. Taft and R.A. Duff, editors. Ada 95 Reference Manual: Language and Standard Libraries, volume 1246 of LNCS. Springer-Verlag, 1997."},{"issue":"1","key":"5_CR25","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1145\/374369.374371","volume":"XXI","author":"A.J. Wellings","year":"2001","unstructured":"A.J. Wellings. Session summary: Status and future of the Ravenscar profile. Ada Letters, XXI(1): 5\u20138, 2001.","journal-title":"Ada Letters"},{"key":"5_CR26","doi-asserted-by":"crossref","unstructured":"P.J. Whysall and J.A. McDermid. Object oriented specification and refinement. In 4th Refinement Workshop, Workshops in Computing, pages 150\u2013184. Springer-Verlag, 1991.","DOI":"10.1007\/978-1-4471-3756-6_9"},{"key":"5_CR27","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"434","DOI":"10.1007\/3-540-50214-9_27","volume-title":"VDM\u201988","author":"J.C.P. Woodcock","year":"1988","unstructured":"J.C.P. Woodcock and B. Dickinson. Using VDM with rely and guarantee conditions: Experiences of a real project. In VDM\u201988, volume 328 of LNCS, pages 434\u2013458. Springer-Verlag, 1988."},{"issue":"2","key":"5_CR28","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/BF01211617","volume":"9","author":"Q. Xu","year":"1997","unstructured":"Q. Xu, W-P. Roever, and J. He. The rely-guarantee method for verifying shared variable concurrent programs. Formal Aspects of Computing, 9(2):149\u2013174, 1997.","journal-title":"Formal Aspects of Computing"}],"container-title":["Lecture Notes in Computer Science","Reliable Software Technologies \u2014 Ada-Europe 2003"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44947-7_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T16:37:28Z","timestamp":1556728648000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44947-7_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540403760","9783540449478"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/3-540-44947-7_5","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]}}}