The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.03 - March (2013 vol.39)
pp: 361-383
Dalal Alrajeh , Imperial College London, London
Jeff Kramer , Imperial College London, London
Alessandra Russo , Imperial College London, London
Sebastian Uchitel , Imperial College London, London
ABSTRACT
The process of Requirements Engineering (RE) includes many activities, from goal elicitation to requirements specification. The aim is to develop an operational requirements specification that is guaranteed to satisfy the goals. In this paper, we propose a formal, systematic approach for generating a set of operational requirements that are complete with respect to given goals. We show how the integration of model checking and inductive learning can be effectively used to do this. The model checking formally verifies the satisfaction of the goals and produces counterexamples when incompleteness in the operational requirements is detected. The inductive learning process then computes operational requirements from the counterexamples and user-provided positive examples. These learned operational requirements are guaranteed to eliminate the counterexamples and be consistent with the goals. This process is performed iteratively until no goal violation is detected. The proposed framework is a rigorous, tool-supported requirements elaboration technique which is formally guided by the engineer's knowledge of the domain and the envisioned system.
INDEX TERMS
Wheels, Computational modeling, Software, Adaptation models, Calculus, Switches, Semantics, inductive learning, Requirements elaboration, goal operationalization, behavior model refinement, model checking
CITATION
Dalal Alrajeh, Jeff Kramer, Alessandra Russo, Sebastian Uchitel, "Elaborating Requirements Using Model Checking and Inductive Learning", IEEE Transactions on Software Engineering, vol.39, no. 3, pp. 361-383, March 2013, doi:10.1109/TSE.2012.41
REFERENCES
[1] D. Alrajeh, "Requirements Elaboration Using Model Checking and Inductive Learning," PhD thesis, Imperial College London, 2010.
[2] D. Alrajeh, J. Kramer, A. Russo, and S. Uchitel, "Deriving Non-Zeno Behavior Models from Goal Models Using ILP," J. Formal Aspects of Computing, vol. 22, pp. 217-241, 2010.
[3] D. Alrajeh, J. Kramer, A. Russo, and S. Uchitel, "Learning Operational Requirements from Goal Models," Proc. 31st Int'l Conf. Software Eng., pp. 265-275, 2009.
[4] D. Alrajeh, O. Ray, A. Russo, and S. Uchitel, "Extracting Requirements from Scenarios with ILP," Proc. 16th Int'l Conf. Inductive Logic Programming, pp. 63-77, 2006.
[5] D. Alrajeh, O. Ray, A. Russo, and S. Uchitel, "Using Abduction and Induction for Operational Requirements Elaboration," J. Applied Logic, vol. 7, no. 3, pp. 275-288, 2009.
[6] A.I. Anton, "Goal Identification and Refinement in the Specification of Software-Based Information Systems," PhD thesis, Georgia Inst. of Tech nology, 1997.
[7] A. Cimatti, E. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani, and A. Tachella, "NuSMV 2: An Opensource Tool for Symbolic Model Checking," Proc. 14th Int'l Conf. Computer Aided Verification, pp. 241-268, 2002.
[8] K. Clark, "Negation as Failure," Readings in Nonmonotonic Reasoning, pp. 311-325, Morgan Kaufmann Publishers, 1987.
[9] D. Corapi, A. Russo, and E. Lupu, "Inductive Logic Programming as Abductive Search," Proc. Technical Comm. 26th Int'l Conf. Logic Programming, pp. 54-63, 2010.
[10] C. Damas, P. Dupont, B. Lambeau, and A. van Lamsweerde, "Generating Annotated Behavior Models from End-User Scenarios," IEEE Trans. Software Eng., special issue on interaction and state-based modeling, vol. 31, no. 12, pp. 1056-1073, Dec. 2005.
[11] C. Damas, B. Lambeau, and A. van Lamsweerde, "Scenarios, Goals, and State Machines: A Win-Win Partnership for Model Synthesis," Proc. ACM Int'l Symp. Foundations of Software Eng., pp. 197-207, 2006.
[12] A. Dardenne, A. van Lamsweerde, and S. Fickas, "Goal-Directed Requirements Acquisition," Science of Computer Programming, vol. 20, no. 1, pp. 3-50, 1993.
[13] R. Darimont and A. van Lamsweerde, "Formal Refinement Patterns for Goal-Driven Requirements Elaboration," Proc. Fourth ACM SIGSOFT Symp. Foundations of Software Eng., pp. 179-190, 1996.
[14] W.P. de Roever and J. Hooman, "Design and Verification in Real-Time Distributed Computing: An Introduction to Compositional Methods," Proc. IFIP WG6.1 Ninth Int'l Symp. Protocol Specification, Testing and Verification IX, pp. 37-56, 1990.
[15] A. Fidjeland, W. Luk, and S. Muggleton, "Scalable Acceleration of Inductive Logic Programs," Proc. IEEE Int'l Conf. Field-Programmable Technology, pp. 252-259, 2002.
[16] A. Finkelstein and J. Dowell, "A Comedy of Errors: The London Ambulance Service Case Study," Proc. Eighth Int'l Workshop Software Specification and Design, pp. 2-4, 1996.
[17] A. Fuxman, L. Liu, J. Mylopoulos, M. Pistore, M. Roveri, and P. Traverso, "Specifying and Analyzing Early Requirements in TROPOS," Requirements Eng., vol. 9, no. 2, pp. 132-150, 2004.
[18] A. Fuxman, J. Mylopoulos n, M. Pistore, and P. Traverso, "Model Checking Early Requirements Specifications in Tropos," Proc. IEEE Fifth Int'l Symp. Requirements Eng., pp. 174-181, 2001.
[19] M. Gelfond and V. Lifschitz, "The Stable Model Semantics for Logic Programming," Proc. Fifth Int'l Conf. Logic Programming, pp. 1070-1080, 1988.
[20] D. Giannakopoulou, "Model Checking for Concurrent Software Architectures," PhD thesis, Imperial College London, 1999.
[21] D. Giannakopoulou and J. Magee, "Fluent Model Checking for Event-Based Systems," Proc. 11th ACM SIGSOFT Symp. Foundations Software Eng., pp. 257-266, 2003.
[22] M. Jackson, "The World and the Machine," Proc. 17th Int'l Conf. Software Eng., pp. 283-292, 1995.
[23] R.M. Keller, "Formal Verification of Parallel Programs," Comm. ACM, vol. 19, no. 7, pp. 371-384, 1976.
[24] R.A. Kowalski and M. Sergot, "A Logic-Based Calculus of Events," New Generation Computing, vol. 4, no. 1, pp. 67-95, 1986.
[25] R. Koymans, Specifying Message Passing and Time-Critical Systems with Temporal Logic. Springer, 1992.
[26] J. Kramer, J. Magee, and M. Sloman, "Conic: An Integrated Approach to Distributed Computer Control Systems," Proc. IEE Computers and Digital Techniques, vol. 30, pp. 1-10, 1983.
[27] E. Letier, "Reasoning About Agents in Goal-Oriented Requirements Engineering," PhD thesis, Dépt. Ingénierie Informatique, Université Catholique de Louvain, 2001.
[28] E. Letier, "Goal-Oriented Elaboration of Requirements for a Safety Injection Control System," technical report, Département d'Ingénierie Informatique, Université Catholique de Louvain, 2002.
[29] E. Letier, J. Kramer, J. Magee, and S. Uchitel, "Deriving Event-Based Transitions Systems from Goal-Oriented Requirements Models," Automated Software Eng., vol. 15, pp. 175-206, 2008.
[30] E. Letier and A. van Lamsweerde, "Agent-Based Tactics for Goal-Oriented Requirements Elaboration," Proc. 24th Int'l Conf. Software Eng., pp. 83-93, 2002.
[31] E. Letier and A. van Lamsweerde, "Deriving Operational Software Specifications from System Goals," Proc. 10th ACM SIGSOFT Symp. Foundations of Software Eng., pp. 119-128, 2002.
[32] J.W. Lloyd, Foundations of Logic Programming. Springer, 1984.
[33] J. Ma, A. Russo, K. Broda, and K. Clark, "DARE: A System for Distributed Abductive Reasoning," Autonomous Agents and Multi-Agent Systems, vol. 16, no. 3, pp. 271-297, 2008.
[34] J. Magee and J. Kramer, Concurrency: State Models and Java Programs. Wiley, 1999.
[35] Z. Manna and A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems. Springer, 1992.
[36] T. Mitchell, Machine Learning. McGraw Hill, 1997.
[37] S.H. Muggleton, "Inverse Entailment and Progol," New Generation Computing, special issue on inductive logic programming, vol. 13, nos. 3/4, pp. 245-286, 1995.
[38] S.H. Muggleton and L. De Raedt, "Inductive Logic Programming: Theory and Methods," J. Logic Programming, vol. 19, no. 20, pp. 629-679, 1994.
[39] J. Mylopoulos, L. Chung, and B.A. Nixon, "Representing and Using Non-Functional Requirements: A Process-Oriented Approach," IEEE Trans. Software Eng., vol. 18, pp. 483-497, 1992.
[40] F. Patrizi, N. Lipoveztky, G. De Giacomo, and H. Geffner, "Computing Infinite Plans for LTL Goals Using a Classical Planner," Proc. 22nd Int'l Joint Conf. Artificial Intelligence, pp. 2003-2009, 2011.
[41] O. Ray, "Using Abduction for Induction of Normal Logic Programs," Proc. Workshop Abduction and Induction in AI and Scientific Modelling, 2006.
[42] O. Ray, "Nonmonotonic Abductive Inductive Learning," J. Applied Logic, vol. 7, no. 3, pp. 329-340, 2009.
[43] O. Ray, K. Broda, and A. Russo, "A Hybrid Abductive Inductive Proof Procedure," Logic J. Interest Group in Pure and Applied Logic, vol. 12, no. 5, pp. 371-397, 2004.
[44] A. Rifaut, P. Massonet, J. Molderez, C. Ponsard, P. Stadnik, A. van Lamsweerde, and H. Tran Van, "FAUST: Formal Analysis Using Specification Tools," Proc. 11th IEEE Int'l Conf. Requirements Eng., p. 350, 2003.
[45] C. Rolland, G. Grosz, and R. Kla, "Experience with Goal-Scenario Coupling in Requirements Engineering," Proc. IEEE Int'l Symp. Requirements Eng., pp. 74-81, 1999.
[46] C. Rolland, C. Souveyet, and C.B. Achour, "Guiding Goal Modeling Using Scenarios," IEEE Trans. Software Eng., vol. 24, no. 12, pp. 1055-1071, Dec. 1998.
[47] G. Sibay, S. Uchitel, and V. Braberman, "Existential Live Sequence Charts Revisited," Proc. 30th Int'l Conf. Software Eng., pp. 41-50, 2008.
[48] V.S. Subrahmanian and C. Zaniolo, "Relating Stable Models and AI Planning Domains," Proc. 12th Int'l Conf. Logic Programming, pp. 233-247, 1995.
[49] A. Sutcliffe, N.A.M. Maiden, S. Minocha, and D. Manuel, "Supporting Scenario-Based Requirements Engineering," IEEE Trans. Software Eng., vol. 24, no. 12, pp. 1072-1088, Dec. 1998.
[50] S. Uchitel, G. Brunet, and M. Chechik, "Synthesis of Partial Behavior Models from Properties and Scenarios," IEEE Trans. Software Eng., vol. 35, no. 3, pp. 384-406, May/June 2009.
[51] A. van Lamsweerde, "Goal-Oriented Requirements Eng.: A Guided Tour," Proc. Fifth IEEE Int'l Symp. Requirements Eng., pp. 249-262, 2001.
[52] A. van Lamsweerde and L. Willemet, "Inferring Declarative Requirements Specifications from Operational Scenarios," IEEE Trans. Software Eng., vol. 24, no. 12, pp. 1089-1114, Dec. 1998.
68 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool