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 . Fue desarrollado originalmente en la década de 1980 por Jean-Raymond Abrial [1] 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 las principales aplicaciones de sistemas críticos para la seguridad en Europa(como las líneas 14 y 1 del metro de París automático y el cohete Ariane 5 ). Tiene soporte de herramientas robusto y disponible comercialmente para especificación , diseño , prueba y generación de código .
En comparación con Z, B tiene un nivel ligeramente más bajo y está más centrado en el refinamiento del código en lugar de solo en la 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, hay un buen soporte de herramientas para esto. El mismo lenguaje se utiliza en la especificación, el diseño y la programación. Los mecanismos incluyen encapsulación y localidad de datos.
Posteriormente, se ha desarrollado otro método formal llamado Event-B [2] . El evento B se considera una evolución de B (también conocido como B clásico). Es una notación más simple, que es más fácil de aprender y usar [ cita requerida ] . Viene con soporte para herramientas en forma de herramienta Rodin .
Los componentes principales
La notación B depende de la teoría de conjuntos y la lógica de primer orden para especificar diferentes versiones de software que cubren el ciclo completo del desarrollo del proyecto.
Máquina abstracta
En la primera y más abstracta versión, que se llama Abstract Machine , el diseñador debe especificar el objetivo del diseño.
Refinamiento
- Luego, durante un paso de refinamiento, puede 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.
- La nueva versión, que se llama Refinamiento , debe demostrar que es coherente e incluye todas las propiedades de la máquina abstracta.
- El diseñador puede hacer uso de 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 se puede traducir a un lenguaje de programación para su compilación.
Software
B-Toolkit
El B-Toolkit , [3] desarrollado por Ib Holm Sørensen et al. , es una colección de herramientas de programación diseñadas para respaldar el uso de B-Tool, un intérprete matemático basado en la teoría de conjuntos, para los propósitos de una metodología formal de ingeniería de software conocida como el método B.
El kit de herramientas utiliza una interfaz personalizada X Window Motif [4] para la gestión de la GUI y se ejecuta principalmente en los sistemas operativos Linux , Mac OS X y Solaris . Ha sido desarrollado por la empresa británica B-Core (UK) Limited. [5]
El código fuente de B-Toolkit ya está disponible. [6]
Atelier B
Desarrollado por ClearSy, Atelier B [7] es una herramienta industrial que permite el uso operativo del Método B para desarrollar software probado libre de defectos (software formal). Hay dos versiones disponibles: Community Edition disponible para cualquier persona sin ninguna restricción, Maintenance Edition solo para titulares de contratos de mantenimiento.
Se utiliza para desarrollar automatismos de seguridad para los distintos subterráneos 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 .
Libros
- The B-Book: Assigning Programs to Meanings , Jean-Raymond Abrial , Cambridge University Press , 1996. ISBN 0-521-49619-5 .
- El método B: una introducción , Steve Schneider, Palgrave Macmillan , serie Cornerstones of Computing, 2001. ISBN 0-333-79284-X .
- Ingeniería de software con B , John Wordsworth, Addison Wesley Longman , 1996. ISBN 0-201-40356-0 .
- El lenguaje y el método B: una guía para el desarrollo formal práctico , Kevin Lano , Springer-Verlag , serie FACIT, 1996. ISBN 3-540-76033-4 .
- Especificación en B: Introducción utilizando el kit de herramientas B , Kevin Lano , World Scientific Publishing Company , Imperial College Press , 1996. ISBN 1-86094-008-0 .
- Modelado en Event-B: Ingeniería de sistemas y software , Jean-Raymond Abrial , Cambridge University Press , 2010. ISBN 978-0-521-89556-9 .
Conferencias
- Conferencia Z2B, Nantes, Francia, oct. 10-12 de 1995
- Primera Conferencia B, Nantes, Francia, nov. 25-27 1996
- Segunda Conferencia B, Montpellier, Francia, ap. 22-24 1998,
- ZB'2000, York, Reino Unido, 28 de agosto, 2 de septiembre. 2000,
- ZB'2002, Grenoble, Francia, 23-25 de enero. 2002,
- ZB'2003, Turku, Finlandia, 4-6 de junio. 2003
- ZB'05, Guildford, Reino Unido, 2005
- B'2007, Besançon, 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
- Conferencia ABZ: ABZ 2008, British Computer Society, Londres, Reino Unido, 16-18 de septiembre de 2008
- Conferencia ABZ: ABZ 2010, Oxford, Québec, Canadá, 23-25 de febrero de 2010
- Conferencia ABZ: ABZ 2012, Pisa, Italia, 18-22 de junio de 2012
- Conferencia ABZ: ABZ 2014, Toulouse, Francia, 2 a 6 de junio de 2014
- Conferencia ABZ: ABZ 2016, Linz, Austria, 23-27 de mayo de 2016
Ver también
- APCB (Association de Pilotage des Conférences B)
- BHDL
Referencias
- ^ Jean-Raymond Abrial (1988). "La herramienta B (Resumen)" (PDF) . En Robin E. Bloomfield y Lynn S. Marshall y Roger B. Jones (ed.). VDM: el camino a seguir, Proc. 2º Simposio VDM-Europa . Apuntes de conferencias en informática . 328 . Saltador. págs. 86-87. doi : 10.1007 / 3-540-50214-9_8 . ISBN 978-3-540-50214-2.
- ^ Event-B.org - Event-B y la plataforma Rodin .
- ^ "El B-Toolkit" . [B-Core (Reino Unido) Limited] . 2004. Archivado desde el original el 12 de octubre de 2004 . Consultado el 22 de febrero de 2012 .
- ^ Requisitos de B-Toolkit Archivado el 12 de octubre de 2004 en la Wayback Machine.
- ^ "B-Core (Reino Unido) Limited" . Datos de la empresa Rex . Consultado el 22 de febrero de 2012 .
- ^ Código fuente de B-Toolkit
- ^ "AtelierB.eu" .
enlaces externos
- Método B.com : este sitio está diseñado para presentar diferentes trabajos y temas relacionados con el método B, un método formal con prueba
- Atelier B.eu : Atelier B es un taller de ingeniería de sistemas, que permite desarrollar software sin fallas garantizado
- Sitio B Grenoble
Este artículo se basa en material extraído del Diccionario gratuito de informática en línea antes del 1 de noviembre de 2008 e incorporado bajo los términos de "renovación de licencias" de la GFDL , versión 1.3 o posterior.