{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,15]],"date-time":"2025-08-15T01:23:09Z","timestamp":1755220989425,"version":"3.43.0"},"reference-count":41,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Real-Time Systems"],"published-print":{"date-parts":[[1999,1]]},"DOI":"10.1023\/a:1008008003332","type":"journal-article","created":{"date-parts":[[2002,12,22]],"date-time":"2002-12-22T07:45:23Z","timestamp":1040543123000},"page":"81-114","source":"Crossref","is-referenced-by-count":8,"title":["Procedure-Level Verification of Real-time Concurrent Systems"],"prefix":"10.1007","volume":"16","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","reference":[{"key":"190965_CR1","unstructured":"Alur, R., Courcoubetis, C., and Dill, D. L. 1990. Model checking for real-time systems. IEEE LICS."},{"key":"190965_CR2","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1145\/174644.174651","volume":"41","author":"R. Alur","year":"1994","unstructured":"Alur, R., and Henzinger, T. A. 1994. A really temporal logic. Journal of ACM 41: 181\u2013204","journal-title":"Journal of ACM"},{"key":"190965_CR3","unstructured":"Alur, R., Henzinger, T. A., and Ho, P.-H. 1993. Automatic symbolic cerification of embedded systems. Proceedings of 1993 IEEE Real-Time System Symposium."},{"key":"190965_CR4","unstructured":"Abdulla, P. A., and Jonsson, B. 1993. Verifying programs with unreliable channels. 8th IEEE International Symposium on Logic in Computer Science."},{"key":"190965_CR5","unstructured":"Aho, A. V., Sethi, R., and Ullman, J. D. 1986. Compliers-Principles, Techniques, and Tools, pp. 393\u2013396. Addison-Wesley Publishing Company"},{"key":"190965_CR6","unstructured":"Burch, J. R., Clarke, E. M., McMillan, K. L., Dill, D. L., and Hwang, L. J. 1990. Symbolic model checking: 1020 states and beyond. IEEE LICS."},{"key":"190965_CR7","doi-asserted-by":"crossref","unstructured":"Berthomieu, B., and Diaz, M. 1991. Modeling and verification of time dependent systems Using time Petri nets. IEEE TSE 17(3).","DOI":"10.1109\/32.75415"},{"key":"190965_CR8","unstructured":"Boyer, R., and Moore, S. 1988. A Computational Logic Handbook. Academic Press."},{"key":"190965_CR9","volume-title":"Proceedings of Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"D. Bosscher","year":"1994","unstructured":"Bosscher, D., Polak, I., and Vaandrager, F. 1994. Verification of an audio control protocol. Proceedings of Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems. LNCS, Springer-Verlag."},{"key":"190965_CR10","doi-asserted-by":"crossref","unstructured":"Bryant, R. E. 1986. Graph-based algorithms for Boolean function manipulation. IEEE Trans.Comput. C-35(8).","DOI":"10.1109\/TC.1986.1676819"},{"key":"190965_CR11","unstructured":"Clarke, E., and Emerson, E. A. 1981. Design and synthesis of synchronization skeletons using branchingtime temporal logic.Proceedings of Workshop on Logic of Programs, Lecture Notes in Computer Science 131, Springer-Verlag."},{"issue":"2","key":"190965_CR12","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E. Clarke","year":"1986","unstructured":"Clarke, E., Emerson, E. A., and Sistla, A. P. 1986. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems 8(2): 244\u2013263.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"190965_CR13","doi-asserted-by":"crossref","unstructured":"Chandy, K. M., and Misra, J. 1988. Parallel Program Design: A Foundation. Addison-Wesley.","DOI":"10.1007\/978-1-4613-9668-0_6"},{"key":"190965_CR14","unstructured":"Deitel, H. M. 1984. An Introduction to Operating Systems, pp. 110\u2013115. Addison-Wesley"},{"key":"190965_CR15","first-page":"275","volume-title":"Science of Computer Programming 8","author":"E. A. Emerson","year":"1997","unstructured":"Emerson, E. A., and Lei, C.-L. 1997. Modalities for model checking: Branching time logic strikes back. Science of Computer Programming 8, pp.275\u2013306. Science Publishers B.V. (North-Holland)."},{"key":"190965_CR16","volume-title":"HOL-A Proof Generating System for Higher-Order Logic","author":"M. J. C. Gordon","year":"1987","unstructured":"Gordon, M. J. C. HOL-A Proof Generating System for Higher-Order Logic. Computer Laboratory, Cambridge University, 1987."},{"key":"190965_CR17","doi-asserted-by":"crossref","unstructured":"Hong, S., and Gerber, R. June 1993. Compiling real-time programs into schedulable code. ACM SIGPLAN'93 Conference on Programming Language Design and Implementation; ACM SIGPLAN Notices, 28(6).","DOI":"10.1145\/173262.155106"},{"key":"190965_CR18","unstructured":"Henzinger, T. A., Nicollin, X., Sifakis, J., and Yovine, S. 1992. Symbolic model checking for real-time systems. IEEE LICS."},{"key":"190965_CR19","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C. A. R. Hoare","year":"1969","unstructured":"Hoare, C. A. R. 1969. An axiomatic basis of computer programming. Comm.ACM 12: 576\u2013583.","journal-title":"Comm. ACM"},{"key":"190965_CR20","doi-asserted-by":"crossref","unstructured":"Hoare, C. A. R. 1985. Communicating Sequential Processes. Prentice Hall.","DOI":"10.1007\/978-3-642-82921-5_4"},{"key":"190965_CR21","doi-asserted-by":"crossref","unstructured":"Horowitz, E. 1984. Fundamentals of Programming Languages. Computer Science Press.","DOI":"10.1007\/978-3-642-69406-6"},{"key":"190965_CR22","unstructured":"Hopcroft, J. E., and Ullman, J. D. 1979. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley."},{"issue":"9","key":"190965_CR23","doi-asserted-by":"crossref","first-page":"890","DOI":"10.1109\/TSE.1986.6313045","volume":"12","author":"F. Jahanian","year":"1986","unstructured":"Jahanian, F., and Mok, A. K. 1986. Safety analysis of timing properties in real-time systems. IEEE Transactions on Software Engineering SE-12(9): 890\u2013904.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"190965_CR24","unstructured":"Jahanian, F., and Stuart, D. A. 1988. A method for verifying properties of Modechart specifications. IEEE RTSS."},{"key":"190965_CR25","unstructured":"Jones, C. B. 1990. Systematic Software Development using VDM, 2nd ed. Prentice Hall."},{"key":"190965_CR26","doi-asserted-by":"crossref","unstructured":"Kesten, Y., Pnueli, A., Sifakis, J., and Yovine, S. 1993. Integration graphs: A class of decidable hybrid systems. Proc.Workshop on Theory of Hybrid Systems, LNCS 736. Springer-Verlag.","DOI":"10.1007\/3-540-57318-6_29"},{"key":"190965_CR27","unstructured":"Lewis, H. R. 1979. Unsolvable Classes of Quantificational Formulus. Addison-Wesley Pub. Co."},{"key":"190965_CR28","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K. L. McMillan","year":"1993","unstructured":"McMillan, K. L. 1993. Symbolic Model Checking. Boston, MA: Kluwer Academic Publishers."},{"key":"190965_CR29","doi-asserted-by":"crossref","unstructured":"Merlin, P., and Faber, D. J. Sept. 1976. Recoverability of communication protocols. IEEE Trans.Commun COM-24(9).","DOI":"10.1109\/TCOM.1976.1093424"},{"key":"190965_CR30","unstructured":"Milner, R. 1989. Communication and Concurrency. Prentice Hall."},{"key":"190965_CR31","doi-asserted-by":"crossref","unstructured":"Maler, O., Manna, Z., and Pnueli, A. 1991. From timed to hybrid systems. In Real Time: Theory in Practice, LNCS 600, pp. 447\u2013484. Springer-Verlag.","DOI":"10.1007\/BFb0032003"},{"key":"190965_CR32","doi-asserted-by":"crossref","unstructured":"Manna, Z., and Pnueli, A. 1993. Verifying hybrid systems. Proc.Workshop on Theory of Hybrid Systems, LNCS 736. Springer-Verlag.","DOI":"10.1007\/3-540-57318-6_22"},{"key":"190965_CR33","unstructured":"Pressman, R. S. 1982. Software Engineering, A Practitioner's Approach. McGraw-Hill."},{"key":"190965_CR34","unstructured":"Slind, K. HOL90 Users Manual. Technical report, 1992."},{"key":"190965_CR35","unstructured":"Spivey, J. M. 1992. The Z Notation, A Reference Manual, second edition. Prentice Hall."},{"key":"190965_CR36","unstructured":"Satoh, I., and Tokoro, M. Semantics for a real-time object-oriented programming language. Proceedings of 1994 IEEE International Conference on Computer Languages."},{"issue":"4","key":"190965_CR37","doi-asserted-by":"crossref","first-page":"346","DOI":"10.1145\/158431.158434","volume":"2","author":"F. Wang","year":"1993","unstructured":"Wang, F., Mok, A. K., and Emerson, E. A. Octobor 1993. Real-time distributed system specification and verifi-cation in APTL. ACM TOSEM 2(4): 346\u2013378.","journal-title":"ACM TOSEM"},{"key":"190965_CR38","unstructured":"Wang, F. 1995. Timing behavior analysis for real-time systems. IEEE LICS."},{"key":"190965_CR39","doi-asserted-by":"crossref","unstructured":"Wang, F. August 1995. Reachability analysis at procedure level through timing coincidence. Proceedings of the 6th CONCUR. Philadelphia, LNCS 962.","DOI":"10.1007\/3-540-60218-6_21"},{"key":"190965_CR40","unstructured":"Wang, F. High-level execution time analysis. Proceedings of 1997 AMAST Real-Time Systems Workshop. Malleoca, Spain, LNCS 1231. Springer-Verlag. (An enhanced and more complete version is in IIS Technical Report: TR-IIS\u201397\u2013009."},{"key":"190965_CR41","volume-title":"Fundamentals of Computer Science","author":"W. Wulf","year":"1981","unstructured":"Wulf, W., Shaw, M., Hilfinger, P., and Flon, L. 1981. Fundamentals of Computer Science. Reading, Mass.: Addison-Wesley."}],"container-title":["Real-Time Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1008008003332.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1008008003332\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1008008003332.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,8]],"date-time":"2025-08-08T07:10:34Z","timestamp":1754637034000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1008008003332"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999,1]]},"references-count":41,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1999,1]]}},"alternative-id":["190965"],"URL":"https:\/\/doi.org\/10.1023\/a:1008008003332","relation":{},"ISSN":["0922-6443","1573-1383"],"issn-type":[{"type":"print","value":"0922-6443"},{"type":"electronic","value":"1573-1383"}],"subject":[],"published":{"date-parts":[[1999,1]]}}}