Metoda B

Podstatou tohoto článku na počítačích, je třeba zkontrolovat (prosince 2016).

Vylepšete to nebo diskutujte o věcech, které chcete zkontrolovat . Pokud jste právě připojili banner, zde označte body, které chcete zkontrolovat .

Metoda B je formální metoda, která umožňuje uvažování o složitých systémech i o vývoji softwaru .

Metoda B umožňuje modelovat abstraktním způsobem chování a specifikace softwaru v jazyce B, poté postupným vylepšováním dospět ke konkrétnímu modelu v podmnožině jazyka B transkódovatelného v Adě nebo v C , spustitelném pomocí betonový stroj. Umožňuje formalizovat systém a jeho prostředí abstraktním způsobem, poté postupnými zdokonaleními a přidáním podrobností k modelu systému. Činnost formálního dokazování umožňuje ověřit soulad abstraktního modelu a shodu každé upřesnění s nadřazeným modelem (což dokazuje soulad všech konkrétních implementací s abstraktním modelem).

Rozlišujeme:

Historie B.

Jazyk B navrhl JRAbrial , který byl jedním z hlavních designérů Z v 80. letech, za pomoci G. Laffitteho, F. Mejie a I. Mc Neala. Je založen na vědecké práci EW Dijkstra , CAR Hoare , CB Jones, C. Morgan, He Jifeng (z Programming Research Group University of Oxford).

B je součástí dlouhé řady základního výzkumu:

První konference o B se konala ve Francii v Nantes dne 25.26,27. listopadu v roce 1996.

Metoda B byla úspěšně použita pro několik průmyslových aplikací. Můžeme citovat vývoj palubního softwaru pro linku 14 pařížského metra ( METEOR ), který byl modelován, osvědčen a generován z formálních specifikací B. V roce 2005 se RATP rozhodl automatizovat linku 1 a znovu se odvolal na metodu B pro - palubní software. Od roku 1995 bylo vyvinuto mnoho autopilotů metra, zejména Barcelona, ​​Dillí, Lausanne, Madrid, New York, Peking (u příležitosti olympijských her), Soul a Singapur. Kantonový autopilot kyvadlové dopravy na letišti Charlese de Gaulla je součástí vývoje B. A konečně několik vyvíjených nebo renovovaných metropolitních oblastí používá metodu B pro vývoj palubního softwaru: Istanbul, Káhira, Milán, Sao Paulo, Šanghaj nebo dokonce Toronto.

V roce 1996 vydal JR Abrial knihu B, Přiřazení programů významům . V roce 2010 vydal další knihu o události B: Modeling in Event-B, Hardback .

Cíle B.

Z čistě teoretického hlediska je cílem metody B dokázat, že mezi specifikací a provedeným kódem není mezera.

Zatímco metody založené na testech jen říkají, že testeři žádné nenašli; a to bez ohledu na úroveň automatizace generování testovacích scénářů a implementovaných prostředků.

Nedostatek času a prostředků (silné omezení v průmyslu) tedy povede k nepoužitelnému programu (protože není prokázán), kde konkurenční metody vedou k „odposlouchávaným“ programům.

Výsledkem je, že koncový uživatel nebo sponzor může mít v program velkou důvěru. Tato důvěra je obzvláště nezbytná, dokonce povinná v odvětví dopravy, zejména v letectví se standardem DO-178B nebo v železnici (CENELEC EN 50128), protože bezpečnost uživatelů je zásadní.

B pokrývá specifikaci, design postupným vylepšováním, vrstvenou architekturu a překlad do zdrojového kódu (příklad: Ada, C); to umožňuje implementaci optimalizací na „vysoké úrovni“; například :

B nepokrývá generování konečného spustitelného programu (např. .Exe), a proto optimalizaci na nízké úrovni, přičemž toto ponechává na specializované kompilátory.

Příklady

Příklad abstraktního stroje a jeho zdokonalení

Použili jsme ASCII notaci B (":" představuje členství v sadě, "<:" zahrnutí, "&" the "a" logické, "::" the "stává se patří" (indeterministická volba prvku sady) , „||“ paralelní substituce.) „NAT“ odpovídá množině přirozených čísel.

