{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,21]],"date-time":"2026-06-21T04:19:07Z","timestamp":1782015547687,"version":"3.54.5"},"reference-count":42,"publisher":"Association for Computing Machinery (ACM)","issue":"5","license":[{"start":{"date-parts":[[2016,9,1]],"date-time":"2016-09-01T00:00:00Z","timestamp":1472688000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2016,9]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>At the very beginning of system development, typically only natural-language requirements are documented. As an informal source of information, however, natural-language specifications may be ambiguous and incomplete; this can be hard to detect by means of manual inspection. In this work, we present a formal model, named data-flow reactive system (DFRS), which can be automatically obtained from natural-language requirements that describe functional, reactive and temporal properties. A DFRS can also be used to assess whether the requirements are consistent and complete. We define two variations of DFRS: a symbolic and an expanded version. A symbolic DFRS (s-DFRS) is a concise representation that inherently avoids an explicit representation of (possibly infinite) sets of states and, thus, the state space-explosion problem. We use s-DFRS as part of a technique for test-case generation from natural-language requirements. In our approach, an expanded DFRS (e-DFRS) is built dynamically from a symbolic one, possibly limited to some bound; in this way, bounded analysis (e.g., reachability, determinism, completeness) can be performed. We adopt the s-DFRS as an intermediary representation from which models, for instance, SCR and CSP, are obtained for the purpose of test generation. An e-DFRS can also be viewed as the semantics of the s-DFRS from which it is generated. In order to connect such a semantic representation to established ones in the literature, we show that an e-DFRS can be encoded as a TIOTS: an alternative timed model based on the widely used IOLTS and ioco. To validate our overall approach, we consider two toy examples and two examples from the aerospace and automotive industry. Test cases are independently created and we verify that they are all compatible with the corresponding e-DFRS models generated from symbolic ones. This verification is performed mechanically with the aid of the NAT2TEST tool, which supports the manipulation of such models.<\/jats:p>","DOI":"10.1007\/s00165-016-0387-x","type":"journal-article","created":{"date-parts":[[2016,7,26]],"date-time":"2016-07-26T09:42:29Z","timestamp":1469526149000},"page":"725-765","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":16,"title":["Modelling timed reactive systems from natural-language requirements"],"prefix":"10.1145","volume":"28","author":[{"given":"Gustavo","family":"Carvalho","sequence":"first","affiliation":[{"name":"Centro de Inform\u00e1tica, Universidade Federal de Pernambuco, 50740-560, Recife, Brazil"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ana","family":"Cavalcanti","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of York, YO10 5GH, York, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Augusto","family":"Sampaio","sequence":"additional","affiliation":[{"name":"Centro de Inform\u00e1tica, Universidade Federal de Pernambuco, 50740-560, Recife, Brazil"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1002\/stvr.1522"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Aceituna D Do H Srinivasan S (2014) A systematic approach to transforming system requirements into model checking specifications. In: Companion Proceedings of the 36th International Conference on Software Engineering ICSE Companion 2014. ACM New York pp 165\u2013174","DOI":"10.1145\/2591062.2591183"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10515-006-5468-2"},{"key":"e_1_2_1_2_5_2","unstructured":"Allen J (1995) Natural language understanding. Benjamin\/Cummings Redwood City"},{"key":"e_1_2_1_2_6_2","unstructured":"Blackburn M Busser R Fontaine J (1997) Automatic Generation of Test Vectors for SCR-style Specifications. In: Annual conference on computer assurance"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Backes J Cofer D Miller S Whalen MW (2015) Requirements analysis of a quad-redundant flight control system. In: Havelund K Holzmann G Joshi R (eds) NASA formal methods Lecture notes in computer science vol 9058. Springer International Publishing Pasadena pp 82\u201396","DOI":"10.1007\/978-3-319-17524-9_7"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Bucchiarone A Gnesi S Fantechi A Trentanni G (2010) An experience in using a tool for evaluating a large set of natural language requirements. In: Proceedings of the 2010 ACM symposium on applied computing SAC \u201910. ACM New York pp 281\u2013286","DOI":"10.1145\/1774088.1774148"},{"key":"e_1_2_1_2_9_2","unstructured":"Boddu R Guo L Mukhopadhyay S Cukic B (2004) RETNA: from requirements to testing in a natural way. In: IEEE International requirements engineering conference pp 262\u2013271"},{"key":"e_1_2_1_2_10_2","unstructured":"Carvalho G (2016) NAT2TEST: generating test cases from natural language requirements based on CSP. PhD thesis Centro de Inform\u00e1tica Universidade Federal de Pernambuco (UFPE) Brazil"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Carvalho G Barros F Carvalho A Cavalcanti A Mota A Sampaio A (2015) NAT2TEST Tool: from Natural Language Requirements to Test Cases based on CSP. In: International conference on software engineering and formal methods. Springer International Publishing Cham","DOI":"10.1007\/978-3-319-22969-0_20"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Carvalho G Barros F Lapschies F Schulze U Peleska J (2014) Model-Based Testing from Controlled Natural Language Requirements. In: Artho C \u00d6lveczky PC (eds) Formal techniques for safety-critical systems Communications in computer and information science vol 419. Springer International Publishing Cham pp 19\u201335","DOI":"10.1007\/978-3-319-05416-2_3"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Cimatti A Clarke EM Giunchiglia F Roveri M (1999) NuSMV: a new symbolic model verifier. In: Proceedings of the 11th international conference on computer aided verification CAV \u201999. Springer-Verlag London pp 495\u2013499","DOI":"10.1007\/3-540-48683-6_44"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Carvalho G Carvalho A Rocha E Cavalcanti A Sampaio A (2014) A formal model for natural-language timed requirements of reactive systems. In: Merz S Pang J (eds) Formal methods and software engineering international conference on formal engineering methods ICFEM Lecture notes in computer science vol 8829. Springer International Publishing Cham pp 43\u201358","DOI":"10.1007\/978-3-319-11737-9_4"},{"key":"e_1_2_1_2_15_2","unstructured":"Carvalho G Cavalcanti A Sampaio A (2015) DFRS: definition and proofs. Technical report Universidade Federal de Pernambuco"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Carvalho G Falc\u00e3o D Barros F Sampaio A Mota A Motta L Blackburn M (2013) Test case generation from natural language requirements based on SCR specifications. In: Symposium on applied computing vol 2 pp 1217\u20131222","DOI":"10.1145\/2480362.2480591"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Carvalho G Falc\u00e3o D Barros F Sampaio A Mota A Motta L Blackburn M (2014) NAT2TEST SCR : test case generation from natural language requirements based on SCR specifications. Sci Comput Program 95(Part 3(0)):275\u2013297","DOI":"10.1016\/j.scico.2014.06.007"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Carvalho G Sampaio A Mota A (2013) A CSP timed input-output relation and a strategy for mechanised conformance verification. In: Formal methods and software engineering LNCS vol 8144. Springer Berlin Heidelberg pp 148\u2013164","DOI":"10.1007\/978-3-642-41202-8_11"},{"key":"e_1_2_1_2_19_2","unstructured":"Esser M Struss P (2007) Obtaining models for test generation from natural-language like functional specifications. In: International workshop on principles of diagnosis pp 75\u201382"},{"key":"e_1_2_1_2_20_2","unstructured":"FAA (2009) Requirements engineering management findings report. Technical report U.S. Department of Transportation-Federal Aviation Administration"},{"key":"e_1_2_1_2_21_2","unstructured":"Fillmore CJ (1968) The case for case. In: Bach Harms (eds) Universals in linguistic theory. Holt Rinehart and Winston New York pp 1\u201388"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Ferrari A Lipari G Gnesi S Spagnolo GO (2014) Pragmatic ambiguity detection in natural language requirements. In: Artificial intelligence for requirements engineering (AIRE) 2014 IEEE 1st International Workshop on pp 1\u20138","DOI":"10.1109\/AIRE.2014.6894849"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Ilic D (2007) Deriving formal specifications from informal requirements. In: Computer software and applications conference 2007. COMPSAC 2007. 31st Annual International vol 1 pp 145\u2013152","DOI":"10.1109\/COMPSAC.2007.104"},{"key":"e_1_2_1_2_24_2","unstructured":"ISO (2002) Z formal specification notation (ISO\/IEC 13568). Technical report International Organization for Standardization"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.738342"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1023072104553"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.317428"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"Larsen K Mikucionis M Nielsen B (2004) Online testing of real-time systems using uppaal: status and future work. In: Perspectives of model-based testing\u2014Dagstuhl Seminar vol 04371","DOI":"10.1007\/978-3-540-31848-4_6"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Liu S Sun J Liu Y Zhang Y Wadhwa B Dong JS Wang X (2014) Automatic early defects detection in use case documents. In: Proceedings of the 29th ACM\/IEEE international conference on automated software engineering ASE \u201914. ACM New York pp 785\u2013790","DOI":"10.1145\/2642937.2642969"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"Miller SP Tribble AC Whalen MW Heimdahl MPE (2006) Proving the shalls. Int J Softw Tools Technol Transf 8(4\u20135):303\u2013319","DOI":"10.1007\/s10009-004-0173-6"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-012-0258-z"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"crossref","unstructured":"Owre S Rushby JM Shankar N (1992) PVS: A prototype verification system. In: Kapur D (ed) 11th International Conference On Automated Deduction (CADE) Lecture notes in artificial intelligence vol 607. Springer-Verlag Saratoga pp 748\u2013752","DOI":"10.1007\/3-540-55602-8_217"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"crossref","unstructured":"Peleska J et\u00a0al (2011) A real-world benchmark model for testing concurrent real-time systems in the automotive domain. In: Proceedings of the ICTSS ICTSS\u201911. Springer-Verlag Berlin Heidelberg pp 146\u2013161","DOI":"10.1007\/978-3-642-24580-0_11"},{"key":"e_1_2_1_2_34_2","unstructured":"Peleska J Vorobev E Lapschies F Zahlten C (2011) Automated model-based testing with RT-Tester. Technical report Universit\u00e4t Bremen"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"crossref","unstructured":"Roscoe AW (2010) Understanding concurrent systems. Springer London","DOI":"10.1007\/978-1-84882-258-0"},{"key":"e_1_2_1_2_36_2","unstructured":"Schwitter R (2002) English as a formal specification language. In: Proceedings of the 13th international workshop on database and expert systems applications"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"crossref","unstructured":"Schnelte M (2009) Generating test cases for timed systems from controlled natural language specifications. In: International conference on system integration and reliability improvements pp 348\u2013353","DOI":"10.1109\/SSIRI.2009.58"},{"key":"#cr-split#-e_1_2_1_2_38_2.1","doi-asserted-by":"crossref","unstructured":"Siegl S Hielscher K-S German R (2010) Model based requirements analysis and testing of automotive systems with timed usage models. In: Requirements engineering conference","DOI":"10.1109\/ICVES.2010.5550938"},{"key":"#cr-split#-e_1_2_1_2_38_2.2","unstructured":"(RE) 2010 18th IEEE International pp 345-350"},{"key":"e_1_2_1_2_39_2","doi-asserted-by":"publisher","DOI":"10.1007\/s11219-011-9155-6"},{"key":"e_1_2_1_2_40_2","doi-asserted-by":"crossref","unstructured":"39. Sun J Liu Y Dong JS Pang J Pat: (2009) Towards flexible verification under fairness Lecture Notes in Computer Science vol 5643. Springer Heidelberg pp 709\u2013714","DOI":"10.1007\/978-3-642-02658-4_59"},{"key":"e_1_2_1_2_41_2","doi-asserted-by":"crossref","unstructured":"40. Tretmans J (1999) Testing concurrent systems: a formal approach. In: Proceedings of CONCUR. Springer-Verlag London pp 46\u201365","DOI":"10.1007\/3-540-48320-9_6"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-016-0387-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-016-0387-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-016-0387-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T16:16:49Z","timestamp":1641485809000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-016-0387-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,9]]},"references-count":42,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2016,9]]}},"alternative-id":["10.1007\/s00165-016-0387-x"],"URL":"https:\/\/doi.org\/10.1007\/s00165-016-0387-x","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,9]]}}}