Hispanopedia Wiki
Articulo de referencia

Método B

El método B es un método de desarrollo de software basado en B , un método formal con soporte de herramientas basado en una notación de máquina abstracta , utilizado en el desar...

Hispanopedia WikiContenido en espanolLectura gratuita

El método B es un método de desarrollo de software basado en B , un método formal con soporte de herramientas basado en una notación de máquina abstracta , utilizado en el desarrollo de software informático . [ 1 ] [ 2 ]

En comparación con la notación Z , B es ligeramente más básica y se centra más en el refinamiento del código que en la mera especificación formal ; por lo tanto, es más fácil implementar correctamente una especificación escrita en B que una en Z. En particular, cuenta con un buen soporte de herramientas para ello. El mismo lenguaje se utiliza en la especificación, el diseño y la programación. Entre sus mecanismos se incluyen la encapsulación y la localidad de datos.

Historia

Jean-Raymond Abrial , creador del Método B y del Evento B.

B fue desarrollado originalmente en la década de 1980 por Jean-Raymond Abrial [ 3 ] [ 4 ] en Francia y el Reino Unido . [ 5 ] B está relacionado con la notación Z (también originada por Abrial) y admite el desarrollo de código de lenguaje de programación a partir de especificaciones. B se ha utilizado en importantes aplicaciones de sistemas críticos para la seguridad en Europa (como las líneas automáticas 14 y 1 del metro de París y el cohete Ariane 5 ). [ 6 ] [ 7 ] [ 8 ] Cuenta con un soporte de herramientas robusto y disponible comercialmente para especificación , diseño , prueba y generación de código .

Ib Holm Sørensen , líder del equipo de desarrollo de B-Toolkit y fundador de B-Core.

Desde finales de la década de 1980, Ib Holm Sørensen (1949–2012) fue fundamental para el desarrollo del Método B, [ 9 ] [ 10 ] habiendo trabajado previamente también en el desarrollo inicial de la notación Z. Dejó el Laboratorio de Computación de la Universidad de Oxford para dirigir un equipo para BP Research [ 11 ] y desarrollar el B-Toolkit, proporcionando soporte de herramientas para el Método B. Posteriormente, fundó la empresa B-Core (UK) Limited para dar soporte al B-Toolkit, [ 12 ] [ 13 ] que es una colección de herramientas de programación diseñadas para apoyar el uso de la notación B, y ayudó a completar varios proyectos relacionados con B.

Evento B

Posteriormente, se desarrolló otro método formal llamado Event-B [ 14 ] [ 15 ] [ 16 ] basado en el Método B, con el apoyo de la Plataforma Rodin . [ 17 ] [ 18 ] Event-B es un método formal orientado al modelado y análisis a nivel de sistema. Las características de Event-B son el uso de la teoría de conjuntos para el modelado, el uso del refinamiento para representar sistemas en diferentes niveles de abstracción y el uso de pruebas matemáticas para verificar la consistencia entre estos niveles de refinamiento.

Los componentes principales

La notación B se basa en la teoría de conjuntos y la lógica de primer orden para especificar diferentes niveles de descripción del software, abarcando el ciclo completo de desarrollo del proyecto.

Máquina abstracta

En la primera y más abstracta versión, que se denomina Máquina Abstracta , el diseñador debe especificar el objetivo del diseño.

Refinamiento

  • Luego, durante una etapa de refinamiento, pueden ampliar la especificación para aclarar el objetivo o para hacer que la máquina abstracta sea más concreta, agregando detalles sobre las estructuras de datos y los algoritmos que definen cómo se logra el objetivo.
  • La nueva versión, que se denomina Refinamiento , debe demostrar ser coherente e incluir todas las propiedades de la máquina abstracta.
  • El diseñador puede utilizar bibliotecas B para modelar estructuras de datos o para incluir o importar componentes existentes.

Implementación

  • El refinamiento continúa hasta que se logra una versión determinista: la Implementación .
  • Durante todas las etapas de desarrollo se utiliza la misma notación, y la última versión puede traducirse a un lenguaje de programación para su compilación.

Software

Existen diversos programas informáticos que son compatibles con el método B y el evento B.

Taller B

