Una guía general para la especificación y verificación formal de requerimientos usando Event-B™ y Rodin™

  • Holmes Giovanny Salazar Osorio Universidad del Valle, Cali
  • Harvin Jessid Rengifo Romero Universidad del Valle, Cali
  • Liliana Esther Machuca Villegas Universidad del Valle, Cali
  • Jesús Alexander Aranda Bueno Universidad del Valle, Cali

Resumen

El modelamiento formal es una técnica utilizada comúnmente para especificar y verificar modelos matemáticos de un sistema de software a través de métodos formales. Theorem Proving hace parte de dichos métodos, el cual utiliza la lógica de primer orden y la teoría de conjuntos para verificar modelos matemáticos.

Para llevar a cabo el proceso de especificación de un sistema existe una gran variedad de lenguajes, uno de ellos es Event-B™ y su respectivo entorno de desarrollo Rodin™, ambos proveen los componentes necesarios para realizar el modelamiento y la verificación formal de sistemas. Este artículo presenta una guía para llevar a cabo el proceso de especificación y verificación formal de requerimientos basadas en el modelamiento formal, de esta manera se explora la posibilidad ofrecida por Event-B™ y Rodin™, como herramientas de apoyo al proceso de verificación.

Biografía del autor/a

Holmes Giovanny Salazar Osorio, Universidad del Valle, Cali
Estudiante de Ingeniería de Sistemas de la Universidad del Valle
Harvin Jessid Rengifo Romero, Universidad del Valle, Cali
Estudiante de Ingeniería de Sistemas de la Universidad del Valle
Liliana Esther Machuca Villegas, Universidad del Valle, Cali

Ingeniera de Siatemas con Maestría en Ingeneiría con énfasis en Ingeniería de sistemas y computación.

Actualmente soy docente de la Escuela de Ingeniería de Sistemas y Computación de la Universidad del Valle, Cali, Colombia

Jesús Alexander Aranda Bueno, Universidad del Valle, Cali

Ingeniero de Siatemas con Doctorado en Ingeniería con énfasis en Ingeniería de sistemas y computación.

Actualmente soy docente de la Escuela de Ingeniería de Sistemas y Computación de la Universidad del Valle, Cali, Colombia

Citas

Aagaard, M., Leeser, M. (1993). A Theorem Proving Based Methodology for Software Verification. Recuperado en noviembre de 2012 de http://ecommons.cornell.edu/bitstream/1813/6101/1/93-1335.pdf.

Abrial, J. R. (2010). Modeling in Event-B - System and Software Engineering. Cambridge University Press.

Abrial, J., Butler, M., Hallerstede, S., Hoang, T., Mehta, F., &

Voisin, L. (2010). Rodin: an open toolset for modeling and reasoning in Event-B. International Journal on Software Tools for Technology Transfer (STTT), 12 (6), 447–466.

Badeau, F., & Amelot, A. (2005). Using B as a high level programming language in an industrial project: Roissy VAL. ZB 2005: Formal Specification and Development in Z and B, 15 - 25.

Behm, P., Benoit, P., Faivre, A., & Meynadier, J. M. (1999). METEOR: A successful application of B in a large project. FM’99—Formal Methods, 712 - 712.

Bibel, W. (1987). Automated Theorem Proving Artificial Intelligence. (2da. Ed.). Braunschweig: Vieweg & Sohn.

Bloem, R. Cavada, R. Pill, I. Roveri, M. & Tchaltsev, A. (2005). RAT: A tool for the formal analysis of requirements. In Proc. 19th CAV, LNCS 4590, 263–267.

Bove, A., Dybjer, P. & Norell, U. (2009). A Brief Overview of Agda - A Functional Language with Dependent Types. Theorem Proving in Higher Order Logics , 5674 (LNCS), 73-78.

Cavada, R. Cimatti, A. Mariotti, A. Mattarei, C. & Micheli, A. (2009). Supporting Requirements Validation: The EuRailCheck Tool. Proceedings of the 2009 IEEE/ACM International Conference on Automated Software Engineering, 665 – 667.

Cimatti, A. Giunchiglia, A. Mongardi, G. Romano, D. Torielli, F.

Traverso, P. (1997). Model Checking Safety Critical Software with SPIN: An Application to a Railway Interlocking System. Proceedings.Third SPIN Workshop, R. Langerak, ed., Twente Univ, 1-13.

Clarke, E. (1997). Model checking. Foundations of software technology and theoretical computer science, 54–56.

Deploy Project. (2012). Rodin User’s Handbook. Recuperado en junio de 2012 de http://handbook.Event-B.org/current/html/index.html.

Deploy Project. (2012a) Rodin Plug-ins. Recuperado en junio de 2012 de http://wiki.Event-B.org/index.php/Rodin_Plug-ins.

Duque, J. G. (2000). Especificación, verificación y mantenimiento de requisitos funcionales con técnicas de descripción formal. PhD thesis, Departamento de Tecnología de las Comunicaciones. University of Vigo.

Free Software Foundation. (2012). Common Public License: Licencia Pública Común. Recuperado en junio de 2012 en http://www.gnu.org/licenses/license-list.es.html#SoftwareLicenses.

Gervasi, A. & Zowghi, A. (2005). Reasoning about inconsistencies in natural language requirements. ACM Transactions on software engineering and methodology, 277-330.

Jones, C. B. (1990). Systematic software development using VDM, Vol. 2. Prentice Hall.

Montoya, E. S. (2010). Métodos formales e Ingeniería de Software. Revista Virtual Universidad Católica del Norte, (30), 1–26.

Nipkow, T., Paulson, L. C., & Wenzel, M. (2002). Isabelle/HOL: a proof assistant for higher-order logic, Springer Verlag, 2283.

Owre, S., Rushby, J., & Shankar, N. (1992). PVS: A prototype verification system, Automated Deduction—CADE-11, 748–752.

Padidar, S. (2010). A Study In The Use Of Event-B For System Development From A Software Engineering Viewpoint. MSc Dissertation, University of Edinburgh. Recuperado en noviembre de 2012 de http://www.ai4fm.org/papers/MSc-Padidar.pdf

Robinson, K. (2011). System Modeling & Design Using Event-B. The University of New South Wales. Recuperado en agosto de 2012 de http://wiki.event-b.org/images/SM%26D-KAR.pdf

Rueda, C. (2012). Desarrollo Formal de Software: Obligaciones de Prueba. Recuperado en febrero de 2012 de http://cic.javerianacali.edu.co/wiki/lib/exe/fetch.php?media=materias:desarrollo:clase4_5-obligaciones.pdf.

Wiegers, K. (2003). Software Requirements. (2da. Ed.). Microsoft Press.

Publicado
2012-12-15
Cómo citar
Salazar Osorio, H. G., Rengifo Romero, H. J., Machuca Villegas, L. E., & Aranda Bueno, J. A. (2012). Una guía general para la especificación y verificación formal de requerimientos usando Event-B™ y Rodin™. Revista Educación En Ingeniería, 7(14), 82-91. https://doi.org/10.26507/rei.v7n14.230
Sección
Sección Ingeniería y Desarrollo