{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,5]],"date-time":"2025-04-05T19:23:45Z","timestamp":1743881025573},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319641188"},{"type":"electronic","value":"9783319641195"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-64119-5_1","type":"book-chapter","created":{"date-parts":[[2017,8,1]],"date-time":"2017-08-01T13:05:09Z","timestamp":1501592709000},"page":"3-18","source":"Crossref","is-referenced-by-count":2,"title":["Building Models We Can Rely On: Requirements Traceability for Model-Based Verification Techniques"],"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":[[2017,8,2]]},"reference":[{"key":"1_CR1","doi-asserted-by":"publisher","unstructured":"Aceituna, D., Do, H.: Exposing the susceptibility of off-nominal behaviors in reactive system requirements. In: RE, pp. 136\u2013145 (2015). doi:\n10.1109\/RE.2015.7320416","DOI":"10.1109\/RE.2015.7320416"},{"key":"1_CR2","doi-asserted-by":"publisher","unstructured":"Aceituna, D., Do, H., Srinivasan, S.: A systematic approach to transforming system requirements into model checking specifications. In: ICSE, pp. 165\u2013174 (2014). doi:\n10.1145\/2591062.2591183","DOI":"10.1145\/2591062.2591183"},{"key":"1_CR3","doi-asserted-by":"publisher","unstructured":"Ammann, P.E., Black, P.E., Majurski, W.: Using model checking to generate tests from specifications. In: Proceedings of the Second International Conference on Formal Engineering Methods, pp. 46\u201354. IEEE (1998). doi:\n10.1007\/3-540-48166-4_10","DOI":"10.1007\/3-540-48166-4_10"},{"key":"1_CR4","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P., Larsen, K.G.: Principles of Model Checking. MIT Press, Cambridge (2008). ISBN: 9780262026499"},{"key":"1_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/978-3-319-45477-1_8","volume-title":"Computer Safety, Reliability, and Security","author":"V Bos","year":"2016","unstructured":"Bos, V., Bruintjes, H., Tonetta, S.: Catalogue of system and software properties. In: Skavhaug, A., Guiochet, J., Bitsch, F. (eds.) SAFECOMP 2016. LNCS, vol. 9922, pp. 88\u2013101. Springer, Cham (2016). doi:\n10.1007\/978-3-319-45477-1_8"},{"key":"1_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-642-04468-7_15","volume-title":"Computer Safety, Reliability, and Security","author":"M Bozzano","year":"2009","unstructured":"Bozzano, M., Cimatti, A., Katoen, J.P., Nguyen, V.Y., Noll, T., Roveri, M.: The COMPASS approach: correctness, modelling and performability of aerospace systems. In: Buth, B., Rabe, G., Seyfarth, T. (eds.) SAFECOMP 2009. LNCS, vol. 5775, pp. 173\u2013186. Springer, Heidelberg (2009). doi:\n10.1007\/978-3-642-04468-7_15"},{"key":"1_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-540-75596-8_13","volume-title":"Automated Technology for Verification and Analysis","author":"M Bozzano","year":"2007","unstructured":"Bozzano, M., Cimatti, A., Tapparo, F.: Symbolic fault tree analysis for reactive systems. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol. 4762, pp. 162\u2013176. Springer, Heidelberg (2007). doi:\n10.1007\/978-3-540-75596-8_13"},{"key":"1_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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). doi:\n10.1007\/978-3-642-03240-0_15"},{"key":"1_CR9","unstructured":"EN 50128: Railway applications-communication, signaling and processing systems-software for railway control and protection systems (2011)"},{"key":"1_CR10","unstructured":"Filax, M., Gonschorek, T., Lipaczewski, M., Ortmeier, F.: On traceability of informal specifications for model-based verification. In: IMBSA: Short & Tutorial Proceedings, pp. 11\u201318. OvGU Magdeburg (2014)"},{"key":"1_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1007\/978-3-319-33951-1_8","volume-title":"Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification","author":"M Filax","year":"2016","unstructured":"Filax, M., Gonschorek, T., Ortmeier, F.: Correct formalization of requirement specifications: a v-model for building formal models. In: Lecomte, T., Pinger, R., Romanovsky, A. (eds.) RSSR 2016. LNCS, vol. 9707, pp. 106\u2013122. Springer, Cham (2016). doi:\n10.1007\/978-3-319-33951-1_8"},{"key":"1_CR12","doi-asserted-by":"publisher","unstructured":"Ge, X., Paige, R.F., McDermid, J.A.: Analysing system failure behaviours with PRISM. In: SSIRI-C, pp. 130\u2013136 (2010). doi:\n10.1109\/SSIRI-C.2010.32","DOI":"10.1109\/SSIRI-C.2010.32"},{"key":"1_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1007\/978-3-540-75101-4_44","volume-title":"Computer Safety, Reliability, and Security","author":"M G\u00fcdemann","year":"2007","unstructured":"G\u00fcdemann, M., Ortmeier, F., Reif, W.: Using deductive cause-consequence analysis (DCCA) with SCADE. In: Saglietti, F., Oster, N. (eds.) SAFECOMP 2007. LNCS, vol. 4680, pp. 465\u2013478. Springer, Heidelberg (2007). doi:\n10.1007\/978-3-540-75101-4_44"},{"key":"1_CR14","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1016\/j.scico.2013.03.008","volume":"82","author":"S Hallerstede","year":"2014","unstructured":"Hallerstede, S., Jastram, M., Ladenberger, L.: A method and tool for tracing requirements into specifications. Sci. Comput. Program. 82, 2\u201321 (2014). doi:\n10.1016\/j.scico.2013.03.008","journal-title":"Sci. Comput. Program."},{"key":"1_CR15","unstructured":"IEC 61508: Functional safety of electrical\/electronic\/programmable electronic safety-related systems (2005)"},{"key":"1_CR16","unstructured":"ISO 26262: Road Vehicles-Functional Safety (2009)"},{"key":"1_CR17","unstructured":"OMG UML: Unified modeling language, superstructure (2011)"},{"key":"1_CR18","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1016\/j.entcs.2007.05.034","volume":"185","author":"F Ortmeier","year":"2007","unstructured":"Ortmeier, F., Schellhorn, G.: Formal fault tree analysis-practical experiences. Electron. Not. Theoret. Comput. Sci. 185, 139\u2013151 (2007). doi:\n10.1016\/j.entcs.2007.05.034","journal-title":"Electron. Not. Theoret. Comput. Sci."},{"issue":"22","key":"1_CR19","doi-asserted-by":"publisher","first-page":"109","DOI":"10.3182\/20130904-3-UK-4041.00015","volume":"46","author":"D Soliman","year":"2013","unstructured":"Soliman, D., Frey, G., Thramboulidis, K.: On formal verification of function block applications in safety-related software development. IFAC 46(22), 109\u2013114 (2013). doi:\n10.3182\/20130904-3-UK-4041.00015","journal-title":"IFAC"},{"key":"1_CR20","unstructured":"Withall, S.: Software Requirement Patterns (Developer Best Practices). Microsoft Press (2007). ISBN: 9780735623989"}],"container-title":["Lecture Notes in Computer Science","Model-Based Safety and Assessment"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-64119-5_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,8,1]],"date-time":"2017-08-01T13:05:10Z","timestamp":1501592710000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-64119-5_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319641188","9783319641195"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-64119-5_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}