Keep All Objectives Satisfied (KAOS) to Event-B Models Transformation

Syahana Nur'Ain Saharudin, Mar Yah Said

Abstract


Requirements engineering is an important aspect of the software development methodology because it is the first phase in every software development. The usefulness of formal language in requirements is well-established to ensure consistency. However, the conversion from informal requirements to the formal specification phase is still challenging because it requires advanced skills and much practice. Due to this challenge, we improve the conversion and relationship of these two phases by capturing requirements using KAOS approach and writing the formal specification using Event-B language. KAOS approach allows modeling the requirements through goal hierarchies, whereas Event-B is a formal system-level modeling and analysis method. This work proposes model transformation rules from KAOS model to Event-B model, along with implementing the rules, and evaluates the proposed rules using Mine Pump Controller case study. We used a model-driven approach, specifically model-to-model transformation, to transform KAOS model to Event-B model. We modeled the case study into the KAOS model to obtain the source model for our model transformation and extend the existing KAOS meta-model by adding four new meta-classes to ensure the KAOS model can accommodate all Event-B components. Our proposed rules manage to generate an abstract Event-B model, and a set of proof obligations have been used to verify the correctness of the model. However, the designers must manually perform the transition between the generated outputs to the Event-B platform.

Keywords


KAOS method; Event-B; goal-oriented requirements engineering; model-driven engineering; formal specification.

Full Text:

PDF

References


J. Horkoff, F. B. Aydemir, E. Cardoso, T. Li, A. Mate, E. Paja, M. Salnitri, L. Piras, J. Mylopoulous and P. Giorgini, “Goal-oriented requirements engineering: An extended systematic mapping study,†Req. Eng., vol. 4, no. 2, pp. 133-160. June. 2019, doi: 10.1007/s00766-017-0280-z.

R. Kasauli, E. Knauss, J. Horkoff, G. Liebel and F. G. de Oliveira, “Requirements engineering challenges and practices in large-scale agile system development,†J. Sys. Soft., vol. 172. Elsevier Ltd, p. 110851, Feb. 2021, doi: 10.1016/j.jss.2020.110851.

M. Tukur, S. Umar and J. Hassine, “Requirement engineering challenges: A systematic mapping study on the academic and the industrial perspective,†Arabian J. Sci. Eng., vol. 46, no. 4, pp. 3723-3748, Apr. 2021, doi: 10.1007/s13369-020-05159.

H. Kaiya, N. Yoshioka, H. Washizaki, T. Okubo, A. Hazeyama, S. Ogata and T. Tanaka, “Eliciting requirements for improving users’ behavior using transparency,†in Comm. Comp. Inf. Sci., 2018, vol. 809, pp. 41-56, doi: 10.1007/978-981-10-7796-8_4.

M. M. Awan, F. Azam, M. W. Anwar and Y. Rasheed, “Formal requirements specification: Z notation meta model facilitating model to model transformation,†in ICSIE 2020 – Proc. 2020 9th Int. Conf. Soft. Info. Eng., Nov. 2020, pp. 61-66, doi: 10.1145/3436829.3436845.

M. Gleirscher, S. Foster and J. Woodcock, “New opportunities for integrated formal methods,†ACM Computing Surveys, vol. 52, no. 6, pp. 1-36, Oct. 2019, doi: 10.1145/3357231.

M. Ozkaya, “Do the informal and formal software modelling notations satisfy practitioners for software architecture modelling?†Info. Soft. Tech., vol. 95, pp. 15-33, March. 2018, doi: 10.1016/j.infsof.2017.10.008.

E. Alkhammash, “Formal modelling of OWL ontologies-based requirements for the development of safe and secure smart city systems,†Soft Computing, vol. 24, no. 15, pp. 11095-11108, Feb. 2020, doi: 10.1007/s00500-020-04688-z.

E. Osama, M. Abdelsalam and A. Khedr, “The effect of requirements quality and requirements volatility on the success of information systems projects,†Int. J. Adv. Comp. Sci. App., vol. 11, no. 9, Oct. 2020, doi: 10.14569/IJACSA.2020.0110950.

A. Matoussi, F. Gervais and R. Laleau, “A goal-based approach to guide the design of an abstract Event-B specification,†in 16th IEEE Int. Conf. Eng. Complex Comp. Sys., 2011, pp. 139-148, doi: 10.1109/ICECCS.2011.21.

E. Souza and A. Moreira, “Deriving services from KAOS models,†In Proc. ACM Symposium on Applied Computing, 2018, pp. 1308-1315, doi: 10.1145/3167132.3167273.

A. Cailliau and A. van Lamsweerde, “Runtime monitoring and resolution of probabilistic obstacles to system goals,†ACM Transactions on Autonomous and Adaptive Systems, vol. 14, no. 1, pp. 1-40, Sept. 2019, doi: 10.1145/3337800.

