{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,12]],"date-time":"2026-03-12T15:51:54Z","timestamp":1773330714268,"version":"3.50.1"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319339504","type":"print"},{"value":"9783319339511","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-33951-1_8","type":"book-chapter","created":{"date-parts":[[2016,6,14]],"date-time":"2016-06-14T09:21:26Z","timestamp":1465896086000},"page":"106-122","source":"Crossref","is-referenced-by-count":6,"title":["Correct Formalization of Requirement Specifications: A V-Model for Building Formal Models"],"prefix":"10.1007","author":[{"given":"Marco","family":"Filax","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tim","family":"Gonschorek","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Frank","family":"Ortmeier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,6,15]]},"reference":[{"key":"8_CR1","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1109\/MS.1984.233702","volume":"1","author":"BW Boehm","year":"1984","unstructured":"Boehm, B.W.: Verifying and validating software requirements and design specifications. IEEE Softw. 1, 75\u201388 (1984)","journal-title":"IEEE Softw."},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"Bose, P.: Automated translation of UML models of architectures for verification and simulation using spin. In: ASE, pp. 102\u2013109. IEEE (1999)","DOI":"10.1109\/ASE.1999.802135"},{"key":"8_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"494","DOI":"10.1007\/978-3-540-27863-4_27","volume-title":"Integration of Software Specification Techniques for Applications in Engineering","author":"M Brill","year":"2004","unstructured":"Brill, M., Buscherm\u00f6hle, R., Damm, W., Klose, J., Westphal, B., Wittke, H.: Formal verification of LSCs in the development process. In: Ehrig, H., Damm, W., Desel, J., Gro\u00dfe-Rhode, M., Reif, W., Schnieder, E., Westk\u00e4mper, E. (eds.) INT 2004. LNCS, vol. 3147, pp. 494\u2013516. Springer, Heidelberg (2004)"},{"key":"8_CR4","unstructured":"Burmester, S., Giese, H., Hirsch, M., Schilling, D.: Incremental design and formal verification with UML\/RT in the FUJABA real-time tool suite. In: SVERTS, pp. 1\u201320. Citeseer (2004)"},{"key":"8_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1007\/978-3-540-68624-8_7","volume-title":"Reliable Software Technologies \u2013 Ada-Europe 2008","author":"L Carnevali","year":"2008","unstructured":"Carnevali, L., Grassi, L., Vicario, E.: A tailored V-model exploiting the theory of preemptive time petri nets. In: Kordon, F., Vardanega, T. (eds.) Ada-Europe 2008. LNCS, vol. 5026, pp. 87\u2013100. Springer, Heidelberg (2008)"},{"key":"8_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"334","DOI":"10.1007\/978-3-319-08867-9_22","volume-title":"Computer Aided Verification","author":"R Cavada","year":"2014","unstructured":"Cavada, R., et al.: The nuXmv symbolic model checker. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 334\u2013342. Springer, Heidelberg (2014)"},{"key":"8_CR7","unstructured":"CENELEC: 50129. Railway Applications: Safety Related Electronic Systems for Signalling (1998)"},{"key":"8_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"166","DOI":"10.1007\/978-3-642-03240-0_15","volume-title":"Formal Methods for Industrial Critical Systems","author":"A Cimatti","year":"2009","unstructured":"Cimatti, A., Roveri, M., Susi, A., Tonetta, S.: From informal requirements to property-driven formal validation. In: Cofer, D., Fantechi, A. (eds.) FMICS 2008. LNCS, vol. 5596, pp. 166\u2013181. Springer, Heidelberg (2009)"},{"key":"8_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"277","DOI":"10.1007\/978-3-642-31424-7_23","volume-title":"Computer Aided Verification","author":"A Cimatti","year":"2012","unstructured":"Cimatti, A., Griggio, A.: Software model checking via IC3. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 277\u2013293. Springer, Heidelberg (2012)"},{"key":"8_CR10","volume-title":"UAT Defined: A Guide to Practical User Acceptance Testing","author":"R Cimperman","year":"2006","unstructured":"Cimperman, R.: UAT Defined: A Guide to Practical User Acceptance Testing. Addison-Wesley Professional, Upper Saddle River (2006)"},{"key":"8_CR11","volume-title":"Model Checking","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"218","DOI":"10.1007\/3-540-45923-5_15","volume-title":"Fundamental Approaches to Software Engineering","author":"A David","year":"2002","unstructured":"David, A., M\u00f6ller, M.O., Yi, W.: Formal verification of UML statecharts with real-time extensions. In: Kutsche, R.-D., Weber, H. (eds.) FASE 2002. LNCS, vol. 2306, pp. 218\u2013232. Springer, Heidelberg (2002)"},{"key":"8_CR13","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"EA Emerson","year":"1986","unstructured":"Emerson, E.A., Halpern, J.Y.: Sometimes and not never revisited: on branching versus linear time temporal logic. J. ACM 33, 151\u2013178 (1986)","journal-title":"J. ACM"},{"key":"8_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1007\/11576280_5","volume-title":"Formal Methods and Software Engineering","author":"H Fecher","year":"2005","unstructured":"Fecher, H., Sch\u00f6nborn, J., Kyas, M., de Roever, W.-P.: 29 new unclarities in the semantics of UML 2.0 state machines. In: Lau, K.-K., Banach, R. (eds.) ICFEM 2005. LNCS, vol. 3785, pp. 52\u201365. Springer, Heidelberg (2005)"},{"key":"8_CR15","unstructured":"Filax, M., Gonschorek, T., Lipaczewski, M., Ortmeier, F.: On traceability of informal specifications for model-based verification. In: IMBSA 2014: Short & Tutorial Proceedings, pp. 11\u201318 (2014)"},{"key":"8_CR16","doi-asserted-by":"crossref","unstructured":"Giese, H., Tichy, M., Burmester, S., Sch\u00e4fer, W., Flake, S.: Towards the compositional verification of real-time UML designs. In: ESEC\/FSE, pp. 38\u201347 (2003)","DOI":"10.1145\/940071.940078"},{"key":"8_CR17","unstructured":"Gonschorek, T., Filax, M., Lipaczewski, M., Ortmeier, F.: VECS - verification enviroment for critical systems - tool supported formal modeling an verification. In: IMBSA 2014: Short & Tutorial Proceedings, pp. 63\u201364 (2014)"},{"key":"8_CR18","unstructured":"G\u00fcdemann, M.: Qualitative and quantitative formal model-based safety analysis. Ph.D. thesis, Otto-von-Guericke-Universit\u00e4t Magdeburg (2011)"},{"key":"8_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1007\/978-3-540-24756-2_11","volume-title":"Integrated Formal Methods","author":"K Lano","year":"2004","unstructured":"Lano, K., Clark, D., Androutsopoulos, K.: UML to B: formal verification of object-oriented models. In: Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. LNCS, vol. 2999, pp. 187\u2013206. Springer, Heidelberg (2004)"},{"key":"8_CR20","first-page":"637","volume":"11","author":"D Latella","year":"1999","unstructured":"Latella, D., Majzik, I., Massink, M.: Automatic verification of a behavioural subset of UML statechart diagrams using the spin model-checker. FAC 11, 637\u2013664 (1999)","journal-title":"FAC"},{"key":"8_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"430","DOI":"10.1007\/3-540-46852-8_31","volume-title":"\u00abUML\u00bb \u201999 - The Unified Modeling Language. Beyond the Standard","author":"J Lilius","year":"1999","unstructured":"Lilius, J., Paltor, I.P.: Formalising UML state machines for model checking. In: France, R.B. (ed.) UML 1999. LNCS, vol. 1723, pp. 430\u2013444. Springer, Heidelberg (1999)"},{"key":"8_CR22","doi-asserted-by":"crossref","unstructured":"Lilius, J., Paltor, I.P.: vUML: A tool for verifying UML models. In: ASE, pp. 255\u2013258. IEEE (1999)","DOI":"10.1109\/ASE.1999.802301"},{"key":"8_CR23","unstructured":"OMG: OMG Unified Modeling Language (OMG UML), Superstructure. Object Management Group (2011)"},{"key":"8_CR24","doi-asserted-by":"crossref","first-page":"92","DOI":"10.1145\/1125808.1125811","volume":"15","author":"C Snook","year":"2006","unstructured":"Snook, C., Butler, M.: UML-B: Formal modeling and design aided by UML. TOSEM 15, 92\u2013122 (2006)","journal-title":"TOSEM"},{"key":"8_CR25","doi-asserted-by":"crossref","unstructured":"Tang, W., Ning, B., Xu, T., Zhao, L.H.: Scenario-based modeling and verification of system requirement specification for the european train control system. In: Computers in Railways XII, pp. 759\u2013770 (2010)","DOI":"10.2495\/CR100691"},{"key":"8_CR26","unstructured":"Vardi, M., Wolper, P.: An automata-theoretic approach to automatic program verification. In: LICS, pp. 322\u2013331. IEEE (1986)"},{"key":"8_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"378","DOI":"10.1007\/3-540-45832-8_28","volume-title":"Graph Transformation","author":"A Varr\u00f3","year":"2002","unstructured":"Varr\u00f3, A.: A formal semantics of UML statecharts by model transition systems. In: Corradini, A., Ehrig, H., Kreowski, H.-J., Rozenberg, G. (eds.) ICGT 2002. LNCS, vol. 2505, pp. 378\u2013392. Springer, Heidelberg (2002)"},{"key":"8_CR28","unstructured":"Vizel, Y., Grumberg, O., Shoham, S.: Lazy abstraction and sat-based reachability in hardware model checking. In: FMCAD, pp. 173\u2013181. IEEE (2012)"}],"container-title":["Lecture Notes in Computer Science","Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-33951-1_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,3]],"date-time":"2025-06-03T21:40:23Z","timestamp":1748986823000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-33951-1_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319339504","9783319339511"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-33951-1_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]}}}