{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,21]],"date-time":"2026-02-21T04:22:13Z","timestamp":1771647733677,"version":"3.50.1"},"reference-count":52,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2019,6,21]],"date-time":"2019-06-21T00:00:00Z","timestamp":1561075200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2019,6,21]],"date-time":"2019-06-21T00:00:00Z","timestamp":1561075200000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Requirements Eng"],"published-print":{"date-parts":[[2019,9]]},"DOI":"10.1007\/s00766-019-00316-x","type":"journal-article","created":{"date-parts":[[2019,6,21]],"date-time":"2019-06-21T02:02:45Z","timestamp":1561082565000},"page":"341-364","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":18,"title":["Automating requirements analysis and test case generation"],"prefix":"10.1007","volume":"24","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7027-2082","authenticated-orcid":false,"given":"Abha","family":"Moitra","sequence":"first","affiliation":[]},{"given":"Kit","family":"Siu","sequence":"additional","affiliation":[]},{"given":"Andrew W.","family":"Crapo","sequence":"additional","affiliation":[]},{"given":"Michael","family":"Durling","sequence":"additional","affiliation":[]},{"given":"Meng","family":"Li","sequence":"additional","affiliation":[]},{"given":"Panagiotis","family":"Manolios","sequence":"additional","affiliation":[]},{"given":"Michael","family":"Meiners","sequence":"additional","affiliation":[]},{"given":"Craig","family":"McMillan","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,6,21]]},"reference":[{"key":"316_CR1","doi-asserted-by":"crossref","unstructured":"Siu K, Moitra A, Durling M, Crapo A, Li M, Yu H, Herencia-zapana H, Castillo-Effen M, Sen S, McMillan C, Manolios P (2017) Flight critical software and systems development using ASSERT\u2122. In: IEEE\/AIAA 36th digital avionics systems conference (DASC), St. Petersburg, FL, USA","DOI":"10.1109\/DASC.2017.8102059"},{"key":"316_CR2","doi-asserted-by":"crossref","unstructured":"Crapo A, Moitra A, McMillan C, Russell D (2017) Requirements capture and analysis in ASSERT\u2122. In: IEEE 25th international requirements engineering conference (RE), Lisbon, Portugal","DOI":"10.1109\/RE.2017.54"},{"key":"316_CR3","doi-asserted-by":"crossref","unstructured":"Moitra A, Siu K, Crapo AW, Chamarti H, Durling M, Li M, Yu H, Manolios P, Meiners M (2018) Towards development of complete and conflict-free requirements. In: IEEE 26th international requirements engineering conference (RE), Banff, Canada","DOI":"10.1109\/RE.2018.00036"},{"key":"316_CR4","doi-asserted-by":"crossref","unstructured":"McMillan C, Crapo A, Durling M, Li M, Moitra A, Manolios P, Stephens M, Russell D (2019) Increasing development assurance for system and software development with validation and verification using ASSERT\u2122. In: SAE technical paper no. 2019-01-1370","DOI":"10.4271\/2019-01-1370"},{"key":"316_CR5","unstructured":"RTCA (2011) DO-178C software considerations in airborne systems and equipment certification 12\/13\/2011"},{"key":"316_CR6","doi-asserted-by":"crossref","unstructured":"Owre S, Rushby J, Shankar N (1992) PVS: a prototype verification system. In: International conference on automated deduction, Springer, Berlin","DOI":"10.1007\/3-540-55602-8_217"},{"key":"316_CR7","unstructured":"PVS: property verification system. \n                              http:\/\/www.csl.sri.com\/projects\/pvs\n                              \n                           . Accessed 3 May 2019"},{"key":"316_CR8","unstructured":"Heimdahl MPK, Czerny BJ (1996) Using PVS to analyze hierarchical state-based requirements for completeness and consistency. In: IEEE high-assurance systems engineering workshop (Cat. No. 96TB100076)"},{"key":"316_CR9","unstructured":"Owre S, Rushby J, Shankar N (1995) Analyzing tabular and state-transition requirements specifications in PVS. In: Proceedings of TACAS"},{"key":"316_CR10","doi-asserted-by":"crossref","unstructured":"Rayadurgam S, Joshi A, Heimdahl M (2003) Using PVS to prove properties of systems modelled in a synchronous dataflow language. In: International conference on formal engineering methods","DOI":"10.1007\/978-3-540-39893-6_11"},{"key":"316_CR11","doi-asserted-by":"crossref","unstructured":"Leveson N, Heimdahl M, Hildreth H, Reese J (1994) Requirements specification for process-control systems. In: IEEE transaction on software engineering","DOI":"10.1109\/32.317428"},{"key":"316_CR12","doi-asserted-by":"crossref","unstructured":"Leveson N, Heimdahl M, Reese J (1999) Designing specification languages for process control systems: lessons learned and steps to the future. In: Nierstrasz O, Lemoine M (eds) Software engineering\u2014ESEC\/FSE\u201999. Lecture notes in computer science, vol 1687, Springer, Berlin","DOI":"10.1007\/3-540-48166-4_9"},{"issue":"1","key":"316_CR13","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1109\/32.663994","volume":"24","author":"S Easterbrook","year":"1998","unstructured":"Easterbrook S, Lutz R, Covington R, Kelly J, Ampo Y, Hamilton D (1998) Experiences using lightweight formal methods for requirements modeling. IEEE Trans Softw Eng 24(1):4\u201314","journal-title":"IEEE Trans Softw Eng"},{"key":"316_CR14","volume-title":"Design and validation of computer protocols","author":"GJ Holtzmann","year":"1991","unstructured":"Holtzmann GJ, Lieberman WS (1991) Design and validation of computer protocols. Prentice Hall, Englewood Cliffs"},{"key":"316_CR15","doi-asserted-by":"publisher","first-page":"10","DOI":"10.1016\/S1571-0661(04)00127-6","volume":"25","author":"D Berry","year":"1999","unstructured":"Berry D (1999) Formal methods: the very idea, some thought about why they work when they work. Electron Notes Theor Comput Sci 25:10\u201322","journal-title":"Electron Notes Theor Comput Sci"},{"key":"316_CR16","doi-asserted-by":"crossref","unstructured":"Nuseibeh B, Easterbrook S (2000) Requirements engineering: a roadmap. In: Proceedings of the conference on the future of software engineering, ACM","DOI":"10.1145\/336512.336523"},{"key":"316_CR17","doi-asserted-by":"crossref","unstructured":"Mavin A, Wilkinson P, Harwood A, Novak M (2009) Easy approach to requirements syntax (EARS). In: 17th IEEE international requirements engineering conference, Atlanta, USA","DOI":"10.1109\/RE.2009.9"},{"key":"316_CR18","doi-asserted-by":"crossref","unstructured":"Mavin A, Wilkinson P, Gregory S, Uusitalo E (2016) Listens learned (8 lessons learned applying EARS). In: IEEE 24th international requirements engineering conference, Beijing, China","DOI":"10.1109\/RE.2016.38"},{"key":"316_CR19","doi-asserted-by":"crossref","unstructured":"Badger J, Throop D, Claunch C (2014) VARED verification and analysis of requirements and early designs. In: IEEE 22nd requirements engineering conference, Karlskrona, Sweden","DOI":"10.1109\/RE.2014.6912279"},{"key":"316_CR20","doi-asserted-by":"crossref","unstructured":"Gross K, Fifarek A, Hoffman J (2016) Incremental formal methods based design approach demonstrated on a coupled tank control system. In: IEEE 17th international symposium on high assurance systems engineering","DOI":"10.1109\/HASE.2016.16"},{"key":"316_CR21","unstructured":"GitHub SpeAR. \n                              https:\/\/github.com\/lgwagner\/SpeAR\n                              \n                           . Accessed 3 May 2019"},{"key":"316_CR22","doi-asserted-by":"crossref","unstructured":"Feiler PH, Gluch DP, Hudak JJ (2006) The architecture analysis and design language (AADL): an introduction (no. CMU\/SEI-2006-TN-011). Carnegie-Mellon Univ Pittsburgh PA Software Engineering Inst","DOI":"10.21236\/ADA455842"},{"key":"316_CR23","doi-asserted-by":"crossref","unstructured":"Brat G, Bushnell D, Davies M, Giannakopoulou D, Howar F, Kahsai T (2015) Verifying the safety of a flight-critical system. In: International symposium on formal methods, Springer, Cham","DOI":"10.1007\/978-3-319-19249-9_20"},{"key":"316_CR24","unstructured":"W3C: Semantic Web Standards. Web Ontology Language (OWL). \n                              https:\/\/www.w3.org\/OWL\/\n                              \n                           . Accessed 3 May 2019"},{"key":"316_CR25","doi-asserted-by":"crossref","unstructured":"Crapo A, Moitra A (2019) Using OWL ontologies as a domain-specific language for capturing requirements for formal analysis and test case generation. In: International conference on semantic computing, Newport Beach","DOI":"10.1109\/ICOSC.2019.8665630"},{"key":"316_CR26","doi-asserted-by":"crossref","unstructured":"Whalen M, Gacek A, Cofer D, Murugesan A, Heimdahl M, Rayadurgam S (2013) Your \u201cwhat\u201d is my \u201chow\u201d: iteration and hierarchy in system design. IEEE software, vol 30, no 2","DOI":"10.1109\/MS.2012.173"},{"key":"316_CR27","unstructured":"Some Famous Unit Conversion Errors. \n                              https:\/\/spacemath.gsfc.nasa.gov\/weekly\/6Page53.pdf\n                              \n                           . Accessed 3 May 2019"},{"issue":"3","key":"316_CR28","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1109\/MS.1997.589224","volume":"14","author":"B Nuseibeh","year":"1997","unstructured":"Nuseibeh B (1997) Ariane 5: who dunnit? IEEE Softw 14(3):15\u201316","journal-title":"IEEE Softw"},{"issue":"12","key":"316_CR29","doi-asserted-by":"publisher","first-page":"543","DOI":"10.2514\/1.13048","volume":"1","author":"J Litt","year":"2004","unstructured":"Litt J, Simon D, Garg S, Guo TH, Mercer C, Millar R, Behbahani A, Bajwa A, Jensen DT (2004) A survey of intelligent control and health management technologies for aircraft propulsion systems. JACIC 1(12):543\u2013563","journal-title":"JACIC"},{"key":"316_CR30","unstructured":"Semantic Application Design Language (SADL). \n                              http:\/\/sadl.sourceforge.net\/index.html\n                              \n                           . Accessed 3 May 2019"},{"issue":"3","key":"316_CR31","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1142\/S1793351X13500025","volume":"7","author":"A Crapo","year":"2013","unstructured":"Crapo A, Moitra A (2013) Toward a unified English-like representation of semantic models, data, and graph patterns for subject matter experts. Int J Semant Comput 7(3):215\u2013236","journal-title":"Int J Semant Comput"},{"issue":"7","key":"316_CR32","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1109\/2.56851","volume":"23","author":"JC Laprie","year":"1990","unstructured":"Laprie JC, Arlat J, Beounes C, Kanoun K (1990) Definition and analysis of hardware- and software-fault-tolerant architectures. Computer 23(7):39\u201351","journal-title":"Computer"},{"key":"316_CR33","unstructured":"IBM Rational DOORS. \n                              https:\/\/www.ibm.com\/us-en\/marketplace\/rational-doors\n                              \n                           . Accessed 3 May 2019"},{"key":"316_CR34","unstructured":"Manolios P (2017) Scalable methods for analyzing formalized requirements and localizing errors. Patent 9,639,450, 2 May 2017"},{"key":"316_CR35","doi-asserted-by":"crossref","unstructured":"Chamarthi HR, Dillinger PC, Manolios P, Vroon D (2011) The ACL2 Sedan theorem proving system. In: TACAS, Springer","DOI":"10.1007\/978-3-642-19835-9_27"},{"key":"316_CR36","doi-asserted-by":"crossref","unstructured":"Manolios P, Vroon D (2006) Termination analysis with calling context graphs. In: Computer aided verification (CAV). Lecture notes in computer science, Springer, vol 4144, pp 401\u2013414","DOI":"10.1007\/11817963_36"},{"key":"316_CR37","doi-asserted-by":"crossref","unstructured":"Manolios P, Vroon D (2010) Interactive termination proofs using termination cores. In: Interactive theorem proving, lecture notes in computer science, Springer, vol 6172","DOI":"10.1007\/978-3-642-14052-5_25"},{"key":"316_CR38","doi-asserted-by":"crossref","unstructured":"Chamarthi HR, Dillinger PC, Kaufmann M, Manolios P (2011) Integrating testing and interactive theorem proving. In: ACL2 2011, EPTCS 70, pp 4\u201319","DOI":"10.4204\/EPTCS.70.1"},{"key":"316_CR39","doi-asserted-by":"crossref","unstructured":"Chamarthi HR, Manolios P (2011) Automated specification analysis using an interactive theorem prover. In: FMCAD","DOI":"10.4204\/EPTCS.70.1"},{"key":"316_CR40","doi-asserted-by":"crossref","unstructured":"Chamarthi HR, Dillinger PC, Manolios P (2014) Data definitions in the ACL2 Sedan. In: ACL2","DOI":"10.4204\/EPTCS.152.3"},{"key":"316_CR41","unstructured":"ACL2 Tutorial. \n                              http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/v7-4\/combined-manual\/\n                              \n                           . Accessed 3 May 2019"},{"key":"316_CR42","volume-title":"Computer-aided reasoning: an approach","author":"J Moore","year":"2000","unstructured":"Moore J, Kaufmann M, Manolios P (2000) Computer-aided reasoning: an approach. Kluwer, Dordrecht"},{"key":"316_CR43","unstructured":"Li M (2014) Integrated automated test case generation for safety-critical software. Patent U.S. Patent Application 20160170864A1, filed December 2014"},{"key":"316_CR44","unstructured":"Li M, Durling M, Siu K, Oliveira I, Yu H, De Conto A (2018) System and method for safety-critical software automated requirements-based test case generation. Patent 9,940,222, 10 Apr 2018"},{"key":"316_CR45","unstructured":"De Conto A, Li M, Manolios P, Oliveira I (2016) System and method for equivalence class analysis-based automated requirements-based test case generation. Patent U.S. Patent Application 20170228309A1, filed February 2016"},{"key":"316_CR46","doi-asserted-by":"crossref","unstructured":"Durrieu G, Laurent O, Seguin C, Wiels V (2004) Formal proof and test case generation for critical embedded systems using SCADE. In: Jacquart R (ed) Building the information society, Springer, Boston, MA, vol 156, pp 499\u2013504","DOI":"10.1007\/978-1-4020-8157-6_44"},{"key":"316_CR47","unstructured":"Wiels V, Delmas R, Doose D, Garoche PL, Cazin J, Durrieu G (2012) Formal verification of critical aerospace software. In: Aerospace Lab"},{"key":"316_CR48","doi-asserted-by":"crossref","unstructured":"Bochot T, Virelizier P, Waeselynck H, Wiels V (2009) Model checking flight control systems: the Airbus experience. In: International conference on software engineering","DOI":"10.1109\/ICSE-COMPANION.2009.5070960"},{"key":"316_CR49","unstructured":"ANSYS SCADE Suite. \n                              https:\/\/www.ansys.com\/products\/embedded-software\/ansys-scade-suite\n                              \n                           . Accessed 3 May 2019"},{"key":"316_CR50","unstructured":"Z3. \n                              https:\/\/github.com\/Z3Prover\/z3\n                              \n                           . Accessed 3 May 2019"},{"key":"316_CR51","unstructured":"dReal. dreal.github.io\/. Accessed 3 May 2019"},{"key":"316_CR52","unstructured":"Federal Aviation Administration (2001) Rationale for accepting masking MC\/DC in certification projects. Certification Authorities Software Team, Position Paper, CAST-6"}],"container-title":["Requirements Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00766-019-00316-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00766-019-00316-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00766-019-00316-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,19]],"date-time":"2020-06-19T23:16:56Z","timestamp":1592608616000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00766-019-00316-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,6,21]]},"references-count":52,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2019,9]]}},"alternative-id":["316"],"URL":"https:\/\/doi.org\/10.1007\/s00766-019-00316-x","relation":{},"ISSN":["0947-3602","1432-010X"],"issn-type":[{"value":"0947-3602","type":"print"},{"value":"1432-010X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,6,21]]},"assertion":[{"value":"11 December 2018","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"5 June 2019","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"21 June 2019","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}