Desarrollado por ClearSy, Atelier B [ 19 ] [ 20 ] es una herramienta industrial que permite el uso operativo del Método B para desarrollar software probado y sin defectos (software formal). Hay dos versiones disponibles: 1) Edición Comunitaria, disponible para cualquier persona sin ninguna restricción; 2) Edición de Mantenimiento solo para titulares de contratos de mantenimiento. Atelier B se ha utilizado para desarrollar automatismos de seguridad para los diversos metros instalados en todo el mundo por Alstom y Siemens , y también para la certificación de Criterios Comunes y el desarrollo de modelos de sistemas por ATMEL y STMicroelectronics .

Kit de herramientas B

El B-Toolkit [ 21 ] [ 22 ] es una colección de herramientas de programación diseñadas para apoyar el uso de la B-Tool, [ 23 ] es un intérprete matemático basado en la teoría de conjuntos para apoyar el método B. El desarrollo fue realizado originalmente por Ib Holm Sørensen y otros, en BP Research y luego en B-Core (UK) Limited. [ 10 ]

El conjunto de herramientas utiliza una interfaz X Window Motif personalizada [ 24 ] para la gestión de la interfaz gráfica de usuario y se ejecuta principalmente en los sistemas operativos Linux , Mac OS X y Solaris . El código fuente de B-Toolkit está disponible en GitHub . [ 25 ]

Interfaz de la herramienta Click'n'Prove, un demostrador de teoremas interactivo para ayudar con las demostraciones formales utilizando el método B.

Haz clic y demuestra

La herramienta Click'n'Prove proporciona un entorno para la generación y el cumplimiento de obligaciones de prueba, para la verificación de consistencia y refinamiento. [ 26 ]

ProB

ProB es una herramienta combinada de animación de software y verificador de modelos para el método B. [ 27 ] Permite la animación de muchas especificaciones B y también puede verificar sistemáticamente una especificación en busca de varios tipos de errores. ProB incluye funciones de resolución de restricciones que pueden utilizarse para ayudar en la detección de interbloqueos , el descubrimiento de modelos y la generación de casos de prueba . La herramienta fue desarrollada por el grupo STUPS de la Universidad Heinrich Heine de Düsseldorf . [ 28 ]

Rodin

La plataforma Rodin es una herramienta que admite Event-B . [ 14 ] [ 29 ] [ 17 ] Rodin se basa en un entorno de desarrollo integrado (IDE) de software Eclipse y proporciona soporte para refinamiento y demostración matemática . La plataforma es de código abierto y forma parte del marco de Eclipse. Es extensible mediante complementos de componentes de software . El desarrollo de Rodin ha sido financiado por los proyectos de la Unión Europea DEPLOY (2008–2012), RODIN (2004–2007) y ADVANCE (2011–2014). [ 14 ]

Otros

BHDL proporciona un método para el diseño correcto de circuitos digitales , combinando las ventajas del lenguaje de descripción de hardware VHDL con la formalidad de B. [ 30 ]

APCB

APCB ( en francés : Association de Pilotage des Conférences B , el Comité Directivo de la Conferencia Internacional B ) ha organizado reuniones asociadas con el Método B. [ 31 ] Ha organizado conferencias ZB con el Grupo de Usuarios Z y conferencias ABZ, incluyendo Máquinas de Estado Abstractas (ASM) así como la notación Z.

Libros

Conferencias

