{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:01:09Z","timestamp":1725663669277},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540551799"},{"type":"electronic","value":"9783540467632"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1992]]},"DOI":"10.1007\/3-540-55179-4_39","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T04:52:17Z","timestamp":1330231937000},"page":"421-431","source":"Crossref","is-referenced-by-count":0,"title":["Verifying properties of HMS machine specifications of real-time systems"],"prefix":"10.1007","author":[{"given":"A.","family":"Gabrielian","sequence":"first","affiliation":[]},{"given":"R.","family":"Iyer","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,29]]},"reference":[{"key":"39_CR1","doi-asserted-by":"crossref","unstructured":"Abadi, M., \u201cTemporal-logic theorem proving,\u201d Dissertation, Stanford Univ., 1987.","DOI":"10.21236\/ADA325959"},{"issue":"No.1","key":"39_CR2","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1145\/59287.62028","volume":"11","author":"B. Alpern","year":"1989","unstructured":"Alpern, B., and F.B. Schneider, \u201cVerifying temporal properties without temporal logic,\u201d ACM Transactions on Programming Languages and Systems, Vol. 11, No. 1, January 1989, pp. 147\u2013167.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"39_CR3","volume-title":"Formal Methods: Theory and Practice","author":"L. Da-Hai","year":"1988","unstructured":"Da-Hai, L., and T.S.E. Maibaum, \u201cDeveloping a high level specification formalism,\u201d in Formal Methods: Theory and Practice, P.N. Scharbach (Ed.), CRC Press, Boca Baton, FL, 1988."},{"key":"39_CR4","doi-asserted-by":"crossref","unstructured":"Fitting, M., First-Order Logic and Automated Theorem Proving, Springer-Verlag, 1990.","DOI":"10.1007\/978-1-4684-0357-2"},{"key":"39_CR5","doi-asserted-by":"crossref","unstructured":"Franklin, M.K., and A. Gabrielian, \u201cA transformational method for verifying safety properties in real-time systems,\u201d Proc. 10th Real-Time Systems Symposium, Santa Monica, CA, December 5\u20137, 1989, pp. 112\u2013123.","DOI":"10.1109\/REAL.1989.63562"},{"key":"39_CR6","volume-title":"Foundations of Real-Time Computing: Formal Specifications and Methods","author":"A. Gabrielian","year":"1991","unstructured":"Gabrielian, A., \u201cHMS machines: a unified framework for specification, verification and reasoning for real-time systems,\u201d Foundations of Real-Time Computing: Formal Specifications and Methods, A. van Tilborg (Ed.), Kluwer Academic Publishers, Norwell, Mass., 1991, to appear."},{"key":"39_CR7","doi-asserted-by":"crossref","unstructured":"Gabrielian, A., and M. K. Franklin, \u201cState-based specification of complex real-time systems,\u201d Proc. IEEE Real-Time Systems Symposium, 1988, pp. 2\u201311.","DOI":"10.1109\/REAL.1988.51095"},{"key":"39_CR8","doi-asserted-by":"crossref","unstructured":"Gabrielian, A., and M.K. Franklin, \u201cMulti-level specification and verification of real-time software,\u201d 12th Int. Conf. Software Engineering, March 26\u201330, 1990, Nice, France, pp. 52\u201362. Revised version in Communications of the ACM, May 1991, pp. 50\u201360.","DOI":"10.1109\/ICSE.1990.63603"},{"key":"39_CR9","volume-title":"The Unified Computation Laboratory, Inst. of Math. and its Applications","author":"A. Gabrielian","year":"1991","unstructured":"Gabrielian, A., and R. Iyer, \u201cIntegrating automata and temporal logic: a framework for specification of real-time systems and software,\u201d The Unified Computation Laboratory, Inst. of Math. and its Applications, Stirling, Scotland, Oxford University Press, 1991."},{"key":"39_CR10","doi-asserted-by":"crossref","unstructured":"Ghezzi, C., D. Madrioli, et al., \u201cA general way to put time in Petri nets,\u201d Proc. Fifth Int. Workshop on Software Specif. and Design, Pittsburgh, PA, May 1989, pp. 60\u201367.","DOI":"10.1145\/75199.75210"},{"key":"39_CR11","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Z. Manna, and A. Pneuli, \u201cTemporal proof methodologies for real-time systems,\u201d Proc. 18th Annual ACM Symposium on Principles of Programming Languages, 1991.","DOI":"10.1145\/99583.99629"},{"key":"39_CR12","doi-asserted-by":"crossref","unstructured":"Melliar-Smith, P.M., \u201cA graphical representation of interval logic,\u201d in Proc. Concurrency 88, LNCS 335, Springer-Verlag, 1988, pp. 106\u2013120.","DOI":"10.1007\/3-540-50403-6_36"},{"key":"39_CR13","doi-asserted-by":"crossref","unstructured":"Manna, Z., and Pnueli, A., \u201cThe anchored version of the temporal framework,\u201d Proc. Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, LNCS 354, Springer-Verlag, 1989, pp. 201\u2013284.","DOI":"10.1007\/BFb0013024"},{"key":"39_CR14","doi-asserted-by":"crossref","unstructured":"Pnueli, A., and E. Harel, \u201cApplications of temporal logic to the specification of real-time systems (extended abstract),\u201d Proc. Symp. Formal Techniques in Real-Time and Fault-Tolerant Systems, LNCS 331, Springer-Verlag, 1988, pp. 84\u201398.","DOI":"10.1007\/3-540-50302-1_4"},{"key":"39_CR15","doi-asserted-by":"crossref","unstructured":"Reisig, W., Petri Nets, Springer-Verlag, 1985.","DOI":"10.1007\/978-3-642-69968-9"},{"key":"39_CR16","first-page":"166","volume-title":"CCS, liveness, and local model checking in the linear time mucalculus","author":"C. Stirling","year":"1990","unstructured":"Stirling, C., and D. Walker, \u201cCCS, liveness, and local model checking in the linear time mucalculus,\u201d Proc. Automatic Verification Methods for Finite State Systems, Grenoble, 1989, LNCS 407, Springer-Verlag, 1990, pp. 166\u2013178."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-55179-4_39.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T15:58:01Z","timestamp":1605628681000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-55179-4_39"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992]]},"ISBN":["9783540551799","9783540467632"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-55179-4_39","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1992]]}}}