{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T05:39:18Z","timestamp":1737005958574,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540660101"},{"type":"electronic","value":"9783540487784"}],"license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48778-6_19","type":"book-chapter","created":{"date-parts":[[2007,5,1]],"date-time":"2007-05-01T10:18:07Z","timestamp":1178014687000},"page":"315-333","source":"Crossref","is-referenced-by-count":1,"title":["Proof Assistance for Real-Time Systems Using an Interactive Theorem Prover"],"prefix":"10.1007","author":[{"given":"Paul Z.","family":"Kolano","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[1999,4,30]]},"reference":[{"key":"19_CR1","doi-asserted-by":"crossref","unstructured":"Alborghetti, A., A. Gargantini, and A. Morzenti. Providing automated support to deductive analysis of time critical systems. Proc. 6th European Software Engineering Conf., 1997.","DOI":"10.1145\/267896.267912"},{"key":"19_CR2","doi-asserted-by":"crossref","unstructured":"Archer, M. and C. Heitmeyer. Mechanical verification of timed automata: a case study. Proc. Real-Time Technology and Applications Symp., pp. 192\u2013203, 1996.","DOI":"10.1109\/RTTAS.1996.509536"},{"key":"19_CR3","unstructured":"Bun, L. Checking properties of ASTRAL specifications with PVS. Proc. 2nd Annual Conf. of the Advanced School for Computing and Imaging, pp. 102\u2013107, 1996."},{"key":"19_CR4","unstructured":"Bun, L. Embedding Astral in PVS. Proc. 3rd Annual Conf. of the Advanced School for Computing and Imaging, pp. 130\u2013136, 1997."},{"issue":"9","key":"19_CR5","doi-asserted-by":"publisher","first-page":"572","DOI":"10.1109\/32.629494","volume":"23","author":"A. Coen-Porisini","year":"1997","unstructured":"Coen-Porisini, A., C. Ghezzi, and R.A. Kemmerer. Specification of realtime systems using ASTRAL. IEEE Transactions on Software Engineering, 23(9): 572\u2013598, 1997.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"19_CR6","doi-asserted-by":"crossref","unstructured":"Coen-Porisini, A., R.A. Kemmerer, and D. Mandrioli. A formal framework for ASTRAL inter-level proof obligations. Proc. 5th European Software Engineering Conf., pp. 90\u2013108, 1995.","DOI":"10.1007\/3-540-60406-5_9"},{"issue":"8","key":"19_CR7","doi-asserted-by":"publisher","first-page":"548","DOI":"10.1109\/32.310665","volume":"20","author":"A. Coen-Porisini","year":"1994","unstructured":"Coen-Porisini, A., R.A. Kemmerer, and D. Mandrioli. A formal framework for ASTRAL intralevel proof obligations. IEEE Transactions on Software Engineering, 20(8): 548\u2013561, 1994.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"19_CR8","unstructured":"Crow, J., S. Owre, J. Rushby, N. Shankar, and M. Srivas. A tutorial introduction to PVS. Workshop on Industrial-Strength Formal Specification Techniques, 1995."},{"key":"19_CR9","doi-asserted-by":"crossref","unstructured":"Ghezzi, C. and R.A. Kemmerer. ASTRAL: an assertion language for specifying realtime systems. Proc. 3rd European Software Engineering Conf., pp. 122\u2013140, 1991.","DOI":"10.1007\/3540547428_46"},{"key":"19_CR10","doi-asserted-by":"crossref","unstructured":"Ghezzi, C. and R.A. Kemmerer. Executing formal specifications: the ASTRAL to TRIO translation approach. Proc. Symp. on Testing, Analysis, and Verification, 1991.","DOI":"10.1145\/120807.120817"},{"key":"19_CR11","unstructured":"Gordon, M. Notes on PVS from a HOL perspective. Available at <http:\/\/www.cl.cam.ac.uk\/users\/mjcg\/PVS.html>, 1995."},{"key":"19_CR12","unstructured":"Gordon, M.J.C. and T.F. Melham (eds.). Introduction to HOL: a theorem proving environment for higher order logic. Cambridge University Press, 1993."},{"issue":"1\u20132","key":"19_CR13","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/BF01383987","volume":"3","author":"R. Hale","year":"1993","unstructured":"Hale, R., R. Cardell-Oliver, and J. Herbert. An embedding of timed transition systems in HOL. Formal Methods in System Design, 3(1\u20132): 151\u2013174, 1993.","journal-title":"Formal Methods in System Design"},{"key":"19_CR14","unstructured":"Heitmeyer, C. and D. Mandrioli (eds.). Formal methods for real-time computing. John Wiley, 1996."},{"key":"19_CR15","doi-asserted-by":"crossref","unstructured":"Kaufmann, M. and J. Strother Moore. ACL2: an industrial strength version of Nqthm. Proc. 11th Annual Conf. on Computer Assurance, pp. 23\u201334, 1996.","DOI":"10.1109\/CMPASS.1996.507872"},{"key":"19_CR16","volume-title":"Tools and techniques for the design and systematic analysis of real-time systems","author":"P.Z. Kolano","year":"1999","unstructured":"Kolano, P.Z. Tools and techniques for the design and systematic analysis of real-time systems. Ph.D. Thesis, University of California, Santa Barbara, 1999."},{"issue":"1\/4","key":"19_CR17","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1023\/A:1018934104631","volume":"7","author":"Paul Z. Kolano","year":"1999","unstructured":"Kolano, P.Z., Z. Dang, and R.A. Kemmerer. The design and analysis of real-time systems using the ASTRAL software development environment. Annals of Software Engineering, 7, 1999.","journal-title":"Annals of Software Engineering"},{"key":"19_CR18","doi-asserted-by":"crossref","unstructured":"Skakkebaek, J.U. and N. Shankar. Towards a duration calculus proof assistant in PVS. 3rd Int. Symp. on Formal Techniques in Real-Time and Fault-Tolerant Systems, pp. 660\u2013679, 1994.","DOI":"10.1007\/3-540-58468-4_189"},{"issue":"5","key":"19_CR19","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1109\/52.57889","volume":"7","author":"J.M. Spivey","year":"1990","unstructured":"Spivey, J.M. Specifying a real-time kernel. IEEE Software, 7(5): 21\u201328, 1990.","journal-title":"IEEE Software"},{"key":"19_CR20","doi-asserted-by":"crossref","unstructured":"Young, W.D. Comparing verification systems: interactive consistency in ACL2. Proc. 11th Annual Conf. on Computer Assurance, pp. 35\u201345, 1996.","DOI":"10.1109\/CMPASS.1996.507873"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Real-Time and Probabilistic Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48778-6_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T00:07:34Z","timestamp":1736986054000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48778-6_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540660101","9783540487784"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/3-540-48778-6_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1999]]}}}