{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,15]],"date-time":"2025-08-15T00:29:53Z","timestamp":1755217793551,"version":"3.43.0"},"reference-count":29,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2001,9,1]],"date-time":"2001-09-01T00:00:00Z","timestamp":999302400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2001,9,1]],"date-time":"2001-09-01T00:00:00Z","timestamp":999302400000},"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":["Formal Methods in System Design"],"published-print":{"date-parts":[[2001,9]]},"DOI":"10.1023\/a:1011279932612","type":"journal-article","created":{"date-parts":[[2002,12,23]],"date-time":"2002-12-23T04:18:21Z","timestamp":1040617101000},"page":"121-141","source":"Crossref","is-referenced-by-count":36,"title":["Verification of a Radio-Based Signaling System Using the STATEMATE Verification Environment"],"prefix":"10.1007","volume":"19","author":[{"given":"Werner","family":"Damm","sequence":"first","affiliation":[]},{"given":"Jochen","family":"Klose","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"336114_CR1","unstructured":"A. Allara, M. Bombana, S. Comai, B. Josko, R. Schl\u00f6r, and D. Sciuto, \u201cSpecification of embedded monitors for property checking,\u201d in Proceedings of the Forum on Design Languages, FDL'99, ECSI, 1999, pp 117\u2013126."},{"key":"336114_CR2","first-page":"167","volume-title":"Design, Automation and Test in Europe\/User Forum","author":"A. Allara","year":"1999","unstructured":"A. Allara, S. Comai, and R. Schl\u00f6r, \u201cSystem verification using user-friendly interfaces,\u201d in Design, Automation and Test in Europe\/User Forum, IEEE Computer Society Press, Los Alamitos, 1999, pp. 167\u2013172."},{"issue":"7","key":"336114_CR3","doi-asserted-by":"crossref","first-page":"498","DOI":"10.1109\/32.708566","volume":"24","author":"R. Anderson","year":"1998","unstructured":"R. Anderson, P. Beame, S. Burns, W. Chan, F. Modugno, D. Notkin, and J. Reese, \u201cModel checking large software specifications,\u201d IEEE Transactions on Software Engineering, Vol. 24, No. 7, pp. 498\u2013520, 1998.","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"2","key":"336114_CR4","doi-asserted-by":"crossref","first-page":"139","DOI":"10.1023\/A:1008645826258","volume":"12","author":"C. Bernardeschi","year":"1998","unstructured":"C. Bernardeschi, A. Fantechi, S. Gnesi, S. LaRosa, G. Mongardi, and D. Romano, \u201cA formal verification environment for railway signaling design,\u201d Formal Methods in System Design, Vol. 12, No. 2, pp. 139\u2013162, 1998.","journal-title":"Formal Methods in System Design"},{"key":"336114_CR5","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1007\/3-540-48092-7_14","volume-title":"Correct System Design","author":"T. Bienm\u00fcller","year":"1999","unstructured":"T. Bienm\u00fcller, J. Bohn, H. Brinkmann, U. Brockmeyer, W. Damm, H. Hungar, and P. Jansen, \u201cVerification of automotive control units,\u201d in E.-R. Olderog and B. Steffen (Eds.), Correct System Design, Springer Verlag, Berlin, 1999, number 1710 in LNCS, pp. 319\u2013341."},{"key":"336114_CR6","first-page":"150","volume-title":"Towards System Safety\u2014Proceedings of the Seventh Safety-critical Systems Symposium, Huntingdon, UK","author":"T. Bienm\u00fcller","year":"1999","unstructured":"T. Bienm\u00fcller, U. Brockmeyer, W. Damm, G. D\u00f6hmen, C. E\u00dfmann, H.-J. Holberg, H. Hungar, B. Josko, R. Schl\u00f6r, G. Wittich, H. Wittke, G. Clements, J. Rowlands, and E. Sefton, \u201cFormal verification of an avionics application using abstraction and symbolic model checking,\u201d in F. Redmill and T. Anderson (Eds.), Towards System Safety\u2014Proceedings of the Seventh Safety-critical Systems Symposium, Huntingdon, UK, Safety-Critical Systems Club, Springer Verlag, Berlin, 1999, pp. 150\u2013173."},{"key":"336114_CR7","first-page":"165","volume":"10","author":"A.D. Bimbo","year":"1999","unstructured":"A.D. Bimbo and E. Vicario, \u201cA visual formalism for computational tree logic,\u201d Journal of Visual Languages, Vol. 10, pp. 165\u2013187, 1999.","journal-title":"Journal of Visual Languages"},{"key":"336114_CR8","unstructured":"J. Bohn, U. Brockmeyer, C. E\u00dfmann, and H. Hungar, \u201cSMI\u2014System Modelling Interface, Draft Version 0.1,\u201d Technical Report, Kuratorium OFFIS, e.V., Oldenburg, 1999."},{"key":"336114_CR9","first-page":"283","volume-title":"FSTTCS","author":"J. Bohn","year":"1998","unstructured":"J. Bohn, W. Damm, O. Grumberg, H. Hungar, and K. Laster, \u201cFirst-order-CTL model checking,\u201d in FSTTCS, Springer Verlag, Berlin, 1998, number 1530 in LNCS, pp. 283\u2013294."},{"key":"336114_CR10","doi-asserted-by":"crossref","first-page":"338","DOI":"10.1007\/s001650050021","volume":"10","author":"A. Bor\u00e4lv","year":"1998","unstructured":"A. Bor\u00e4lv, \u201cCase study: Formal verification of a computerized railway interlocking,\u201d Formal Aspects of Computing, Vol. 10, pp. 338\u2013360, 1998.","journal-title":"Formal Aspects of Computing"},{"key":"336114_CR11","unstructured":"U. Brockmeyer and H. Hungar, \u201cSSL\u2014System Specification Language, Draft Version 0.1,\u201d Technical Report, Kuratorium OFFIS, e.V., Oldenburg, 1999."},{"key":"336114_CR12","doi-asserted-by":"crossref","first-page":"361","DOI":"10.1007\/s001650050022","volume":"10","author":"A. Cimatti","year":"1998","unstructured":"A. Cimatti, F. Giunchiglia, G. Mongardi, D. Romano, F. Torielli, and P. Traverso, \u201cFormal verification of a railway interlocking system using model cecking,\u201d Formal Aspects of Computing, Vol. 10, pp. 361\u2013380, 1998.","journal-title":"Formal Aspects of Computing"},{"key":"336114_CR13","volume-title":"FMOODS'99 IFIP TC6\/ WG6.1 Third International Conference on Formal Methods for Open Object-Based Distributed Systems","author":"W. Damm","year":"1999","unstructured":"W. Damm and D. Harel, \u201cLSCs: breathing life into message sequence charts,\u201d in FMOODS'99 IFIP TC6\/ WG6.1 Third International Conference on Formal Methods for Open Object-Based Distributed Systems, Kluwer Academic Publishers, NY, 1999."},{"key":"336114_CR14","doi-asserted-by":"crossref","unstructured":"W. Damm, B. Josko, H. Hungar, and A. Pnueli, \u201cA compositional real-time semantics of STATEMATE designs,\u201d in W.-P. de Roever (Ed.), Proceedings, International Symposium on Compositionality\u2014The Significant Difference, Springer-Verlag, 1998, Lecture Notes in Computer Science.","DOI":"10.1007\/3-540-49213-5_8"},{"key":"336114_CR15","unstructured":"M. Fessler and J. Sch\u00fctte, \u201cDie methode B\u2014Sichere software f\u00a8ur bahnanwendungen, 1999,\u201d Presentation at Formale Techniken f\u00fcr Eisenbahnsicherungssysteme\u2014FORMS'99, http:\/\/www.ifra.ing.tu-bs.de\/forms\/."},{"key":"336114_CR16","series-title":"Technical Report","volume-title":"Realtime Symbolic Timing Diagrams","author":"K. Feyerabend","year":"1996","unstructured":"K. Feyerabend, \u201cRealtime Symbolic Timing Diagrams,\u201d Technical Report, Carl von Ossietzky Universit\u00e4t Oldenburg, 1996."},{"key":"336114_CR17","doi-asserted-by":"crossref","unstructured":"K. Feyerabend and B. Josko, \u201cA visual formalism for real time requirement specifications,\u201d in Proceedings of the 4th International AMAST Workshop on Real-Time Systems and Concurrent and Distributed Software, ARTS'97, Lecture Notes in Computer Science 1231, 1997, pp. 156\u2013168.","DOI":"10.1007\/3-540-63010-4_11"},{"key":"336114_CR18","unstructured":"W.J. Fokkink and P. Hollingshead, \u201cVerification of interlockings: from control tables to ladder logic diagrams,\u201d in Proceedings of the 3rd Workshop on Formal Methods for Industrial Critical Systems\u2013FMICS'98, Amsterdam. Stichting Mathematisch Centrum, 1998."},{"key":"336114_CR19","unstructured":"J. Groote, J. Koorn, and S. van Vlijmen, \u201cThe safety guaranteeing system at station Koorn-Kersenboogerd,\u201d in Proceedings of the 10th IEEE Conference on Computer Assurance COMPASS 95, IEEE, 1995, pp. 131\u2013150."},{"key":"336114_CR20","unstructured":"T.V. Group, \u201cVIS: A system for verification and synthesis,\u201d in 8th international Conference on Computer Aided Verification, number 1102 in LNCS, 1996. VIS 1.3 is available from the VIS home-page: http:\/\/wwwcad. eecs.Berkeley.EDU\/~vis."},{"key":"336114_CR21","volume-title":"Modeling Reactive Systems with Statecharts: The STATEMATE Approach","author":"D. Harel","year":"1996","unstructured":"D. Harel and M. Politi, Modeling Reactive Systems with Statecharts: The STATEMATE Approach. Part No. D\u20131100\u201343. i-Logix Inc., Three Riverside Drive, Andover, MA 01810, June 1996."},{"key":"336114_CR22","doi-asserted-by":"crossref","unstructured":"V.Hartonas-Garmhausen, S. Campos, A. Cimatti, E. Clarke, and F. Giunchiglia, \u201cVerification of a safetycritical railway interlocking system with real-time constraints,\u201d in Proceedings of the 28th International Symposium on Fault-Tolerant Computing (FTCS-28), IEEE Computer Society Press, 1998, pp. 458\u2013463.","DOI":"10.1109\/FTCS.1998.689498"},{"key":"336114_CR23","unstructured":"J. Hoffmann, H.-J. Holberg, and R. Schl\u00f6r, \u201cIndustrieller einsatz formaler verifikationsmethoden,\u201d Feb. 2000. to appear in ITG\/GI\/GMM-Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, Frankfurt\/Main."},{"key":"336114_CR24","volume-title":"ITU-T Recommendation Z.120: Message Sequence Chart (MSC)","author":"ITU-T","year":"1996","unstructured":"ITU-T, ITU-T Recommendation Z.120: Message Sequence Chart (MSC). ITU-T, Geneva, October 1996."},{"issue":"1","key":"336114_CR25","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1145\/237432.237438","volume":"6","author":"L.E. Moser","year":"1997","unstructured":"L.E. Moser, Y. Ramakrishna, G. Kutty, P. Melliar-Smith, and L. Dillon, \u201cAgraphical environment for design of concurrent real-time systems,\u201d ACM Transactions on Software Engineering and Methodology, Vol. 6, No. 1, pp. 31\u201379, 1997.","journal-title":"ACM Transactions on Software Engineering and Methodology"},{"key":"336114_CR26","unstructured":"OMG, Unified Modeling Language Specification, Version 1.3. OMG, 1999. http:\/\/www.rational.com\/uml\/ resources\/documentation."},{"key":"336114_CR27","unstructured":"F. Pilarski, \u201cCost effectiveness of formal methods in the development of avionics systems at aerospatiale,\u201d in 17th Digital Avionics Systems Conference, Seattle, October 1998."},{"key":"336114_CR28","unstructured":"H.-J. Reder, \u201cEntwicklungsmethodik und werkzeugkette GRACE, 1999,\u201d Presentation at Formale Techniken f\u00fcr Eisenbahnsicherungssysteme\u2014FORMS'99, http:\/\/www.ifra.ing.tu-bs.de\/forms\/."},{"key":"336114_CR29","doi-asserted-by":"crossref","unstructured":"R. Schl\u00f6r, B. Josko, and D. Werth, \u201cUsing a visual formalism for design verification in industrial environments,\u201d in VISUAL'98, number 1385 in LNCS, Springer Verlag, 1998, pp. 208\u2013221.","DOI":"10.1007\/BFb0053507"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1011279932612.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1011279932612\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1011279932612.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T20:04:55Z","timestamp":1754424295000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1011279932612"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001,9]]},"references-count":29,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2001,9]]}},"alternative-id":["336114"],"URL":"https:\/\/doi.org\/10.1023\/a:1011279932612","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2001,9]]}}}