Navegar

Colección

Datos Estadísticas

Artículo

Estamos trabajando para incorporar este artículo al repositorio
Consulte el artículo en la página del editor
Consulte la política de Acceso Abierto del editor

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. © 1976-2012 IEEE.

Registro:

Documento: Artículo
Título:Elaborating requirements using model checking and inductive learning
Autor:Alrajeh, D.; Kramer, J.; Russo, A.; Uchitel, S.
Filiación:Department of Computing, Imperial College London, 180 Queen's Gate, London SW7 2AZ, United Kingdom
Departamento de Computacion, FCEyN, University of Buenos Aires, Buenos Aires, Argentina
Palabras clave:behavior model refinement; goal operationalization; inductive learning; model checking; Requirements elaboration; Behavior model; goal operationalization; Inductive learning; Operational requirements; Positive examples; Requirements elaboration; Requirements specifications; Iterative methods; Model checking; Specifications; Learning systems
Año:2013
Volumen:39
Número:3
Página de inicio:361
Página de fin:383
DOI: http://dx.doi.org/10.1109/TSE.2012.41
Título revista:IEEE Transactions on Software Engineering
Título revista abreviado:IEEE Trans Software Eng
ISSN:00985589
CODEN:IESED
Registro:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_00985589_v39_n3_p361_Alrajeh