MACHINE swap VARIABLES xx, yy INVARIANT xx : NAT & yy : NAT INITIALISATION xx :: NAT || yy :: NAT OPERATIONS echange = BEGIN xx := yy || yy := xx END END /* La substitution séquencement est interdite dans les machines abstraites, ceci afin de forcer à l'abstraction */ REFINEMENT swapR REFINES swap VARIABLES xr, yr, zr INVARIANT xr= xx & yr = yy & zr : NAT INITIALISATION xr, yr, zr:= 0, 0, 0 OPERATIONS echange = BEGIN zr := xr ; xr := yr ; yr := zr END END

Příklad použití primitiv pro strojové složení, SEES a INCLUDES

MACHINE trucM4(AA, maxe) /* machine paramétrée par un SET et un scalaire */ CONSTRAINTS maxe : 5..10 & card(AA) >maxe VARIABLES var INVARIANT var <: AA & card(var) < maxe +1 INITIALISATION var := {} OPERATIONS trucM1op = ANY ens WHERE ens <: AA & card(ens) < maxe+ 1 THEN var := ens END END MACHINE trucM5(AA,maxe) CONSTRAINTS maxe : 5..10 & card(AA)> maxe INCLUDES tien.trucM4(AA, maxe), mon.trucM4(AA, maxe) OPERATIONS optrucM2 = BEGIN tien.trucM1op || mon.trucM1op END END

Mezinárodní konference o B

Reference

  1. JR. Abrial a Dominique.Cansell, „  Click'n Prove: Interactive Proofs Within Set Theory  “, věta dokazující logiku vyššího řádu , Springer Berlin Heidelberg,2003, str.  1–24 ( číst online )
  2. Jean-Raymond Abrial, B-Book, Přiřazení programů významům , Cambridge University Press, 1996, ( ISBN  0521496195 )
  3. http://www.atelierb.eu/  : vývojový nástroj v B.
  4. http://www.b-core.com/btoolkit.html  : vývojový nástroj v B.
  5. http://rodin-b-sharp.sourceforge.net/  : Projekt Rodin, jehož cílem je vyvinout otevřenou vývojovou platformu

Bibliografie

  • Bibliografický sčítání ve formátu BibTeX ( externí odkaz )
  • Kniha B, Přiřazení programů významům , Cambridge University Press, Cambridge, 1996, ( ISBN  0521496195 ) , zakládající práce metody B.
  • Formální metody pro průmyslové aplikace: Specifikace a programování ovládání parního kotle, LNCS, Springer, 1997
  • Steve Schneider, The B-method, an Introduction , Palgrave, 2001, ( ISBN  033379284X ) ( externí odkaz )
  • E. Sekerinski a K. Sere (redaktoři), Případové studie využívající metodu B , Springer, ( ISBN  0-52149619-5 )
  • John Wordsworth, Softwarové inženýrství s B , Addison-Wesley, ( ISBN  0201403560 )
  • Kevin Lano, The B Language and Method: A Guide to Practical Formal Development , Springer Verlag London Ltd., ( ISBN  3-540-76033-4 )
  • Henri Habrias et al., Formální specifikace s B , Hermes Lavoisier, ( ISBN  2-7462-0302-2 ) ( [1] )
  • JR Abrial, Rozšíření B beze změny v H. Habrias (editovat), První B konference, str. 160-170, 1996
  • JR Abrial, Úvodní kurz k B, Případové studie a Kurz logiky a důkazu , Videokazety, distribuováno IT oddělením IUT v Nantes, 1997
  • JR Abrial, Modeling in Event-B, Hardback , Cambridge University Press, 2010, ( ISBN  9780521895569 ) ( [2] )
  • JR Abrial, The B Book in Chinese http://www.china-pub.com/19779

Související články

  • B-Toolkit , nástroj vyvinutý společností B-Core

externí odkazy

Nástroje

  • ABTools Another B Tool: sada nástrojů B vyvinutých s ANTLR
  • Workshop B  : průmyslový nástroj umožňující operativní využití metody B pro vývoj softwaru.
  • B4free je bezplatná [zastaralá] verze jádra AtelierB, kterou lze použít s Click'n Prove. Od té doby byl nahrazenÚnor 2009 komunitní verzí ateliéru B.
  • Bart  : nástroj pro automatické zdokonalování
  • Nástroj Brama Graphic Modeling aplikovaný na formální metody. B.
  • ComenC Překladač modelů B do jazyka C.
  • CompoSys Metoda a nástroj pro formální popis systémů.
  • RODIN , platforma B-event založená na Eclipse
  • ABtools
  • BATCAVE
  • BRILLANT : vývojový projekt open-source pro nástroje podporující metodu B.
  • jBtools
  • Překladač DumBeX B na notaci\Latex