Una guía general para la especificación y verificación formal de requerimientos usando Event-B™ y Rodin™
DOI:
https://doi.org/10.26507/rei.v7n14.230Palabras clave:
modelamiento formal, métodos formales, Theorem Proving, Event-B™, Rodin™, programación e ingeniería de softwareResumen
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.
Descargas
Referencias bibliográficas
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.
Descargas
Publicado
Cómo citar
Número
Sección
Licencia
Se autoriza la reproducción total o parcial de los documentos publicados en la Revista siempre y cuando se cite la fuente y el autor.
| Estadísticas de artículo | |
|---|---|
| Vistas de resúmenes | |
| Vistas de PDF | |
| Descargas de PDF | |
| Vistas de HTML | |
| Otras vistas | |
