{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:31:35Z","timestamp":1725492695881},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540660934"},{"type":"electronic","value":"9783540487531"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48753-0_2","type":"book-chapter","created":{"date-parts":[[2007,10,10]],"date-time":"2007-10-10T13:58:29Z","timestamp":1192024709000},"page":"12-25","source":"Crossref","is-referenced-by-count":6,"title":["A Formal Model of the Ada Ravenscar Tasking Profile; Protected Objects"],"prefix":"10.1007","author":[{"given":"Kristina","family":"Lundqvist","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lars","family":"Asplund","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stephen","family":"Michell","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,6,11]]},"reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"R. Alur, and D. Dill, \u201cAutomata for Modeling Real-Time Systems\u201d, Proceedings of the 17th International Colloquium on Automata, Languages and Programming, vol. 443, Springer-Verlag, 1990.","DOI":"10.1007\/BFb0032042"},{"key":"2_CR2","unstructured":"J. Barnes, \u201cHigh Integrity Ada \u2014 The SPARK Approach\u201d, Addison Wesley, ISBN 0-201-17517-7, 1997."},{"key":"2_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/BFb0015510","volume-title":"proc. Ada Europe","author":"L. Bj\u00f6rnfot","year":"1995","unstructured":"L. Bj\u00f6rnfot, \u201cAda and Timed Automata\u201d, In proc. Ada Europe, Frankfurt, Germany, LNCS 1031, pp. 389\u2013405, Springer-Verlag, Oct 1995."},{"key":"2_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1007\/BFb0054990","volume-title":"Ada Europe","author":"P. Chapront","year":"1998","unstructured":"Pierre Chapront, \u201cAda+B The Formula for Safety Critical Software Development\u201d, Ada Europe, Uppsala, Sweden, LNCS 1411, pp. 14\u201318, Springer-Verlag, June 1998."},{"key":"2_CR5","unstructured":"J. Crow, S. Owre, J. Rushby, N. Shankar, and M. Srivas, \u201cA tutorial introduction to PVS\u201d, WIFT\u201995:Workshop on Industrial-Strength Formal Specification Techniques, Boca Raton, Florida, April 1995."},{"key":"2_CR6","doi-asserted-by":"crossref","unstructured":"B. Dobbing and A. Burns, \u201cThe Ravenscar Tasking Profile for High Integrity Real-Time Programs\u201d, SIGAda\u201998, Nov 8\u201312, 1998.","DOI":"10.1145\/289524.289525"},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"S. Fowler and A. Wellings, \u201cFormal Analysis of a Real-Time Kernel Specification\u201d, FTRTFT\u201996, 1996","DOI":"10.1007\/3-540-61648-9_55"},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"S. Fowler and A. Wellings, \u201cFormal Development of a Real-Time Kernel\u201d, 19th IEEE Real-Time Systems Symposium, Dec 1997.","DOI":"10.1109\/REAL.1997.641284"},{"issue":"9","key":"2_CR9","doi-asserted-by":"publisher","first-page":"1058","DOI":"10.1109\/32.58790","volume":"16","author":"D. Guaspari","year":"1990","unstructured":"David Guaspari, Carla Marceau, and Wolfgang Polak. Formal Verification of Ada Programs. IEEE Transactions on Software Engineering, vol. 16, no. 9, September 1990, pp. 1058\u20131075.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"2_CR10","unstructured":"ISO\/IEC PDTR 15942, Guidance on the Use of the Ada Programming Language in High Integrity Systems"},{"key":"2_CR11","unstructured":"J.E. Hopcroft and J.D. Ullman, \u201cIntroduction to Automata Theory, Languages and Computation\u201d, ISBN 0-201-02988-X, Addison-Wesley, 1979."},{"key":"2_CR12","unstructured":"A. Hutcheon, \u201cSafe Nucleus Formal Specification\u201d, Project Reference CI\/GNSR\/27: The Design and Development of Safety Kernel, Aug 1994."},{"key":"2_CR13","unstructured":"To be published in Ada letters, spring 1999."},{"issue":"9","key":"2_CR14","doi-asserted-by":"crossref","first-page":"890","DOI":"10.1109\/TSE.1986.6313045","volume":"12","author":"F. Jahanian","year":"1986","unstructured":"F. Jahanian and A. K. Mok, \u201cSafety analysis of timing properties in real-time systems\u201d, IEEE Transactions on Software Engineering, 12(9):890\u2013904, Sept. 1986.","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"number 1","key":"2_CR15","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, \u201cUppaal in a Nutshell\u201d, Int. Journal on Software Tools for Technology Transfer, Springer-Verlag, vol 1, number 1\u20132, pp. 134\u2013152, Oct 1997.","journal-title":"Int. Journal on Software Tools for Technology Transfer"},{"key":"2_CR16","unstructured":"M.K. Smith, The AVA Reference Manual: Derived from ANSI\/MIL-STD-1815A-1983, Computational Logic Inc., Feb. 1992"},{"key":"2_CR17","unstructured":"R.M. Tol, \u201cFormal Design of a Real-Time Operating System Kernel\u201d, Ph.D. thesis, University of Groningen, 1995."},{"key":"2_CR18","unstructured":"A. Wellings and A. Burns, \u201cWorkshop Report\u201d, The Eighth International Real-Time Ada Workshop (IRTAW8), Ada User Journal, vol 18, number 2, June 1997."}],"container-title":["Lecture Notes in Computer Science","Reliable Software Technologies \u2014 Ada-Europe\u2019 99"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48753-0_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,3]],"date-time":"2019-05-03T17:59:16Z","timestamp":1556906356000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48753-0_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540660934","9783540487531"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-48753-0_2","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}