Método B
Método de desarrollo de software

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

Descripción general

B fue desarrollado originalmente en la década de 1980 por Jean-Raymond Abrial [3] [4] en Francia y el Reino Unido . 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 ). [5] [6] [7] Tiene un soporte de herramientas sólido y disponible comercialmente para especificación , diseño , prueba y generación de código .

En comparación con Z, B es un poco más de bajo nivel 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, existe un buen soporte de herramientas para esto. Se utiliza el mismo lenguaje en la especificación, el diseño y la programación. Los mecanismos incluyen la encapsulación y la localización de datos.

Evento-B

Posteriormente, se desarrolló otro método formal llamado Event-B [8] [9] [10] basado en el Método B, con el apoyo de la Plataforma Rodin. [11] [12] Event-B es un método formal destinado 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 de refinamiento para representar sistemas en diferentes niveles de abstracción y el uso de prueba matemática para verificar la consistencia entre estos niveles de refinamiento.

Los componentes principales

La notación B depende de la teoría de conjuntos y de la lógica de primer orden para especificar diferentes versiones de software que cubren el ciclo completo de desarrollo del proyecto.

Máquina abstracta

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

Refinamiento

  • Luego, durante un paso de refinamiento, pueden rellenar la especificación para aclarar el objetivo o hacer que la máquina abstracta sea más concreta agregando detalles sobre estructuras de datos y algoritmos que definen cómo se logra el objetivo.
  • Se debe demostrar que la nueva versión, llamada Refinamiento , es coherente e incluye todas las propiedades de la máquina abstracta.
  • El diseñador puede hacer uso de las 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 todos los pasos 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

B-Kit de herramientas

El B-Toolkit [13] [14] es una colección de herramientas de programación diseñadas para respaldar el uso de B-Tool, [15] es un intérprete matemático basado en la teoría de conjuntos, con el propósito de respaldar el B-Method. El desarrollo fue realizado originalmente por Ib Holm Sørensen y otros, en BP Research y luego en B-Core (UK) Limited. [16]

El kit de herramientas utiliza una interfaz Motif X Window personalizada [17] para la gestión de la GUI y se ejecuta principalmente en los sistemas operativos Linux , Mac OS X y Solaris .

El código fuente de B-Toolkit ya está disponible. [18]

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 libre de defectos (software formal). Hay dos versiones disponibles: 1) Community Edition disponible para cualquier persona sin ninguna restricción; 2) Maintenance Edition 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 Common Criteria y el desarrollo de modelos de sistemas por ATMEL y STMicroelectronics .

Rodin

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

BHDL

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. [22]

APCB

