Towards a guideline for formal specification and verification of requirements using Event-B™ and Rodin™
DOI:
https://doi.org/10.26507/rei.v7n14.230Keywords:
formal modeling, formal methods, Theorem Proving, Event-B™, Rodin™, programming and software engineeringAbstract
Formal modeling is a technique commonly used to specify and verify mathematical models of software systems through formal methods; Theorem Proving is part of such methods, which uses the first-order logic and set theory to verify mathematical models.
To perform the specification process of a system there are several languages, one of them is Event-B™ and their respective development environment Rodin™, both provides the necessary components for the modeling and formal verification of systems. This paper presents some guidelines for carrying out the process of formal specification and verification of requirements by exploring the use of Event-B™ and Rodin™, as tools to support the verification process.Downloads
References
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.
Downloads
Published
How to Cite
Issue
Section
License
Total or partial reproduction of the documents published in the journal is authorized only when the source and author are cited.
| Article metrics | |
|---|---|
| Abstract views | |
| Galley vies | |
| PDF Views | |
| HTML views | |
| Other views | |