J. R. Abrial, Modelling in Event-B – System and software engineering, 1st ed. Cambridge: Cambridge University Press, 2010, pp. 1-586, doi: 10.1017/CBO9781139195881.

C. Zhu, M. Butler, and C. Cirstea, “Trace semantics and refinement patterns for real-time properties Event-B models,†Science of Computer Programming, vol. 197. Elsevier Ltd, p. 102513, Oct. 2020, doi: 10.1016/j.scico.2020.102513.

N. Ulfat-Bunyadi, N. G. Mohammadi, R. Wirtz and M. Heisel, “Systematic refinement of softgoals using a combination of KAOS goal models and problem diagrams,†in Comm. Comp. Inf. Sci., 2019, vol. 1077, pp. 150-172, doi: 10.1007/978-3-030-29157-0_7.

J. R. Abrial, M. Butler, S. Hallerstede, T. S. Hoang, F. Mehta and L. Voisin, “Rodin: An open toolset for modelling and reasoning in Event-B,†Int. J. Soft. Tools for Tech. Transfer, vol. 12, no. 6, pp. 447-466, Apr. 2010, doi: 10.1007/s10009-010-0145-y.

P. Andre, C. Attiogbe and A. Lanoix, “A tool-assisted method for the systematic construction of critical embedded systems using Event-B,†Comp. Sci. Info. Sys., vol. 17, no. 1, pp. 315-338, Jan. 2020, doi: 10.2298/CSIS190501042A.

A. Mammar, M. Frappier, S. J. T. Fotso, and R. Laleau, “A formal refinement-based analysis of the hybrid ERTMS/ETCS level 3 standard,†Int. J. Soft. Tools for Tech. Transfer, vol. 22, no. 3, pp. 333-347, June 2020, doi: 10.1007/s10009-019-00543-1.

J. Bicarregui, A. Arenas, B. Aziz, P. Massonet and C. Ponsard, “Towards modelling obligations in Event-B,†in Lecture Notes in Computer Science, vol. 5238, 2008, pp. 181-194, doi: 10.1007/978-3-540-87603-8_15.

C. Ponsard and X. Devroey, “Generating high-level Event-B system models from KAOS requirements models,†in XXIXeme Congres INFORSID 2011 – 29th Conf. INFORSID, 2011, pp. 317-332.

S. J. T. Fotso, M. Frappier, R. Laleau and A. Mammar, “Modelling the hybrid ERTMS/ETCS level standard using a formal requirement engineering approach,†Int. J. Soft. Tools for Tech. Transfer, vol. 22, no. 3, pp. 349-363, June 2020, doi: 10.1007/s10009-019-00542-2.

D. Akdur, V. Garousi, and O. Demirors, “A survey on modelling and model-driven engineering practices in the embedded software industry,†J. Sys. Arch., vol. 91, pp. 62-82, Oct. 2018, doi: 10.1016/j.sysarc.2018.09.007.

A. Bucchiarone, J. Cabot, R. F. Paige and A. Pierantonio, “Grand challenges in model-driven engineering: An analysis of the state of the research,†Soft. and Sys. Modelling, vol. 19, no. 1, pp. 5-13, Jan. 2020, doi: 10.1007/s10270-019-00773-6.

E. Richa, E. Borde and L. Pautet, “Translation of ATL to AGT and application to code generator for Simulink,†Soft. and Sys. Modelling, vol. 18, no. 1, pp. 321-344, Feb 2019, doi: 10.1007/s10270-017-0607-8.

S. Gotz and M. Tichy, “Investigating the origins of complexity and expressiveness in ATL transformations,†J. Obj. Tech., vol. 19, no. 2, pp. 1-21, July 2020, doi: 10.5381/jot.2020.19.2.a12.

A. P. F. Magalhaes, A. M. S. Andrade and R. S. P. Maciel, “Model driven transformation development (MDTD): An approach for developing model to model transformation,†Info. Soft. Tech., vol. 114, pp. 55-76, Oct. 2019, doi: 10.1016/j.infsof.2019.06.004.

A. S. A. Hadad, C. Ma and A. A. O. Ahmed, “Formal verification of AADL models by Event-B,†IEEE Access, vol. 8, pp. 72814-72834, Apr. 2020, doi: 10.1109/ACCESS.2020.2987972.

K. Morris, C. Snook, T. S. Hoang, G. Hulette, R. Armstrong and M. Butler, “Formal verification of run-to-completion style statecharts using event-b,†in Comm. Comp. Info. Sci., 2020, vol. 1269, pp. 311-325, doi: 10.1007/978-3-030-59155-7_24.

Objectiver (2007). [Online]. Available: http://www.objectiver.com/




DOI: http://dx.doi.org/10.18517/ijaseit.12.6.15875

Refbacks

  • There are currently no refbacks.


Published by INSIGHT - Indonesian Society for Knowledge and Human Development