Las siguientes conferencias han incluido explícitamente el Método B y/o el Evento B: [ 32 ]

  • Conferencia Z2B, Nantes , Francia , 10-12 de octubre de 1995
  • Primera Conferencia B, Nantes, Francia, 25-27 de noviembre de 1996
  • Segunda Conferencia B, Montpellier , Francia, 22-24 de abril de 1998
  • ZB 2000, York , Reino Unido , 28 de agosto - 2 de septiembre de 2000
  • ZB 2002, Grenoble , Francia, 23 a 25 de enero de 2002
  • ZB 2003, Turku , Finlandia , 4 a 6 de junio de 2003
  • ZB 2005, Guildford , Reino Unido, 2005
  • B 2007, Besanzón , Francia, 2007
  • B, De la investigación a la docencia, Nantes, Francia, 16 de junio de 2008
  • B, De la investigación a la docencia, Nantes, Francia, 8 de junio de 2009
  • B, De la investigación a la docencia, Nantes, Francia, 7 de junio de 2010
  • ABZ 2008, BCS , Londres , Reino Unido, 16-18 de septiembre de 2008
  • ABZ 2010, Orford , Québec , Canadá , 23 a 25 de febrero de 2010
  • ABZ 2012, Pisa , Italia , 18 a 22 de junio de 2012
  • ABZ 2014, Toulouse , Francia, 2 a 6 de junio de 2014
  • ABZ 2016, Linz , Austria , 23 a 27 de mayo de 2016
  • ABZ 2018, Southampton , Reino Unido, 5-8 de junio de 2018
  • ABZ 2020, Ulm , Alemania , del 9 al 13 de junio de 2020 (retrasada debido a la pandemia de COVID-19 )
  • ABZ 2021, Ulm, Alemania, del 9 al 13 de junio de 2021
  • ABZ 2023, Nancy , Francia, 30 de mayo – 2 de junio de 2023
  • ABZ 2024, Bérgamo , Italia , 25-28 2024
  • ABZ 2025, Düsseldorf , Alemania, 10 a 13 de junio de 2025
  • ABZ 2026, Tokio , Japón, 18 a 20 de mayo de 2026

Véase también