Referencias:

  • Alrajeh, D., (2010) Requirements Elaboration Using Model Checking and Inductive Learning, , PhD thesis Imperial College London
  • Alrajeh, D., Kramer, J., Russo, A., Uchitel, S., Deriving non-zeno behavior models from goal models using ILP (2010) J. Formal Aspects of Computing, 22, pp. 217-241
  • Alrajeh, D., Kramer, J., Russo, A., Uchitel, S., Learning operational requirements from goal models (2009) Proc. 31st Int'l Conf. Software Eng, pp. 265-275
  • Alrajeh, D., Ray, O., Russo, A., Uchitel, S., Extracting requirements from scenarios with ILP (2006) Proc. 16th Int'l Conf. Inductive Logic Programming, pp. 63-77
  • Alrajeh, D., Ray, O., Russo, A., Uchitel, S., Using abduction and induction for operational requirements elaboration (2009) J. Applied Logic, 7 (3), pp. 275-288
  • Anton, A.I., (1997) Goal Identification and Refinement in the Specification of Software-Based Information Systems, , PhD thesis Georgia Inst. of Technology
  • Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tachella, A., NuSMV 2: An opensource tool for symbolic model checking (2002) Proc. 14th Int'l Conf. Computer Aided Verification, pp. 241-268
  • Clark, K., Negation as failure (1987) Readings in Nonmonotonic Reasoning, pp. 311-325. , Morgan Kaufmann Publishers
  • Corapi, D., Russo, A., Lupu, E., Inductive logic programming as abductive search (2010) Proc. Technical Comm. 26th Int'l Conf. Logic Programming, pp. 54-63
  • Damas, C., Lambeau, B., Dupont, P., Van Lamsweerde, A., Generating annotated behavior models from end-user scenarios (2005) IEEE Transactions on Software Engineering, 31 (12), pp. 1056-1073. , DOI 10.1109/TSE.2005.138
  • Damas, C., Lambeau, B., Van Lamsweerde, A., Scenarios, goals, and state machines: A win-win partnership for model synthesis (2006) Proceedings of the ACM SIGSOFT Symposium on the Foundations of Software Engineering, pp. 197-207. , DOI 10.1145/1181775.1181800, 1181800, Proceedings of the 14th ACM SIGSOFT International Symposium on Foundations of Software Engineering
  • Dardenne Anne, Van Lamsweerde Axel, Fickas Stephen, Goal-directed requirements acquisition (1993) Science of Computer Programming, 20 (1-2), pp. 3-50. , DOI 10.1016/0167-6423(93)90021-G
  • Darimont, R., Van Lamsweerde, A., Formal refinement patterns for goal-driven requirements elaboration (1996) Proc. Fourth ACM SIGSOFT Symp. Foundations of Software Eng, pp. 179-190
  • De Roever, W.P., Hooman, J., Design and verification in real-time distributed computing: An introduction to compositional methods (1990) Proc. IFIP WG6.1 Ninth Int'l Symp. Protocol Specification, Testing and Verification IX, pp. 37-56
  • Fidjeland, A., Luk, W., Muggleton, S., Scalable acceleration of inductive logic programs (2002) Proc. IEEE Int'l Conf. Field-Programmable Technology, pp. 252-259
  • Finkelstein, A., Dowell, J., A comedy of errors: The london ambulance service case study (1996) Proc. Eighth Int'l Workshop Software Specification and Design, pp. 2-4
  • Fuxman, A., Liu, L., Mylopoulos, J., Pistore, M., Roveri, M., Traverso, P., Specifying and analyzing early requirements in Tropos (2004) Requirements Engineering, 9 (2), pp. 132-150. , DOI 10.1007/s00766-004-0191-7
  • Fuxman, A., Pistore, M., Mylopoulos, J., Traverso, P., Model checking early requirements specifications in Tropos (2001) Proceedings of the IEEE International Conference on Requirements Engineering, pp. 174-181
  • Gelfond, M., Lifschitz, V., The stable model semantics for logic programming (1988) Proc. Fifth Int'l Conf. Logic Programming, pp. 1070-1080
  • Giannakopoulou, D., (1999) Model Checking for Concurrent Software Architectures, , PhD thesis Imperial College London
  • Giannakopoulou, D., Magee, J., Fluent model checking for event-based systems (2003) Proc. 11thACM SIGSOFT Symp. Foundations Software Eng, pp. 257-266
  • Jackson, M., The world and the machine (1995) Proc. 17th Int'l Conf. Software Eng, pp. 283-292
  • Keller, R.M., Formal verification of parallel programs (1976) Comm. ACM, 19 (7), pp. 371-384
  • Kowalski, R.A., Sergot, M., A logic-based calculus of events (1986) New Generation Computing, 4 (1), pp. 67-95
  • Koymans, R., (1992) Specifying Message Passing and Time-Critical Systems with Temporal Logic, , Springer
  • Kramer Jeff, Magee Jeff, Sloman Morris, Lister Andrew, CONIC: An integrated approach to distributed computer control systems (1983) IEE Proceedings E: Computers and Digital Techniques, 130 (1), pp. 1-10
  • Letier, E., (2001) Reasoning about Agents in Goal-Oriented Requirements Engineering, , PhD thesis Dépt. Ingénierie Informatique, Université Catholique de Louvain
  • Letier, E., (2002) Goal-Oriented Elaboration of Requirements for A Safety Injection Control System, , technical report, Département d'Inge ́nierie Informatique, Université Catholique de Louvain
  • Letier, E., Kramer, J., Magee, J., Uchitel, S., Deriving event-based transitions systems from goal-oriented requirements models (2008) Automated Software Eng, 15, pp. 175-206
  • Letier, E., Van Lamsweerde, A., Agent-based tactics for goal-oriented requirements elaboration (2002) Proceedings - International Conference on Software Engineering, pp. 83-93
  • Letier, E., Van Lamsweerde, A., Deriving operational software specifications from system goals (2002) Proc. 10th ACM SIGSOFT Symp. Foundations of Software Eng, pp. 119-128
  • Lloyd, J.W., (1984) Foundations of Logic Programming, , Springer
  • Ma, J., Russo, A., Broda, K., Clark, K., DARE: A system for distributed abductive reasoning (2008) Autonomous Agents and Multi-Agent Systems, 16 (3), pp. 271-297
  • Magee, J., Kramer, J., (1999) Concurrency: State Models and Java Programs, , Wiley
  • Manna, Z., Pnueli, A., (1992) The Temporal Logic of Reactive and Concurrent Systems, , Springer
  • Mitchell, T., (1997) Machine Learning, , McGraw Hill
  • Muggleton, S.H., Inverse entailment and progol (1995) New Generation Computing, 13 (3-4), pp. 245-286. , special issue on inductive logic programming
  • Muggleton, S.H., De Raedt, L., Inductive logic programming: Theory and methods (1994) J. Logic Programming, 19 (20), pp. 629-679
  • Mylopoulos, J., Chung, L., Nixon, B.A., Representing and using non-functional requirements: A process-oriented approach (1992) IEEE Trans. Software Eng, 18, pp. 483-497
  • Patrizi, F., Lipoveztky, N., De Giacomo, G., Geffner, H., Computing infinite plans for ltl goals using a classical planner (2011) Proc. 22nd Int'l Joint Conf. Artificial Intelligence, pp. 2003-2009
  • Ray, O., Using abduction for induction of normal logic programs (2006) Proc. Workshop Abduction and Induction in AI and Scientific Modelling
  • Ray, O., Nonmonotonic abductive inductive learning (2009) J. Applied Logic, 7 (3), pp. 329-340
  • Ray, O., Broda, K., Russo, A., A hybrid abductive inductive proof procedure (2004) Logic J. Interest Group in Pure and Applied Logic, 12 (5), pp. 371-397
  • Rifaut, A., Massonet, P., Molderez, J., Ponsard, C., Stadnik, P., Van Lamsweerde, A., Van, H.T., FAUST: Formal analysis using specification tools (2003) Proc. 11th IEEE Int'l Conf. Requirements Eng, p. 350
  • Rolland, C., Grosz, G., Kla, R., Experience with goal-scenario coupling in requirements engineering (1999) Proc. IEEE Int'l Symp. Requirements Eng, pp. 74-81
  • Rolland, C., Guiding goal modeling using scenarios (1998) IEEE Transactions on Software Engineering, 24 (12), pp. 1055-1071
  • Sibay, G., Uchitel, S., Braberman, V., Existential live sequence charts revisited (2008) Proc. 30th Int'l Conf. Software Eng, pp. 41-50
  • Subrahmanian, V.S., Zaniolo, C., Relating stable models and ai planning domains (1995) Proc. 12th Int'l Conf. Logic Programming, pp. 233-247
  • Sutcliffe, A.G., Supporting scenario-based requirements engineering (1998) IEEE Transactions on Software Engineering, 24 (12), pp. 1072-1088
  • Uchitel, S., Brunet, G., Chechik, M., Synthesis of partial behavior models from properties and scenarios (2009) IEEE Trans. Software Eng, 35 (3), pp. 384-406. , May/June
  • Van Lamsweerde, A., Goal-oriented requirements eng.: A guided tour (2001) Proc. Fifth IEEE Int'l Symp. Requirements Eng, pp. 249-262
  • Van Lamsweerde, A., Inferring declarative requirements specifications from operational scenarios (1998) IEEE Transactions on Software Engineering, 24 (12), pp. 1089-1114

Citas:

---------- APA ----------
Alrajeh, D., Kramer, J., Russo, A. & Uchitel, S. (2013) . Elaborating requirements using model checking and inductive learning. IEEE Transactions on Software Engineering, 39(3), 361-383.
http://dx.doi.org/10.1109/TSE.2012.41
---------- CHICAGO ----------
Alrajeh, D., Kramer, J., Russo, A., Uchitel, S. "Elaborating requirements using model checking and inductive learning" . IEEE Transactions on Software Engineering 39, no. 3 (2013) : 361-383.
http://dx.doi.org/10.1109/TSE.2012.41
---------- MLA ----------
Alrajeh, D., Kramer, J., Russo, A., Uchitel, S. "Elaborating requirements using model checking and inductive learning" . IEEE Transactions on Software Engineering, vol. 39, no. 3, 2013, pp. 361-383.
http://dx.doi.org/10.1109/TSE.2012.41
---------- VANCOUVER ----------
Alrajeh, D., Kramer, J., Russo, A., Uchitel, S. Elaborating requirements using model checking and inductive learning. IEEE Trans Software Eng. 2013;39(3):361-383.
http://dx.doi.org/10.1109/TSE.2012.41