{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,5,6]],"date-time":"2022-05-06T10:41:38Z","timestamp":1651833698541},"reference-count":29,"publisher":"IGI Global","issue":"3","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018,7]]},"abstract":"Requirement specification is a key element in model-checking verification. The context-aware approach is an effective technique for automating the specification of requirement considering specific environmental conditions. In most of existing approaches, there is no support of this crucial task and are mainly based on the considerable efforts and expertise of engineers. A domain-specific language, called CDL, has been proposed to facilitate the specification of requirement by formalizing contexts. However, the feedback has shown that manually writing CDL is hard, error prone and difficult to grasp on complex systems. In this article, the authors propose an approach to automatically generate CDL models using (IODs) elaborated through transformation chains from textual use cases. They offer an intermediate formalism between informal use cases scenarios and CDL models allowing to engineers to manipulate with familiar artifacts. Thanks to such high-level formalism, the gap between informal and formal requirements is reduced; consequently, the requirement specification is facilitated.<\/jats:p>","DOI":"10.4018\/ijismd.2018070102","type":"journal-article","created":{"date-parts":[[2018,11,13]],"date-time":"2018-11-13T01:10:20Z","timestamp":1542071420000},"page":"23-47","source":"Crossref","is-referenced-by-count":0,"title":["Automated Context Formalization for Context-aware Specification Approach"],"prefix":"10.4018","volume":"9","author":[{"given":"Amel","family":"Benabbou","sequence":"first","affiliation":[{"name":"Litio Laboratory, University Oran1 Ahmed Ben Bella, Oran, Algeria"}]},{"given":"Safia","family":"Nait-Bahloul","sequence":"additional","affiliation":[{"name":"Litio Laboratory, University Oran1 Ahmed Ben Bella, Oran, Algeria"}]}],"member":"2432","reference":[{"key":"IJISMD.2018070102-0","doi-asserted-by":"publisher","DOI":"10.1007\/11518358_12"},{"key":"IJISMD.2018070102-1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_60"},{"key":"IJISMD.2018070102-2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02574-7_65"},{"key":"IJISMD.2018070102-3","unstructured":"Berthomieu, B., Bodeveix, J. P., Farail, P., Filali, M., Garavel, H., Gaullet, P., . . . Vernadat, F. (2008). Fiacre: an Intermediate Language for Model Verification in the Topcased Environment. Paper presented at European Congress Embedded Real Time Software And Systems 2008, Toulouse, France."},{"issue":"7","key":"IJISMD.2018070102-4","first-page":"35","article-title":"Structuring use cases with goals.","volume":"10","author":"A.Cockburn","year":"1997","journal-title":"Journal of Object-Oriented Programming"},{"key":"IJISMD.2018070102-5","doi-asserted-by":"crossref","unstructured":"Dhaussy, P., Boniol, F., Roger, J. C., & Leroux, L. (2012). Improving model checking with context modeling. Journal of Advances in Software Engineering.","DOI":"10.1155\/2012\/547157"},{"key":"IJISMD.2018070102-6","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04425-0_34"},{"key":"IJISMD.2018070102-7","unstructured":"Dhaussy, P., & Roger, J. (2011). CDL (Context Description Language): Syntax and Semantics (Technical report). ENSTA Bretagne."},{"key":"IJISMD.2018070102-8","first-page":"155","article-title":"Parallelizing the Spin Model Checker.","author":"J.Gerard","year":"2012","journal-title":"Proceedings of the 19th international conference on Model Checking Software"},{"key":"IJISMD.2018070102-9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87875-9_6"},{"key":"IJISMD.2018070102-10","doi-asserted-by":"crossref","unstructured":"Haugen, O., Husa, K. E., Runde, R. K., & Stolen, K. (2005). Stairs: Towards formal design with sequence diagrams. Journal of Software and System Modeling, 4(4), 355-367","DOI":"10.1007\/s10270-005-0087-0"},{"key":"IJISMD.2018070102-11","doi-asserted-by":"crossref","unstructured":"Hassan, Z., Aaron, R., & Somenzi, F. (2012). Incremental, Inductive CTL Model Checking. In Proceedings of the 24th international conference on Computer Aided, Berkeley, CA (pp. 532-547).","DOI":"10.1007\/978-3-642-31424-7_38"},{"key":"IJISMD.2018070102-12"},{"key":"IJISMD.2018070102-13"},{"key":"IJISMD.2018070102-14","unstructured":"Eclipse software. (n.d.). Model To Text (M2T) plug-in. Retrieved from http:\/\/www.eclipse.org\/modeling\/m2t\/?project=xpand"},{"key":"IJISMD.2018070102-15","unstructured":"UML designer. (n.d.). Retrieved from http:\/\/www.umldesigner.org\/"},{"key":"IJISMD.2018070102-16","unstructured":"Language and Tools set website. (n.d.). Retrieved from http:\/\/www.obpcdl.org"},{"key":"IJISMD.2018070102-17","first-page":"1","article-title":"Invited address solved problems, unsolved problems and non-problems in concurrency.","author":"L.Lamport","year":"1984","journal-title":"Proceedings of the Third Annual ACM Symposium on Principles of Distributed Computing,"},{"key":"IJISMD.2018070102-18","doi-asserted-by":"crossref","unstructured":"Mustafiz, S., Kienzle, J., & Vangheluwe, H. (2009). Model transformation of dependability-focused requirements models. Paper presented atInternational Conference on Software Engineering, Vancouver, Canada.","DOI":"10.1109\/MISE.2009.5069897"},{"key":"IJISMD.2018070102-19","year":"2011","journal-title":"OMG unified modeling language tm (omg uml), infrastructure (Technical report)"},{"key":"IJISMD.2018070102-20","article-title":"A formal approach to use cases and their relationships","volume":"Vol. 1618","author":"G.\u00d6vergaard","year":"2004","journal-title":"The Unified Modeling Language, LNCS"},{"key":"IJISMD.2018070102-21","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45314-8_11"},{"key":"IJISMD.2018070102-22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03240-0_7"},{"key":"IJISMD.2018070102-23","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-29645-1_21"},{"key":"IJISMD.2018070102-24","doi-asserted-by":"publisher","DOI":"10.5381\/jot.2005.4.6.a5"},{"key":"IJISMD.2018070102-25","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-13595-8_26"},{"key":"IJISMD.2018070102-26","article-title":"DIVINE: Explicit-State LTL Model Checker","volume":"Vol. 9636","author":"V.\u0160till","year":"2016","journal-title":"Tools and Algorithms for the Construction and Analysis of Systems, LNCS"},{"key":"IJISMD.2018070102-27","doi-asserted-by":"crossref","unstructured":"Whittle, J. (2006). Specifying Precise Use Cases with Use Case Charts. In J.M. Bruel (Eds.), Satellite Events at the MoDELS 2005 Conference, LNCS (Vol. 3844). Springer.","DOI":"10.1007\/11663430_30"},{"key":"IJISMD.2018070102-28","doi-asserted-by":"publisher","DOI":"10.5381\/jot.2005.4.6.a4"}],"container-title":["International Journal of Information System Modeling and Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.igi-global.com\/viewtitle.aspx?TitleId=218170","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,5,6]],"date-time":"2022-05-06T10:26:25Z","timestamp":1651832785000},"score":1,"resource":{"primary":{"URL":"http:\/\/services.igi-global.com\/resolvedoi\/resolve.aspx?doi=10.4018\/IJISMD.2018070102"}},"subtitle":[""],"short-title":[],"issued":{"date-parts":[[2018,7]]},"references-count":29,"journal-issue":{"issue":"3"},"URL":"https:\/\/doi.org\/10.4018\/ijismd.2018070102","relation":{},"ISSN":["1947-8186","1947-8194"],"issn-type":[{"value":"1947-8186","type":"print"},{"value":"1947-8194","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,7]]}}}