{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T13:20:31Z","timestamp":1742995231998,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540884781"},{"type":"electronic","value":"9783540884798"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"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":[[2008]]},"DOI":"10.1007\/978-3-540-88479-8_25","type":"book-chapter","created":{"date-parts":[[2008,11,4]],"date-time":"2008-11-04T14:18:43Z","timestamp":1225808323000},"page":"354-368","source":"Crossref","is-referenced-by-count":1,"title":["Navigating the Requirements Jungle"],"prefix":"10.1007","author":[{"given":"Boris","family":"Langer","sequence":"first","affiliation":[]},{"given":"Michael","family":"Tautschnig","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"25_CR1","doi-asserted-by":"crossref","unstructured":"Nuseibeh, B., Easterbrook, S.: Requirements engineering: A roadmap. In: Finkelstein, A.C.W. (ed.) The Future of Software Engineering, Companion volume to ICSE (2000)","DOI":"10.1145\/336512.336523"},{"key":"25_CR2","unstructured":"IEEE New York, NY, USA: IEEE Recommended Practice for Software Requirements Specifications (June 1998)"},{"key":"25_CR3","unstructured":"Society of Automotive Engineers, Inc. Warrendale, PA, USA: SAE ARP 4754, Certification Considerations For Highly-Integrated Or Complex Aircraft Systems (November 1996)"},{"key":"25_CR4","unstructured":"RTCA Inc. \/ EUROCAE: DO-178B \/ ED-12B, Software Considerations in Airborne Systems and Equipment Certification (December 1992)"},{"key":"25_CR5","unstructured":"International Organization for Standardization: ISO\/IEC 9126-1:2001, Software engineering \u2013 Product quality \u2013 Part 1: Quality model (2001)"},{"key":"25_CR6","unstructured":"Airbus Industries Blagnac Cedex, France: Equipment \u2013 Design \u2013 General Requirements For Suppliers (December 1996)"},{"key":"25_CR7","unstructured":"Eide, P.L.H.: Quantification and Traceability of Requirements. Technical report, NTNU Norwegian University of Science and Technology (2005)"},{"key":"25_CR8","doi-asserted-by":"crossref","unstructured":"Kornecki, A.J., Hall, K., Hearn, D., Lau, H., Zalewsi, J.: Evaluation of software development tools for high assurance safety critical systems. In: HASE (2004)","DOI":"10.1109\/HASE.2004.1281755"},{"key":"25_CR9","volume-title":"Managing Software Requirements","author":"D. Leffingwell","year":"2003","unstructured":"Leffingwell, D., Widrig, D.: Managing Software Requirements. Addison-Wesley, Reading (2003)"},{"key":"25_CR10","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"25_CR11","unstructured":"Society of Automotive Engineers, Inc. Warrendale, PA, USA: SAE ARP 4754, Guidelines and Methods for Conducting the Safety Assessment Process on Civil Airborne Systems and Equipment (December 1996)"},{"key":"25_CR12","volume-title":"Principles of Program Analysis","author":"F. Nielson","year":"2005","unstructured":"Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis, 2nd edn. Springer, Heidelberg (2005)","edition":"2"},{"key":"25_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"757","DOI":"10.1007\/11901433_41","volume-title":"Formal Methods and Software Engineering","author":"A. Bauer","year":"2006","unstructured":"Bauer, A., Leucker, M., Streit, J.: SALT\u2014structured assertion language for temporal logic. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol.\u00a04260, pp. 757\u2013775. Springer, Heidelberg (2006)"},{"key":"25_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/3-540-44829-2_17","volume-title":"Model Checking Software","author":"T.A. Henzinger","year":"2003","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Software Verification with BLAST. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol.\u00a02648, pp. 235\u2013239. Springer, Heidelberg (2003)"},{"key":"25_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E.M. Clarke","year":"2004","unstructured":"Clarke, E.M., Kroening, D., Lerda, F.: A Tool for Checking ANSI-C Programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 168\u2013176. Springer, Heidelberg (2004)"},{"key":"25_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"553","DOI":"10.1007\/3-540-36577-X_40","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Khurshid","year":"2003","unstructured":"Khurshid, S., Pasareanu, C.S., Visser, W.: Generalized Symbolic Execution for Model Checking and Testing. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 553\u2013568. Springer, Heidelberg (2003)"},{"key":"25_CR17","unstructured":"Robinson, J.A., Voronkov, A. (eds.): Handbook of Automated Reasoning, vol.\u00a02. Elsevier and MIT Press (2001)"},{"key":"25_CR18","volume-title":"Isabelle\/HOL\u2014A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL\u2014A Proof Assistant for Higher-Order Logic. Springer, Heidelberg (2002)"},{"key":"25_CR19","unstructured":"Wall, A., Andersson, J., Norstr\u00f6m, C.: Probabilistic simulation-based analysis of complex real-times systems. In: ISORC (2003)"},{"key":"25_CR20","unstructured":"Tretmans, J., Brinksma, E.: TorX: Automated model-based tesing. In: ECMDSE (2003)"},{"key":"25_CR21","doi-asserted-by":"crossref","unstructured":"Holzer, A., Schallhart, C., Tautschnig, M., Veith, H.: FShell: Systematic Test Case Generation for Dynamic Analysis and Measurement. In: CAV, pp. 209\u2013213 (2008)","DOI":"10.1007\/978-3-540-70545-1_20"},{"key":"25_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/978-3-540-73368-3_11","volume-title":"Computer Aided Verification","author":"S. Chaki","year":"2007","unstructured":"Chaki, S., Schallhart, C., Veith, H.: Verification Across Intellectual Property Boundaries. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 82\u201394. Springer, Heidelberg (2007)"},{"key":"25_CR23","doi-asserted-by":"crossref","unstructured":"de Alfaro, L., Henzinger, T.A.: Interface Automata. In: FSE, pp. 109\u2013120 (2001)","DOI":"10.1145\/503209.503226"},{"key":"25_CR24","volume-title":"Types and programming languages","author":"B.C. Pierce","year":"2002","unstructured":"Pierce, B.C.: Types and programming languages. MIT Press, Cambridge (2002)"},{"key":"25_CR25","doi-asserted-by":"crossref","unstructured":"K\u00fchnel, C., Bauer, A., Tautschnig, M.: Compatibility and reuse in component-based systems via type and unit inference. In: SEAA, pp. 101\u2013108 (2007)","DOI":"10.1109\/EUROMICRO.2007.24"},{"key":"25_CR26","unstructured":"Vesely, W.E., et al.: Fault tree handbook. Technical Report NUREG-0492, Systems and Reliability Research, Office of Nuclear Regulatory Research, U.S. Nuclear Regulatory Commission, Washington, DC (1981)"},{"key":"25_CR27","volume-title":"Finite Markov Chains","author":"J.G. Kemeny","year":"1960","unstructured":"Kemeny, J.G., Snell, J.L.: Finite Markov Chains. Van Nostrand Reinhold, New York (1960)"},{"key":"25_CR28","unstructured":"Stamatis, D.H.: Failure Mode and Effect Analysis: FMEA from Theory to Execution, 2nd edn. ASQ Quality Press (2003)"},{"key":"25_CR29","doi-asserted-by":"crossref","unstructured":"Vardi, M.Y.: Automatic verification of probabilistic concurrent finite-state programs. In: FOCS, pp. 327\u2013338 (1985)","DOI":"10.1109\/SFCS.1985.12"},{"key":"25_CR30","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 2.0: A tool for probabilistic model checking. In: QEST, pp. 322\u2013323 (2004)","DOI":"10.1109\/QEST.2004.1348048"},{"key":"25_CR31","doi-asserted-by":"crossref","unstructured":"Kirner, R., Lang, R., Freiberger, G., Puschner, P.: Fully automatic worst-case execution time analysis for Matlab\/Simulink models. In: ECTRS, pp. 31\u201340 (2002)","DOI":"10.1109\/EMRTS.2002.1019183"},{"key":"25_CR32","doi-asserted-by":"crossref","unstructured":"Wang, Z., Haberl, W., Kugele, S., Tautschnig, M.: Automatic Generation of SystemC Models from Component-based Designs for Early Design Validation and Performance Analysis. In: WOSP (2008)","DOI":"10.1145\/1383559.1383577"},{"key":"25_CR33","unstructured":"Kirner, R., Veith, H.: Formal timing analysis suite for real-time programs. Technical Report\u00a058, Technische Universit\u00e4t Wien, Vienna, Austria (2005)"},{"key":"25_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"469","DOI":"10.1007\/3-540-45449-7_32","volume-title":"Embedded Software","author":"C. Ferdinand","year":"2001","unstructured":"Ferdinand, C., Heckmann, R., Langenbach, M., Martin, F., Schmidt, M., Theiling, H., Thesing, S., Wilhelm, R.: Reliable and precise WCET determination for a real-life processor. In: Henzinger, T.A., Kirsch, C.M. (eds.) EMSOFT 2001. LNCS, vol.\u00a02211, pp. 469\u2013485. Springer, Heidelberg (2001)"},{"key":"25_CR35","volume-title":"Large Scale C++ Software Design","author":"J. Lakos","year":"1996","unstructured":"Lakos, J.: Large Scale C++ Software Design. Addison-Wesley, Reading (1996)"}],"container-title":["Communications in Computer and Information Science","Leveraging Applications of Formal Methods, Verification and Validation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-88479-8_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,2]],"date-time":"2025-02-02T13:53:22Z","timestamp":1738504402000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-88479-8_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540884781","9783540884798"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-88479-8_25","relation":{},"ISSN":["1865-0929","1865-0937"],"issn-type":[{"type":"print","value":"1865-0929"},{"type":"electronic","value":"1865-0937"}],"subject":[],"published":{"date-parts":[[2008]]}}}