{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T13:29:07Z","timestamp":1742390947803},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540231356"},{"type":"electronic","value":"9783540278634"}],"license":[{"start":{"date-parts":[[2004,1,1]],"date-time":"2004-01-01T00:00:00Z","timestamp":1072915200000},"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":[[2004]]},"DOI":"10.1007\/978-3-540-27863-4_27","type":"book-chapter","created":{"date-parts":[[2010,9,16]],"date-time":"2010-09-16T12:51:50Z","timestamp":1284641510000},"page":"494-516","source":"Crossref","is-referenced-by-count":10,"title":["Formal Verification of LSCs in the Development Process"],"prefix":"10.1007","author":[{"given":"Matthias","family":"Brill","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ralf","family":"Buscherm\u00f6hle","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Werner","family":"Damm","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jochen","family":"Klose","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bernd","family":"Westphal","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hartmut","family":"Wittke","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"27_CR1","volume-title":"The Unified Software Development Process","author":"I. Jacobson","year":"1999","unstructured":"Jacobson, I., Booch, G., Rumbaugh, J.: The Unified Software Development Process. Addison-Wesley, Reading (1999)"},{"key":"27_CR2","volume-title":"Extreme Programming Explained","author":"K. Beck","year":"1999","unstructured":"Beck, K.: Extreme Programming Explained. Addison-Wesley, Reading (1999)"},{"key":"27_CR3","unstructured":"EStdIT, B.d.I.: V-Model, Development Standard for IT-Systems of the federal Republic of Germany (1997)"},{"key":"27_CR4","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1109\/32.54292","volume":"16","author":"D. Harel","year":"1990","unstructured":"Harel, D., Lachover, H., Naamad, A., Pnueli, A., Politi, M., Sherman, R., Shtull- Trauring, A., Trakhtenbrot, M.: STATEMATE: A working environment for the development of complex reactive systems. IEEE Transactions on Software Engineering\u00a016, 403\u2013414 (1990)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"27_CR5","doi-asserted-by":"crossref","unstructured":"OMG: 1.4-uml-01-09-67 (2001)","DOI":"10.1142\/S021849580100002X"},{"key":"27_CR6","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-19029-2","volume-title":"Come, Let\u2019s Play: Scenario-Based Programming Using LSCs and the Play-Engine","author":"D. Harel","year":"2003","unstructured":"Harel, D., Marelly, R.: Come, Let\u2019s Play: Scenario-Based Programming Using LSCs and the Play-Engine. Springer, Heidelberg (2003)"},{"key":"27_CR7","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1023\/A:1011279932612","volume":"19","author":"W. Damm","year":"2001","unstructured":"Damm, W., Harel, D.: LSCs: Breathing Life into Message Sequence Charts. Formal Methods in System Design\u00a019, 121\u2013141 (2001)","journal-title":"Formal Methods in System Design"},{"key":"27_CR8","unstructured":"ITU-T: ITU-T Recommendation Z.120: Message Sequence Chart (MSC). ITU-T, Geneva (1999)"},{"key":"27_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"561","DOI":"10.1007\/10722167_45","volume-title":"SPIN Model Checking and Software Verification","author":"T. Bienm\u00fcller","year":"2000","unstructured":"Bienm\u00fcller, T., Damm, W., Wittke, H.: The statemate verification environment - making it real. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol.\u00a01885, pp. 561\u2013567. Springer, Heidelberg (2000)"},{"key":"27_CR10","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":"27_CR11","doi-asserted-by":"crossref","unstructured":"Klose, J., Kropf, T., Ruf, J.: A Visual Approach to Validating System Level Designs. In: Proceedings ISSS 2002, pp. 186\u2013191. ACM Press, New York (2002)","DOI":"10.1145\/581233.581240"},{"key":"27_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/3-540-45441-1_24","volume-title":"\u00abUML\u00bb 2001 \u2013 The Unified Modeling Language. Modeling Languages, Concepts, and Tools","author":"J. Klose","year":"2001","unstructured":"Klose, J., Lettrari, M.: Scenario-based Monitoring and Testing of Real-time UML models. In: Gogolla, M., Kobryn, C. (eds.) UML 2001. LNCS, vol.\u00a02185, p. 317. Springer, Heidelberg (2001)"},{"key":"27_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1007\/978-3-540-27863-4_8","volume-title":"Integration of Software Specification Techniques for Applications in Engineering","author":"F. H\u00e4nsel","year":"2004","unstructured":"H\u00e4nsel, F., Poliak, J., Slov\u00e1k, R., Schnieder, E.: Reference case study for comparison and validation of formal specifications using a model demonstrator. 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. 96\u2013118. Springer, Heidelberg (2004)"},{"key":"27_CR14","unstructured":"Jansen, L.: Referenzfallstudie Verkehrsleittechnik (1997) \n                    \n                      http:\/\/www.iva.ing.tubs.de\/institut\/projekte\/Referenzfallstudie_vklt\/referenz.html\n                    \n                    \n                   (16.5.2004)"},{"key":"27_CR15","unstructured":"AG, D.B.: Betriebliches Lastenheft f\u00fcr FunkFahrBetrieb (1996) Minimalkonzept, Version 2.0."},{"key":"27_CR16","unstructured":"Klose, J., Thums, A.: The Statemate Reference Model of the Reference Case Study \u2019Verkehrsleittechnik\u2019. Technical report, University of Augsburg (2000), \n                    \n                      http:\/\/www.Informatik.Uni-Augsburg.DE\/swt\/formosa\/RefVL\/bericht.ps.gz"},{"key":"27_CR17","unstructured":"Klose, J.: Live Sequence Charts: A Graphical Formalism for the Specification of Communication Behavior. PhD thesis, Carl von Ossietzky Universit\u00e4t Oldenburg (2003)"},{"key":"27_CR18","unstructured":"Klose, J., Moik, A.: Modellierung der FORMS-Fallstudien mit Statemate. In: Schnieder, E. (ed.) Proceedings FORMS 2000. Fortschritt-Berichte VDI Reihe 12, vol.\u00a0441, VDI Verlag (2000)"},{"key":"27_CR19","unstructured":"Damm, W., D\u00f6hmen, G., Klose, J.: Secure Decentralized Control of Railway Crossings. In: Gnesi, S., Latella, D. (eds.) Fourth International ERCIM Workshop on Formal Methods in Industrial Critical Systems (1999)"},{"key":"27_CR20","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1145\/235321.235322","volume":"5","author":"D. Harel","year":"1996","unstructured":"Harel, D., Naamad, A.: The statemate semantics of statecharts. ACM Trans. Softw. Eng. Methodol.\u00a05, 293\u2013333 (1996)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"27_CR21","unstructured":"Josko, B.: Modular specification and verification of reactive systems. Carl von Ossietzky Universit\u00e4t Oldenburg, Habilitationsschrift (1993)"},{"key":"27_CR22","unstructured":"Schl\u00f6r, R.C.: Symbolic Timing Diagrams: A Visual Formalism for Model Verification. PhD thesis, Universit\u00e4t Oldenburg (2000)"},{"key":"27_CR23","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)"},{"key":"27_CR24","unstructured":"The VIS Group: VIS: A System for Verification and Synthesis. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, Springer, Heidelberg (1996)"},{"key":"27_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"key":"27_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/3-540-49519-3_7","volume-title":"Formal Methods in Computer-Aided Design","author":"M. Sheeran","year":"1998","unstructured":"Sheeran, M., St\u00e5lmarck, G.: A tutorial on St\u00e5lmarck\u2019s proof procedure for propositional logic. In: Gopalakrishnan, G.C., Windley, P. (eds.) FMCAD 1998. LNCS, vol.\u00a01522, pp. 82\u201399. Springer, Heidelberg (1998)"},{"key":"27_CR27","unstructured":"Gr\u00e9goire, B.: Automata oriented program verification. Master\u2019s thesis, Facult\u00e9s Universitaires Notre-Dame de la Paix, Namur (2002)"},{"key":"27_CR28","unstructured":"Harel, D., Marelly, R.: Playing with Time: On the Specification and Execution of Time-Enriched LSCs. In: Proceedings MASCOTS 2002 (2002)"},{"key":"27_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-540-39656-7_4","volume-title":"Formal Methods for Components and Objects","author":"W. Damm","year":"2003","unstructured":"Damm, W., Westphal, B.: Live and let die: LSC-based verification of UML-models. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2002. LNCS, vol.\u00a02852, pp. 99\u2013135. Springer, Heidelberg (2003)"},{"key":"27_CR30","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1016\/S0167-6423(99)00030-1","volume":"37","author":"K.L. McMillan","year":"2000","unstructured":"McMillan, K.L.: A Methodology for Hardware Verification using Compositional Model Checking. Science of Computer Programming\u00a037, 279\u2013309 (2000)","journal-title":"Science of Computer Programming"},{"key":"27_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/3-540-45923-5_5","volume-title":"Fundamental Approaches to Software Engineering","author":"F. Xie","year":"2002","unstructured":"Xie, F., Browne, J.: Integrated State Space Reduction for Model Checking Executable Object-oriented Software System Designs. In: Kutsche, R.-D., Weber, H. (eds.) FASE 2002. LNCS, vol.\u00a02306, p. 64. Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","Integration of Software Specification Techniques for Applications in Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-27863-4_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T18:36:15Z","timestamp":1558290975000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-27863-4_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540231356","9783540278634"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-27863-4_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}