B-metode - B-Method

Den B-metoden er en metode for utvikling av programvare basert på B , en verktøy-understøttet formelle metode basert på et abstrakt maskin notasjon , som brukes i utviklingen av dataprogramvare . Den ble opprinnelig utviklet på 1980-tallet av Jean-Raymond Abrial i Frankrike og Storbritannia . B er relatert til Z-notasjonen (også opprinnelig fra Abrial) og støtter utvikling av programmeringsspråkkode fra spesifikasjoner. B har blitt brukt i store sikkerhetskritiske systemapplikasjoner i Europa (som de automatiske Paris Métro-linjene 14 og 1 og Ariane 5- raketten). Den har robust, kommersielt tilgjengelig verktøystøtte for spesifikasjoner , design , korrektur og kodegenerering .

Sammenlignet med Z er B litt mer lavt og mer fokusert på raffinering til kode i stedet for bare formell spesifikasjon - derfor er det lettere å implementere en spesifikasjon skrevet i B riktig enn en i Z. Spesielt er det god verktøystøtte for dette. Det samme språket brukes i spesifikasjon, design og programmering. Mekanismer inkluderer innkapsling og datalokalitet.

Deretter er det utviklet en annen formell metode kalt Event-B . Event-B regnes som en evolusjon av B (også kjent som klassisk B). Det er en enklere notasjon, som er lettere å lære og bruke. Den leveres med verktøystøtte i form av Rodin-verktøyet .

Hovedkomponentene

B-notasjon avhenger av mengdeori og førsteordenslogikk for å spesifisere forskjellige versjoner av programvare som dekker hele syklusen av prosjektutvikling.

Abstrakt maskin

I den første og mest abstrakte versjonen, som kalles Abstract Machine , bør designeren spesifisere målet for designet.

Raffinement

  • Så, under et forbedringstrinn, kan han putte spesifikasjonen for å tydeliggjøre målet eller gjøre den abstrakte maskinen mer konkret ved å legge til detaljer om datastrukturer og algoritmer som definerer, hvordan målet oppnås.
  • Den nye versjonen, som heter Refinement , skal bevises å være sammenhengende og inkludere alle egenskapene til den abstrakte maskinen.
  • Designeren kan bruke B-biblioteker for å modellere datastrukturer eller for å inkludere eller importere eksisterende komponenter.

Gjennomføring

  • Raffinementet fortsetter til en deterministisk versjon er oppnådd: Implementeringen .
  • Under alle utviklingstrinnene brukes den samme notasjonen, og den siste versjonen kan oversettes til et programmeringsspråk for kompilering.

Programvare

B-Toolkit

Den B-Toolkit , utviklet av Ib Holm Sørensen et al. , er en samling programmeringsverktøy designet for å støtte bruken av B-Tool, en mengde teoribasert matematisk tolk, for formålet med en formell programvareteknikkmetodikk kjent som B-metoden.

Verktøysettet bruker et tilpasset X Window Motif Interface for GUI-styring og kjører primært på operativsystemene Linux , Mac OS X og Solaris . Den er utviklet av det britiske selskapet B-Core (UK) Limited.

B-Toolkit-kildekoden er nå tilgjengelig.

Atelier B

Atelier B er utviklet av ClearSy, og er et industrielt verktøy som muliggjør operativ bruk av B-metoden for å utvikle feilfri dokumentert programvare (formell programvare). To versjoner er tilgjengelige: Community Edition tilgjengelig for alle uten begrensninger, Maintenance Edition kun for vedlikeholdskontraktsinnehavere.

Den brukes til å utvikle sikkerhetsautomatiseringer for de forskjellige undergrunnsbanene som er installert over hele verden av Alstom og Siemens , og også for Common Criteria-sertifisering og utvikling av systemmodeller av ATMEL og STMicroelectronics .

Bøker

  • B-boken: Tilordne programmer til betydninger , Jean-Raymond Abrial , Cambridge University Press , 1996. ISBN  0-521-49619-5 .
  • The B-Method: An Introduction , Steve Schneider, Palgrave Macmillan , Cornerstones of Computing series, 2001. ISBN  0-333-79284-X .
  • Software Engineering med B , John Wordsworth, Addison Wesley Longman , 1996. ISBN  0-201-40356-0 .
  • B-språket og metoden: En guide til praktisk formell utvikling , Kevin Lano , Springer-Verlag , FACIT-serien, 1996. ISBN  3-540-76033-4 .
  • Spesifikasjon i B: En introduksjon ved bruk av B Toolkit , Kevin Lano , World Scientific Publishing Company , Imperial College Press , 1996. ISBN  1-86094-008-0 .
  • Modellering i Event-B: System- og programvareteknikk , Jean-Raymond Abrial , Cambridge University Press , 2010. ISBN  978-0-521-89556-9 .

Konferanser

  • Konferanse Z2B, Nantes, Frankrike, okt. 10-12 1995
  • Første B-konferanse, Nantes, Frankrike, nov. 25-27 1996
  • Andre B-konferanse, Montpellier, Frankrike, ap. 22-24 1998,
  • ZB'2000, York, Storbritannia, 28. august, 2. sept. 2000,
  • ZB'2002, Grenoble, Frankrike, 23.-25. Jan. 2002,
  • ZB'2003, Turku, Finland, 4-6 jun. 2003
  • ZB'05, Guildford, Storbritannia, 2005
  • B'2007, Besançon, Frankrike, 2007
  • B, fra forskning til undervisning, Nantes, Frankrike, 16. juni 2008
  • B, fra forskning til undervisning, Nantes, Frankrike, 8. juni 2009
  • B, fra forskning til undervisning, Nantes, Frankrike, 7. juni 2010
  • ABZ-konferanse: ABZ 2008, British Computer Society, London, Storbritannia, 16. – 18. September 2008
  • ABZ-konferanse: ABZ 2010, Oxford, Québec, Canada, 23. – 25. Februar 2010
  • ABZ-konferanse: ABZ 2012, Pisa, Italia, 18. – 22. Juni 2012
  • ABZ-konferanse: ABZ 2014, Toulouse, Frankrike, 2. – 6. Juni 2014
  • ABZ-konferanse: ABZ 2016, Linz, Østerrike, 23. – 27. Mai 2016

Se også

  • APCB (Association de Pilotage des Conférences B)
  • BHDL

Referanser

Eksterne linker

  • B Method.com : dette nettstedet er utformet for å presentere forskjellige arbeider og emner angående B-metoden, en formell metode med bevis
  • Atelier B.eu : Atelier B er et systemteknisk verksted som gjør det mulig å utvikle programvare som garantert er feilfri
  • Nettsted B Grenoble

Denne artikkelen er basert på materiale hentet fra Free On-line Dictionary of Computing før 1. november 2008 og innlemmet under "relisensing" -vilkårene i GFDL , versjon 1.3 eller nyere.