Referencias

  1. ↑ Cansell, Dominique y Dominique Méry. "Fundamentos del método B". Computing and informatics 22, n.º 3-4 (2003): 221-256.
  2. ↑ Butler, Michael, Philipp Körner, Sebastian Krings, Thierry Lecomte, Michael Leuschel, Luis-Fernando Mejia y Laurent Voisin. «Los primeros veinticinco años de uso industrial del método B». En Conferencia Internacional sobre Métodos Formales para Sistemas Críticos Industriales, págs. 189-209. Springer , Cham, 2020.
  3. ↑ Jean-Raymond Abrial (1988). "The B Tool (Abstract)" (PDF) . En Bloomfield, Robin E.; Marshall, Lynn S.; Jones, Roger B. (eds.). VDM – The Way Ahead, Proc. 2nd VDM-Europe Symposium . Lecture Notes in Computer Science . Vol. 328. Springer. pp. 86–87 . doi : 10.1007/3-540-50214-9_8 . ISBN   978-3-540-50214-2.
  4. ↑ Abrial, JR., Matthew KO Lee, DS Neilson, PN Scharbach e Ib Holm Sørensen. «El método B». En Simposio Internacional de VDM Europa, págs. 398-405. Springer, Berlín, Heidelberg, 1991.
  5. ↑ Bowen, Jonathan P. ; Habrias, Henri (abril–junio 2025). "Jean-Raymond Abrial: Una biografía científica de un pionero de los métodos formales". IEEE Annals of the History of Computing . 48 (2). IEEE Computer Society : 71– 80. arXiv : 2604.07353 . doi : 10.1109/MAHC.2026.3685515 .
  6. ↑ Gerhart, Susan, D. Craigen y Ted Ralston. "Estudio de caso: Sistema de señalización del metro de París". IEEE Software 11, n.º 1 (1994): 32-28.
  7. ↑ Behm, Patrick, Paul Benoit, Alain Faivre y Jean-Marc Meynadier. «METEOR: Una aplicación exitosa de B en un proyecto de gran envergadura». En Simposio Internacional sobre Métodos Formales, págs. 369-387. Springer, Berlín, Heidelberg, 1999.
  8. ↑ Lecomte, Thierry. «Aplicación de un método formal en la industria: una trayectoria de 15 años». En Taller internacional sobre métodos formales para sistemas críticos industriales, págs. 26-34. Springer, Berlín, Heidelberg, 2009.
  9. ↑ Bhattacharya, Sourav; Winter, Victor L., eds. (2012). "8. Historia de B". High Integrity Software. Springer . pág. 40. ISBN 978-1461513919.
  10. 1 2 Bowen, Jonathan (julio de 2022). "Ib Holm Sørensen: Diez años después" (PDF) . FACS FACTS ( 2022–2 ). BCS-FACS : 41–49 . Recuperado el 3 de agosto de 2022 .
  11. ↑ Crichton, Edward (29 de marzo de 2022). " BToolkit ". GitHub.
  12. ↑ Roscoe, Bill (8 de febrero de 2012). " Ib Sorensen – In memoriam ". Departamento de Ciencias de la Computación, Universidad de Oxford , Reino Unido.
  13. ↑ Wordsworth, JB (1996). Ingeniería de software con B. Addison-Wesley. ISBN 978-0201403565
  14. 1 2 3 "Event-B y la plataforma Rodin" . Event-B.org .
  15. ↑ Butler, Michael. "Estructuras de descomposición para el evento B." En Conferencia internacional sobre métodos formales integrados, págs. 20-38. Springer, Berlín, Heidelberg, 2009.
  16. ↑ Abrial, Jean-Raymond. Modelado en Event-B: ingeniería de sistemas y software. Cambridge University Press , 2010.
  17. 1 2 Abrial, Jean-Raymond, Michael Butler, Stefan Hallerstede, Thai Son Hoang, Farhad Mehta y Laurent Voisin. «Rodin: un conjunto de herramientas abiertas para el modelado y el razonamiento en Event-B». International Journal on Software Tools for Technology Transfer 12, n.º 6 (2010): 447–466.
  18. ↑ Hoang, Thai Son, Andreas Fürst y Jean-Raymond Abrial. «Patrones Event-B y su soporte de herramientas». Software & Systems Modeling 12, n.º 2 (2013): 229–244.
  19. ↑ "AtelierB.eu" .
  20. ↑ Mentré, David, Claude Marché, Jean-Christophe Filliâtre y Masashi Asuka. «Cumplimiento de las obligaciones de prueba del Atelier B mediante múltiples probadores automatizados». En Conferencia Internacional sobre Máquinas de Estados Abstractos, Alloy, B, VDM y Z, págs. 238-251. Springer, Berlín, Heidelberg, 2012.
  21. ↑ "The B-Toolkit" . [B-Core (UK) Limited] . 2004. Archivado del original el 12 de octubre de 2004. Consultado el 22 de febrero de 2012 .
  22. ↑ Haughton, Howard y Kevin Lano. Especificación en B: Una introducción al uso del conjunto de herramientas B. World Scientific, 1996.
  23. ↑ Abrial, Jean-Raymond. "La herramienta B". En Simposio Internacional de VDM Europa, págs. 86-87. Springer, Berlín, Heidelberg, 1988.
  24. ↑ Requisitos de B-Toolkit archivados el 12/10/2004 en Wayback Machine
  25. ↑ Crichton, Edward. "Código fuente de B-Toolkit" . GitHub .
  26. ↑ Abrial, J.-R.; Cansell, D. (2003). "Click'n Prove: Pruebas interactivas dentro de la teoría de conjuntos". En Basin, D.; Wolff, B. (eds.). Demostración de teoremas en lógicas de orden superior (TPHOLs) . Lecture Notes in Computer Science . Vol. 2758. Berlín, Heidelberg: Springer. doi : 10.1007/10930755_1 . 
  27. ↑ "¿Qué es ProB?" . Alemania: Heinrich-Heine-Universität Düsseldorf . Consultado el 28 de marzo de 2026 .
  28. ↑ "¿ProB?" . railML.org . Consultado el 28 de marzo de 2026 .
  29. ↑ Abrial, JR. «Un proceso de desarrollo de sistemas con Event-B y la plataforma Rodin». En Conferencia Internacional sobre Métodos de Ingeniería Formal, págs. 1-3. Springer, Berlín, Heidelberg, 2007.
  30. ↑ Aljer, Ammar, Philippe Devienne, Sophie Tison , JL. Boulanger y Georges Mariano. «BHDL: Diseño de circuitos en B». En Actas de la Tercera Conferencia Internacional sobre la Aplicación de la Concurrencia al Diseño de Sistemas, págs. 241-242. IEEE, 2003.
  31. ↑ «Asociación de pilotaje de conferencias B» . librairiecosmopolite.com . Consultado el 27 de julio de 2022 .
  32. ↑ "Conferencias" . ABZ . Consultado el 16 de enero de 2026 .
  • Sitio web de Atelier B
  • Sitio B Grenoble