{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:14:07Z","timestamp":1725484447216},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540000297"},{"type":"electronic","value":"9783540361039"}],"license":[{"start":{"date-parts":[[2002,1,1]],"date-time":"2002-01-01T00:00:00Z","timestamp":1009843200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-36103-0_30","type":"book-chapter","created":{"date-parts":[[2007,5,15]],"date-time":"2007-05-15T23:15:07Z","timestamp":1179270907000},"page":"275-286","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Formal Analysis of Real-Time Systems with SAM"],"prefix":"10.1007","author":[{"given":"Huiqun","family":"Yu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xudong","family":"He","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yi","family":"Deng","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lian","family":"Mo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,10,10]]},"reference":[{"issue":"3","key":"30_CR1","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1109\/32.75415","volume":"17","author":"B. Berthomieu","year":"1991","unstructured":"B. Berthomieu and M. Diaz. Modeling and verification of time dependent systems using Time Petri nets. IEEE Transactions on Software Engineering, 17(3):259\u2013273, 1991.","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"5","key":"30_CR2","doi-asserted-by":"publisher","first-page":"603","DOI":"10.1109\/TSE.1983.235261","volume":"9","author":"J.E. Coolahan Jr.","year":"1983","unstructured":"J.E. Coolahan, Jr. and N. Roussopoulos. Timing requirements for time-driven systems using augmented Petri nets. IEEE Transactions on Software Engineering, 9(5):603\u2013616, 1983.","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"12","key":"30_CR3","doi-asserted-by":"publisher","first-page":"1104","DOI":"10.1016\/S0140-3664(99)00240-6","volume":"23","author":"J.P. Courtiat","year":"2000","unstructured":"J.P. Courtiat, C.A.S. Santos, C. Lohr, and B. Outtaj. Experience with RT-LOTOS, a temporal extension of the LOTOS formal description technique. Computer Communications, 23(12):1104\u20131123, 2000.","journal-title":"Computer Communications"},{"issue":"4","key":"30_CR4","doi-asserted-by":"publisher","first-page":"626","DOI":"10.1145\/242223.242257","volume":"28","author":"E.M. Clarke","year":"1996","unstructured":"E.M. Clarke and J.M. Wing. Formal methods: state of the art and future directions. ACM Computing Surveys, 28(4):626\u2013643, 1996.","journal-title":"ACM Computing Surveys"},{"key":"30_CR5","doi-asserted-by":"crossref","unstructured":"E.A. Emerson. Temporal and modal logic. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, chapter 16. Elsevier Science Publisher B.V., 1990.","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"issue":"1","key":"30_CR6","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1093\/comjnl\/45.1.111","volume":"45","author":"X. He","year":"2002","unstructured":"X. He and Y. Deng. A framework for developing and analyzing software architecture specifications in SAM. The Computer Journal, 45(1):111\u2013128, 2002.","journal-title":"The Computer Journal"},{"issue":"3","key":"30_CR7","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1109\/TSE.1987.233170","volume":"13","author":"N.G. Leveson","year":"1987","unstructured":"N.G. Leveson and J.L. Stolzy. Safety analysis using Petri nets. IEEE Transactions on Software Engineering, 13(3):386\u2013397, 1987.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"30_CR8","doi-asserted-by":"crossref","unstructured":"Z. Manna, A. Anuchitanukul, N. Bj\u00f8rner, A. Browne, E. Chang, M. Col\u00f3n, L. de Alaro, H. Devarajan, H. Sipma, and M. Uribe. STeP: the Stanford Temporal Prover. Technical Report STAN-CS-TR-94-1518, Department of Computer Science, Stanford University, June 1994.","DOI":"10.21236\/ADA324036"},{"issue":"9","key":"30_CR9","doi-asserted-by":"publisher","first-page":"1036","DOI":"10.1109\/TCOM.1976.1093424","volume":"COM-24","author":"P. Merlin","year":"1976","unstructured":"P. Merlin and D.J. Faber. Recoverability of communication protocols. IEEE Transactions on Communications, COM-24(9):1036\u20131043, 1976.","journal-title":"IEEE Transactions on Communications"},{"key":"30_CR10","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, 1992.","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"30_CR11","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, 1995.","DOI":"10.1007\/978-1-4612-4222-2"},{"key":"30_CR12","unstructured":"Z. Manna and A. Pnueli. Clocked transition systems. Technical Report STAN-CS-TR-96-1566, Computer Science Department, Stanford University, 1996."},{"issue":"4","key":"30_CR13","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1109\/5.24143","volume":"77","author":"T. Murata","year":"1989","unstructured":"T. Murata. Petri nets properties, analysis and applications. Proceedings of the IEEE, 77(4):27\u201360, 1989.","journal-title":"Proceedings of the IEEE"},{"key":"30_CR14","doi-asserted-by":"crossref","unstructured":"A. Pnueli. The temporal logic of programs. In 18th Ann. IEEE Symp. on Foundations of Computer Science, pages 46\u201357, 1977.","DOI":"10.1109\/SFCS.1977.32"},{"key":"30_CR15","unstructured":"W3C Recommendation. Synchronized Multimedia Integration Language (SMIL) 1.0 Specification. \n                    http:\/\/www.w3.org\/TR\/REC-smil\n                    \n                  , 1998."},{"key":"30_CR16","doi-asserted-by":"crossref","unstructured":"P.N.M. Sampaio and J.P. Courtiat. A formal approach for the presentation of interactive multimedia documents. In Proceedings Proceedings of the 7th ACM International Conference on Multimedia (Part 1), pages 435\u2013438, 2000.","DOI":"10.1145\/354384.376346"},{"key":"30_CR17","unstructured":"M. Trompedeller. A Classification of Petri Nets. \n                    http:\/\/www.daimi.dk\/PetriNets\/classification\n                    \n                  , 1995."},{"key":"30_CR18","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1016\/S0950-5849(99)00009-9","volume":"41","author":"J. Wang","year":"1999","unstructured":"J. Wang, X. He, and Y. Deng. Introducing software architecture specification and analysis in SAM through an example. Information and Software Technology, 41:451\u2013467, 1999.","journal-title":"Information and Software Technology"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36103-0_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T09:18:02Z","timestamp":1558257482000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36103-0_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540000297","9783540361039"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-36103-0_30","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]},"assertion":[{"value":"10 October 2002","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}