{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:18:38Z","timestamp":1725664718968},"publisher-location":"Berlin, Heidelberg","reference-count":34,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540609735"},{"type":"electronic","value":"9783540497493"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-60973-3_114","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T16:09:04Z","timestamp":1330272544000},"page":"682-701","source":"Crossref","is-referenced-by-count":3,"title":["Procedure-level verification of real-time concurrent systems"],"prefix":"10.1007","author":[{"given":"Farn","family":"Wang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Chia-Tien","family":"Lo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,1]]},"reference":[{"key":"38_CR1","doi-asserted-by":"crossref","unstructured":"R. Alur, C. Courcoubetis, D.L. Dill. Model Checking for Real-Time Systems, IEEE LICS, 1990.","DOI":"10.1109\/LICS.1990.113766"},{"key":"38_CR2","unstructured":"R. Alur, T.A. Henzinger, P.-H. Ho. Automatic Symbolic Verification of Embedded Systems, in Proceedings of 1993 IEEE Real-Time System Symposium."},{"key":"38_CR3","unstructured":"A.V. Aho, R. Sethi, J.D. Ullman, Compilers \u2014 Principles, Techniques, and Tools, pp. 393\u2013396, Addison-Wesley Publishing Company, 1986."},{"key":"38_CR4","unstructured":"J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, L.J. Hwang. Symbolic Model Checking: 1020 States and Beyond, IEEE LICS, 1990."},{"key":"38_CR5","doi-asserted-by":"crossref","unstructured":"B. Berthomieu, M. Diaz. Modeling and Verification of Time Dependent Systems Using Time Petri Nets. IEEE TSE, Vol. 17, No.3, March 1991.","DOI":"10.1109\/32.75415"},{"key":"38_CR6","unstructured":"Boyer, Moore. A Computational Logic Handbook, Academic Press, 1988."},{"key":"38_CR7","doi-asserted-by":"crossref","unstructured":"D. Bosscher, I. Polak, F. Vaandrager. Verification of an Audio Control Protocol. Proceedings of Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, 1994; in LNCS, Springer-Verlag.","DOI":"10.1007\/3-540-58468-4_165"},{"key":"38_CR8","doi-asserted-by":"crossref","unstructured":"R.E. Bryant. Graph-based Algorithms for Boolean Function Manipulation, IEEE Trans. Comput., C-35(8), 1986.","DOI":"10.1109\/TC.1986.1676819"},{"key":"38_CR9","unstructured":"E. Clarke and E.A. Emerson. Design and Synthesis of Synchronization Skeletons using Branching-Time Temporal Logic, Proceedings of Workshop on Logic of Programs, Lecture Notes in Computer Science 131, Springer-Verlag, 1981."},{"issue":"2","key":"38_CR10","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E. Clarke","year":"1986","unstructured":"E. Clarke, E.A. Emerson, and A.P. Sistla. Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications, ACM Transactions on Programming Languages and Systems 8(2), 1986, pp. 244\u2013263.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"38_CR11","unstructured":"H.M. Deitel. An Introduction to Operating Systems, pp.110\u2013115, Addison-Wesley, 1984."},{"key":"38_CR12","first-page":"275","volume-title":"Science of Computer Programming 8","author":"E. A. Emerson","year":"1987","unstructured":"E.A. Emerson, C.-L. Lei. Modalities for Model Checking: Branching Time Logic Strikes Back, Science of Computer Programming 8 (1987), pp.275\u2013306, Elsevier Science Publishers B.V. (North-Holland)."},{"key":"38_CR13","doi-asserted-by":"crossref","unstructured":"M.J.C. Gordon. HOL \u2014 A Proof Generating System for Higher-Order Logic. Cambridge University, Computer Laboratory, 1987.","DOI":"10.1007\/978-1-4613-2007-4_3"},{"key":"38_CR14","doi-asserted-by":"crossref","unstructured":"T.A. Henzinger, X. Nicollin, J. Sifakis, S. Yovine. Symbolic Model Checking for Real-Time Systems, IEEE LICS 1992.","DOI":"10.1109\/LICS.1992.185551"},{"key":"38_CR15","doi-asserted-by":"crossref","unstructured":"C.A.R. Hoare. Communicating Sequential Processes, Prentice Hall, 1985.","DOI":"10.1007\/978-3-642-82921-5_4"},{"key":"38_CR16","doi-asserted-by":"crossref","unstructured":"E. Horowitz. Fundamentals of Programming Languages, Computer Science Press, 1984.","DOI":"10.1007\/978-3-642-69406-6"},{"key":"38_CR17","unstructured":"J.E. Hopcroft, J.D. Ullman. Introduction to Automata Theory, Languages, and Computation, Addison-Wesley, 1979."},{"key":"38_CR18","unstructured":"C.B. Jones. Systematic Software Development using VDM, 2nd ed., Prentice Hall, 1990."},{"issue":"No9","key":"38_CR19","doi-asserted-by":"crossref","first-page":"890","DOI":"10.1109\/TSE.1986.6313045","volume":"SE-12","author":"F. Jahanian","year":"1986","unstructured":"F. Jahanian and A.K. Mok. Safety analysis of timing properties in real-time systems, IEEE Transactions on Software Engineering, Vol.SE-12, No9, 1986, pp. 890\u2013904.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"38_CR20","unstructured":"F. Jahanian, D.A. Stuart. A Method for Verifying Properties of Modechart Specifications. IEEE RTSS 1988."},{"key":"38_CR21","doi-asserted-by":"crossref","unstructured":"Y. Kesten, A. Pnueli, J. Sifakis, S. Yovine. Integration Graphs: a Class of Decidable Hybrid Systems. In Proc. Workshop on Theory of Hybrid Systems, LNCS 736, Springer-Verlag, 1993.","DOI":"10.1007\/3-540-57318-6_29"},{"key":"38_CR22","unstructured":"H.R. Lewis. Unsolvable Classes of Quantificational Formulus, 1979, Addison-Wesley Pub. Co."},{"key":"38_CR23","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K. L. McMillan","year":"1993","unstructured":"K.L. McMillan, \u201cSymbolic Model Checking\u201d, Kluwer Academic Publishers, Boston, MA, 1993."},{"key":"38_CR24","doi-asserted-by":"crossref","unstructured":"P. Merlin, D.J. Faber. Recoverability of Communication Protocols. IEEE Trans. Commun, Vol. COM-24, no. 9, Sept. 1976.","DOI":"10.1109\/TCOM.1976.1093424"},{"key":"38_CR25","unstructured":"R. Milner. Communication and Concurrency. Prentice Hall, 1989."},{"key":"38_CR26","doi-asserted-by":"crossref","unstructured":"O. Maler, Z. Manna, A. Pnueli. From Timed to Hybrid Systems. In Real Time: Theory in Practice, LNCS 600, pp. 447\u2013484, Springer-Verlag, 1991.","DOI":"10.1007\/BFb0032003"},{"key":"38_CR27","doi-asserted-by":"crossref","unstructured":"Z. Manna, A. Pnueli. Verifying Hybrid Systems. In Proc. Workshop on Theory of Hybrid Systems, LNCS 736, Springer-Verlag, 1993.","DOI":"10.1007\/3-540-57318-6_22"},{"key":"38_CR28","unstructured":"R.S. Pressman. Software Engineering, A Practitioner's Approach. McGraw-Hill, 1982."},{"key":"38_CR29","unstructured":"K. Slind. HOL90 Users Manual. Technical report, 1992."},{"key":"38_CR30","unstructured":"J.M. Spivey. The Z Notation, A Reference Manual, second edition. Prentice Hall, 1992."},{"issue":"No.4","key":"38_CR31","doi-asserted-by":"crossref","first-page":"346","DOI":"10.1145\/158431.158434","volume":"2","author":"F. Wang","year":"1993","unstructured":"F. Wang, A.K. Mok, E.A. Emerson. Real-Time Distributed System Specification and Verification in APTL. ACM TOSEM, Vol. 2, No. 4, October 1993, pp. 346\u2013378.","journal-title":"ACM TOSEM"},{"key":"38_CR32","unstructured":"F. Wang. Timing Behavior Analysis for Real-Time Systems. IEEE LICS 1995."},{"key":"38_CR33","doi-asserted-by":"crossref","unstructured":"F. Wang. Reachability Analysis at Procedure Level through Timing Coincidence, in Proceedings of the 6th CONCUR, Philadelphia, USA, August 1995, LNCS 962.","DOI":"10.1007\/3-540-60218-6_21"},{"key":"38_CR34","volume-title":"Fundamentals of Computer Science","author":"W. Wulf","year":"1981","unstructured":"W. Wulf, M. Shaw, P. Hilfinger, L. Flon. Fundamentals of Computer Science, Addison-Wesley, Reading, Mass., 1981."}],"container-title":["Lecture Notes in Computer Science","FME'96: Industrial Benefit and Advances in Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-60973-3_114.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,31]],"date-time":"2021-12-31T05:13:54Z","timestamp":1640927634000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-60973-3_114"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540609735","9783540497493"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/3-540-60973-3_114","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}