{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,10]],"date-time":"2026-02-10T19:53:54Z","timestamp":1770753234340,"version":"3.50.0"},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642389108","type":"print"},{"value":"9783642389115","type":"electronic"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-38911-5_2","type":"book-chapter","created":{"date-parts":[[2013,6,12]],"date-time":"2013-06-12T01:55:18Z","timestamp":1371002118000},"page":"19-35","source":"Crossref","is-referenced-by-count":7,"title":["Property Verification with MSC"],"prefix":"10.1007","author":[{"given":"Emmanuel","family":"Gaudin","sequence":"first","affiliation":[]},{"given":"Eric","family":"Brunel","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"2_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"E.M. Clarke","year":"1982","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol.\u00a0131, pp. 52\u201371. Springer, Heidelberg (1982)"},{"key":"2_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/3-540-11494-7_22","volume-title":"International Symposium on Programming","author":"J.P. Queille","year":"1982","unstructured":"Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol.\u00a0137, pp. 337\u2013351. Springer, Heidelberg (1982)"},{"key":"2_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/978-3-540-45236-2_8","volume-title":"FME 2003: Formal Methods","author":"D. Compare","year":"2003","unstructured":"Compare, D., Inverardi, P., Pelliccione, P., Sebastiani, A.: Integrating model-checking architectural analysis and validation in a real software life-cycle. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol.\u00a02805, pp. 114\u2013132. Springer, Heidelberg (2003)"},{"key":"2_CR4","unstructured":"Holzmann, G.J.: The SPIN Model Checker \u2013 Primer and Reference Manual. Addison Wesley (2003)"},{"key":"2_CR5","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J.: The logic of bugs. In: Proceedings of the 10th ACM SIGSOFT Symposium on Foundations of Software Engineering, SIGSOFT 2002\/FSE 2002, pp. 81\u201387. ACM (2002)","DOI":"10.1145\/587051.587064"},{"key":"2_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/11495628_3","volume-title":"Scenarios: Models, Transformations and Tools","author":"A. Muscholl","year":"2005","unstructured":"Muscholl, A., Peled, D.: Deciding Properties of Message Sequence Charts. In: Leue, S., Syst\u00e4, T.J. (eds.) Scenarios. LNCS, vol.\u00a03466, pp. 43\u201365. Springer, Heidelberg (2005)"},{"key":"2_CR7","unstructured":"Babica, J.: Message Sequence Charts properties and checking algorithms. Master Thesis at Masarykova Univerzita Fakulta Informatiky Brno (2009), http:\/\/scstudio.sourceforge.net\/files\/thesis_babica09.pdf"},{"key":"2_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"374","DOI":"10.1007\/978-3-540-27863-4_21","volume-title":"Integration of Software Specification Techniques for Applications in Engineering","author":"M. Brill","year":"2004","unstructured":"Brill, M., Damm, W., Klose, J., Westphal, B., Wittke, H.: Live Sequence Charts. In: Ehrig, H., Damm, W., Desel, J., Gro\u00dfe-Rhode, M., Reif, W., Schnieder, E., Westk\u00e4mper, E. (eds.) INT 2004. LNCS, vol.\u00a03147, pp. 374\u2013399. Springer, Heidelberg (2004)"},{"key":"2_CR9","unstructured":"Specification & Description Language - Real-Time (2006), http:\/\/www.sdl-rt.org\/"},{"key":"2_CR10","unstructured":"Internation Telecommuication Union: Recommendation Z.120 (02\/11) Message Sequence Chart (MSC), http:\/\/www.itu.int\/rec\/T-REC-Z.120"},{"issue":"3","key":"2_CR11","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/s10515-007-0012-6","volume":"14","author":"M. Autili","year":"2007","unstructured":"Autili, M., Inveradi, P., Pelliccione, P.: Graphical scenarios for specifying temporal properties: an automated approach. Automated Software Engineering\u00a014(3), 293\u2013340 (2007)","journal-title":"Automated Software Engineering"},{"key":"2_CR12","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in Property Specifications for Finite-State Verification. In: Proceedings of the 21st International Conference on Software Engineering, ICE 1999, pp. 411\u2013420. IEEE Computer Society (1999)","DOI":"10.1145\/302405.302672"},{"key":"2_CR13","unstructured":"PragmaDev Tracer, http:\/\/www.pragmadev.com\/product\/tracing.html"}],"container-title":["Lecture Notes in Computer Science","SDL 2013: Model-Driven Dependability Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-38911-5_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,7,28]],"date-time":"2020-07-28T06:53:48Z","timestamp":1595919228000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-38911-5_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642389108","9783642389115"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-38911-5_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}