{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,3]],"date-time":"2026-10-03T17:21:48Z","timestamp":1791048108094,"version":"4.1.0"},"reference-count":23,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[1994,5,1]],"date-time":"1994-05-01T00:00:00Z","timestamp":767750400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Method Syst Des"],"published-print":{"date-parts":[[1994,5]]},"DOI":"10.1007\/bf01384048","type":"journal-article","created":{"date-parts":[[2005,4,2]],"date-time":"2005-04-02T06:08:07Z","timestamp":1112422087000},"page":"243-263","source":"Crossref","is-referenced-by-count":67,"title":["Assisting requirement formalization by means of natural language translation"],"prefix":"10.1007","volume":"4","author":[{"given":"A.","family":"Fantechi","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"S.","family":"Gnesi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"G.","family":"Ristori","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"M.","family":"Carenini","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"M.","family":"Vanocchi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"P.","family":"Moreschini","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"CR1","unstructured":"Allen, J.,Natural Language Understanding, Addison-Wesley Publishing Company, 1987."},{"issue":"2","key":"CR2","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.,Automatic Verification of Finite State Concurrent Systems using Temporal Logic Specifications. ACM TOPLAS, 8 (2), pp. 244?263, 1986.","journal-title":"ACM TOPLAS"},{"key":"CR3","doi-asserted-by":"crossref","unstructured":"Cleaveland, R., Steffen, B.,A Linear Time Model Checking Algorithm for the Alternation Free Modal ?-calculus, Lecture Notes in Computer Science 575, Springer-Verlag, 1991. pp. 48?58.","DOI":"10.1007\/3-540-55179-4_6"},{"key":"CR4","unstructured":"DeMillo, R.A., et al., Software Testing and Evaluation, The Benjamin\/Cummings Publishing Company Inc., 1987."},{"issue":"7","key":"CR5","doi-asserted-by":"crossref","first-page":"761","DOI":"10.1016\/0169-7552(93)90047-8","volume":"25","author":"R. Nicola De","year":"1993","unstructured":"De Nicola, R., Fantechi, A., Gnesi, S., Ristori, G.,An action-based framework for verifying logical and behavioural properties of concurrent systems, Computer Networks and ISDN Systems, 25, (7), pp. 761?778, 1993.","journal-title":"Computer Networks and ISDN Systems"},{"key":"CR6","doi-asserted-by":"crossref","unstructured":"De Nicola, R., Inverardi, P. Nesi, M.,Using Axiomatic Presentation of Behavioural Equivalences for Manipulating CCS Specifications, Lecture Notes in Computer Science 407, Springer-Verlag, 1991, pp. 54?67.","DOI":"10.1007\/3-540-52148-8_5"},{"key":"CR7","doi-asserted-by":"crossref","first-page":"407","DOI":"10.1007\/3-540-53479-2_17","volume":"469","author":"R. Nicola De","year":"1990","unstructured":"De Nicola, R., Vaandrager, F.W.,Action versus State based Logics for Transition Systems, Lecture Notes in Computer Science 469, 1990, pp. 407?419.","journal-title":"Lecture Notes in Computer Science"},{"issue":"1","key":"CR8","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"E.A. Emerson","year":"1986","unstructured":"Emerson, E.A., Halpern, J.Y.,?Sometimes? and ?Not Never? Revisited: on Branching Time versus Linear Time Temporal Logic, Journal of ACM, 33 (1), pp. 151?178, 1986.","journal-title":"Journal of ACM"},{"key":"CR9","unstructured":"Fantechi, A., Ferro, G., Gnesi, S., Ristori, G.,AMC Reference Manual, IEI Technical Report, 1993."},{"issue":"1","key":"CR10","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1145\/2455.2460","volume":"32","author":"M. Hennessy","year":"1985","unstructured":"Hennessy, M., Milner, R.,Algebraic Laws for Nondeterminism and Concurrency, Journal of ACM, 32 (1), pp. 137?161, 1985.","journal-title":"Journal of ACM"},{"key":"CR11","unstructured":"Inverardi, P., Yankelevich, D., Priami, C.,Verification of Concurrent Systems in SML, Proceedings SML Workshop, San Francisco, 1992."},{"key":"CR12","doi-asserted-by":"crossref","unstructured":"Ishihara, Y., Seki, H., Kasami, T.,A Translation Method from Natural Language Specifications into Formal Specifications Using Contextual Dependencies, Proceedings IEEE International Symposium on Requirements Engineering, 1992, pp. 232?239.","DOI":"10.1109\/ISRE.1993.324853"},{"key":"CR13","unstructured":"JACK: Just Another Concurrency toolKit. Reference Manual, IEI Technical Report, 1993."},{"issue":"2","key":"CR14","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D. Kozen","year":"1983","unstructured":"Kozen, D.,Results on the Propositional ?-calculus, Theoretical Computer Science, 27 (2), pp. 333?354. 1983.","journal-title":"Theoretical Computer Science"},{"key":"CR15","unstructured":"Madeleine, E., Vergamini, D.,AUTO: A Verification Tool for Distributed Systems Using Reduction of Finite Automata Networks, in S.T. Vuong (ed.), Formal Description Techniques, II, North-Holland, 1990, pp. 61?66."},{"key":"CR16","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.,The Anchored Version of the Temporal Framework, in Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, (de Bakker, J., de Roever, P. and Rozenberg, G. eds.) Lecture Notes in Computer Science 354, Springer-Verlag, 1989, pp. 201?284.","DOI":"10.1007\/BFb0013024"},{"key":"CR17","unstructured":"Marino, M.,A framework for the Development of Natural Language Grammars, Proceedings International Workshop on Parsing Technologies, Carnegie Mellon 1989, pp. 350?360."},{"key":"CR18","unstructured":"Marino, M.,PGDE: Process Grammar Development Environment, User Manual. AITech TR#1\/92-PGDEUM. Pisa, 1992."},{"key":"CR19","unstructured":"Matsumoto, Y., Ohno Y. (eds.),Japanese Perspectives in Software Engineering, Addison-Wesley Publishing Company, 1992."},{"key":"CR20","unstructured":"Milner, R.,Communication and Concurrency, Prentice Hall, 1989."},{"issue":"10","key":"CR21","doi-asserted-by":"crossref","first-page":"1126","DOI":"10.1109\/32.99198","volume":"17","author":"K. Miriyala","year":"1991","unstructured":"Miriyala, K., Harandi, M.T.,Automatic Derivation of Formal Software Specifications from Informal Descriptions, IEEE Transactions on Software Engineering, 17 (10), pp. 1126?1142, 1991.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"CR22","unstructured":"Reilly, R., Prodanof, I., Ferrari, G., Marino, M., Saffiotti, A., MacAogain, E., Sheehy, N.,CFID: a robust manmachine interface system, Atti del Primo Congresso dell' Associazione Italiana per l'Intelligenza Artificiale, Trento, 1989."},{"key":"CR23","doi-asserted-by":"crossref","unstructured":"Roy, V., de Simone, R.,Auto and autograph, Proceedings of Workshop on Computer Aided Verification, AMS-DIMACS, June 1990.","DOI":"10.1090\/dimacs\/003\/29"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01384048.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01384048\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01384048","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,6]],"date-time":"2020-04-06T16:30:05Z","timestamp":1586190605000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF01384048"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994,5]]},"references-count":23,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1994,5]]}},"alternative-id":["BF01384048"],"URL":"https:\/\/doi.org\/10.1007\/bf01384048","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[1994,5]]}}}