APCB ( en francés : Association de Pilotage des Conférences B , Comité Directivo de la Conferencia Internacional B ) ha organizado reuniones asociadas con el Método B. [23] Ha organizado conferencias ZB con el Grupo de Usuarios Z y conferencias ABZ, incluidas las Máquinas de Estados Abstractos (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:

  • 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 enseñanza, Nantes, Francia, 16 de junio de 2008
  • B, De la investigación a la enseñanza, Nantes, Francia, 8 de junio de 2009
  • B, De la investigación a la enseñanza, Nantes, Francia, 7 de junio de 2010
  • ABZ 2008, British Computer Society , 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, 2018
  • ABZ 2020, Ulm , Alemania , 2021 (retrasado debido a la pandemia de COVID-19 )
  • ABZ 2021, Ulm, Alemania, 2021

Véase también

Referencias

  1. ^ Cansell, Dominique y Dominique Méry. "Fundamentos del método B". Computing and informatics 22, no. 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 la Conferencia Internacional sobre Métodos Formales para Sistemas Críticos Industriales, págs. 189-209. Springer , Cham, 2020.
  3. ^ Jean-Raymond Abrial (1988). "La herramienta B (Resumen)" (PDF) . En Bloomfield, Robin E.; Marshall, Lynn S.; Jones, Roger B. (eds.). VDM: el camino a seguir, Proc. 2.º Simposio VDM-Europe . Apuntes de conferencias sobre informática . Vol. 328. Springer. págs. 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 y Ib Holm Sørensen. "El método B". En el Simposio Internacional de VDM Europe, págs. 398-405. Springer, Berlín, Heidelberg, 1991.
  5. ^ Gerhart, Susan, D. Craigen y Ted Ralston. "Estudio de caso: sistema de señalización del metro de París". IEEE Software 11, núm. 1 (1994): 32-28.
  6. ^ Behm, Patrick, Paul Benoit, Alain Faivre y Jean-Marc Meynadier. "METEOR: Una aplicación exitosa de B en un gran proyecto". En Simposio Internacional sobre Métodos Formales, págs. 369-387. Springer, Berlín, Heidelberg, 1999.
  7. ^ 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.
  8. ^ abc "Event-B y la Plataforma Rodin". Event-B.org .
  9. ^ Butler, Michael. "Estructuras de descomposición para Event-B". En la Conferencia Internacional sobre Métodos Formales Integrados, págs. 20-38. Springer, Berlín, Heidelberg, 2009.
  10. ^ Abrial, Jean-Raymond. Modelado en Event-B: ingeniería de sistemas y software. Cambridge University Press , 2010.
  11. ^ ab Abrial, Jean-Raymond, Michael Butler, Stefan Hallerstede, Thai Son Hoang, Farhad Mehta y Laurent Voisin. "Rodin: un conjunto de herramientas abierto para modelado y razonamiento en Event-B". Revista internacional sobre herramientas de software para transferencia de tecnología 12, n.º 6 (2010): 447-466.
  12. ^ Hoang, Thai Son, Andreas Fürst y Jean-Raymond Abrial. "Patrones Event-B y sus herramientas de apoyo". Software & Systems Modeling 12, n.º 2 (2013): 229-244.
  13. ^ "El kit de herramientas B". [B-Core (UK) Limited] . 2004. Archivado desde el original el 12 de octubre de 2004 . Consultado el 22 de febrero de 2012 .
  14. ^ Haughton, Howard y Kevin Lano. Especificación en B: Una introducción utilizando el conjunto de herramientas B. World Scientific, 1996.
  15. ^ Abrial, Jean-Raymond. "La herramienta B". En Simposio internacional de VDM Europe, págs. 86-87. Springer, Berlín, Heidelberg, 1988.
  16. ^ Bowen, Jonathan (julio de 2022). "Ib Holm Sørensen: diez años después" (PDF) . FACS FACTS . N.º 2022–2. BCS-FACS . págs. 41–49 . Consultado el 3 de agosto de 2022 .
  17. ^ Requisitos de B-Toolkit Archivado el 12 de octubre de 2004 en Wayback Machine.
  18. ^ Crichton, Edward. "Código fuente de B-Toolkit". GitHub .
  19. ^ "AtelierB.eu".
  20. ^ Mentré, David, Claude Marché, Jean-Christophe Filliâtre y Masashi Asuka. "Descarga de obligaciones de prueba de Atelier B utilizando múltiples probadores automatizados". En la Conferencia internacional sobre máquinas de estados abstractos, Alloy, B, VDM y Z, págs. 238-251. Springer, Berlín, Heidelberg, 2012.
  21. ^ Abrial, JR. "Un proceso de desarrollo de sistemas con Event-B y la plataforma Rodin". En la Conferencia internacional sobre métodos formales de ingeniería, págs. 1-3. Springer, Berlín, Heidelberg, 2007.
  22. ^ Aljer, Ammar, Philippe Devienne, Sophie Tison, JL. Boulanger y Georges Mariano. "BHDL: Diseño de circuitos en B". En la Tercera Conferencia Internacional sobre la Aplicación de la Concurrencia al Diseño de Sistemas, 2003. Actas, págs. 241-242. IEEE, 2003.
  23. ^ "Asociación de pilotaje de conferencias B". librairiecosmopolite.com . Consultado el 27 de julio de 2022 .
  • B Method.com – trabajos y temas relacionados con el método B, un método formal con pruebas
  • Atelier B.eu Archivado el 21 de febrero de 2008 en Wayback Machine : Atelier B es un taller de ingeniería de sistemas que permite desarrollar software con garantía de impecabilidad.
  • Sitio B Grenoble
Obtenido de "https://es.wikipedia.org/w/index.php?title=Método B&oldid=1253211181"