{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:59:08Z","timestamp":1762459148332},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642405600"},{"type":"electronic","value":"9783642405617"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-40561-7_5","type":"book-chapter","created":{"date-parts":[[2013,9,18]],"date-time":"2013-09-18T13:10:29Z","timestamp":1379509829000},"page":"61-75","source":"Crossref","is-referenced-by-count":1,"title":["From Extraction of Logical Specifications to Deduction-Based Formal Verification of Requirements Models"],"prefix":"10.1007","author":[{"given":"Rados\u0142aw","family":"Klimek","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"4","key":"5_CR1","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1016\/0020-0190(85)90056-0","volume":"21","author":"B. Alpern","year":"1985","unstructured":"Alpern, B., Schneider, F.B.: Defining liveness. Information Processing Letters\u00a021(4), 181\u2013185 (1985)","journal-title":"Information Processing Letters"},{"key":"5_CR2","doi-asserted-by":"crossref","unstructured":"Barrett, S., Sinnig, D., Chalin, P., Butler, G.: Merging of use case models: Semantic foundations. In: 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE 2009), pp. 182\u2013189 (2009)","DOI":"10.1109\/TASE.2009.34"},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"van Benthem, J.: Temporal Logic. In: Handbook of Logic in Artificial Intelligence and Logic Programming, vol.\u00a04, pp. 241\u2013350. Clarendon Press (1993\u20131995)","DOI":"10.1093\/oso\/9780198537915.003.0005"},{"issue":"4","key":"5_CR4","doi-asserted-by":"crossref","first-page":"212","DOI":"10.17705\/1jais.00225","volume":"11","author":"S. Chakraborty","year":"2010","unstructured":"Chakraborty, S., Sarker, S., Sarker, S.: An exploration into the process of requirements elicitation: A grounded approach. Journal of the Association for Information Systems\u00a011(4), 212\u2013249 (2010)","journal-title":"Journal of the Association for Information Systems"},{"issue":"4","key":"5_CR5","doi-asserted-by":"publisher","first-page":"626","DOI":"10.1145\/242223.242257","volume":"28","author":"E. Clarke","year":"1996","unstructured":"Clarke, E., Wing, J., et al.: Formal methods: State of the art and future directions. ACM Computing Surveys\u00a028(4), 626\u2013643 (1996)","journal-title":"ACM Computing Surveys"},{"key":"5_CR6","doi-asserted-by":"crossref","unstructured":"d\u2019Agostino, M., Gabbay, D., H\u00e4hnle, R., Posegga, J.: Handbook of Tableau Methods. Kluwer Academic Publishers (1999)","DOI":"10.1007\/978-94-017-1754-0"},{"key":"5_CR7","doi-asserted-by":"crossref","unstructured":"Emerson, E.: Temporal and Modal Logic. In: Handbook of Theoretical Computer Science, vol.\u00a0B, pp. 995\u20131072. Elsevier, MIT Press (1990)","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"issue":"7","key":"5_CR8","doi-asserted-by":"publisher","first-page":"437","DOI":"10.1109\/TSE.2004.33","volume":"30","author":"R. Eshuis","year":"2004","unstructured":"Eshuis, R., Wieringa, R.: Tool support for verifying uml activity diagrams. IEEE Transactions on Software Engineering\u00a030(7), 437\u2013447 (2004)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"5_CR9","unstructured":"H\u00e4hnle, R.: Tableau-based Theorem Proving. ESSLLI Course (1998)"},{"key":"5_CR10","unstructured":"Hurlbut, R.R.: A survey of approaches for describing and formalizing use cases. Tech. Rep. XPT-TR-97-03, Expertech, Ltd. (1997)"},{"key":"5_CR11","unstructured":"Kazhamiakin, R., Pistore, M., Roveri, M.: Formal verification of requirements using spin: A case study on web services. In: Proceedings of 2nd International Conference on Software Engineering and Formal Methods (SEFM 2004), Beijing, China, pp. 406\u2013415 (September 28-30, 2004)"},{"key":"5_CR12","unstructured":"Klimek, R.: Proposal to improve the requirements process through formal verification using deductive approach. In: Filipe, J., Maciaszek, L. (eds.) Proceedings of 7th Int. Conf. on Evaluation of Novel Approaches to Software Engineering (ENASE 2012), Wroc\u0142aw, Poland. pp. 105\u2013114. SciTePress (June 29\u201330, 2012)"},{"key":"5_CR13","unstructured":"Klimek, R.: A Deduction-based System for Formal Verification of Agent-ready Web Services. In: Advanced Methods and Technologies for Agent and Multi-Agent Systems, Frontiers of Artificial Intelligence and Applications, vol.\u00a0252, pp. 203\u2013212. IOS Press (2013), http:\/\/ebooks.iospress.nl\/publication\/32843"},{"key":"5_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"887","DOI":"10.1007\/11758532_116","volume-title":"Computational Science \u2013 ICCS 2006","author":"L. Kotulski","year":"2006","unstructured":"Kotulski, L.: Supporting software agents by the graph transformation systems. In: Alexandrov, V.N., van Albada, G.D., Sloot, P.M.A., Dongarra, J. (eds.) ICCS 2006. LNCS, vol.\u00a03993, pp. 887\u2013890. Springer, Heidelberg (2006)"},{"key":"5_CR15","unstructured":"van Lamsweerde, A.: Requirements Engineering - From System Goals to UML Models to Software Specifications. John Wiley & Sons (2009)"},{"key":"5_CR16","unstructured":"Pender, T.: UML Bible. John Wiley & Sons (2003)"},{"key":"5_CR17","doi-asserted-by":"crossref","unstructured":"Rauf, R., Antkiewicz, M., Czarnecki, K.: Logical structure extraction from software requirements documents. In: 19th IEEE International Requirements Engineering Conference (RE 2011), Trento, Italy, August 29-September 2, pp. 101\u2013110. IEEE Computer Society (2011)","DOI":"10.1109\/RE.2011.6051638"},{"key":"5_CR18","unstructured":"Schneider, G., Winters, J.: Applying use cases: a practical guide. Addison-Wesley (2001)"},{"issue":"1","key":"5_CR19","first-page":"249","volume":"XXVII","author":"F. Wolter","year":"2011","unstructured":"Wolter, F., Wooldridge, M.: Temporal and dynamic logic. Journal of Indian Council of Philosophical Research\u00a0XXVII(1), 249\u2013276 (2011)","journal-title":"Journal of Indian Council of Philosophical Research"},{"key":"5_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1007\/978-3-642-02457-3_3","volume-title":"Computational Science and Its Applications \u2013 ICCSA 2009","author":"J. Zhao","year":"2009","unstructured":"Zhao, J., Duan, Z.: Verification of use case with petri nets in requirement analysis. In: Gervasi, O., Taniar, D., Murgante, B., Lagan\u00e0, A., Mun, Y., Gavrilova, M.L. (eds.) ICCSA 2009, Part II. LNCS, vol.\u00a05593, pp. 29\u201342. Springer, Heidelberg (2009)"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-40561-7_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,5,17]],"date-time":"2024-05-17T23:17:52Z","timestamp":1715987872000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-40561-7_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642405600","9783642405617"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-40561-7_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}