Menetelmä B

Tämän artikkelin sisältö tietokoneissa on tarkistettava (joulukuu 2016).

Paranna sitä tai keskustele tarkistettavista asioista . Jos olet juuri kiinnittänyt bannerin, ilmoita tarkistettavat kohdat täällä .

B-menetelmä on muodollinen menetelmä , jonka avulla perustelut noin monimutkaisia järjestelmiä sekä ohjelmistokehitys .

Menetelmä B mahdollistaa mallintamisen abstraktilla tavalla ohjelmiston käyttäytymisen ja spesifikaatiot B-kielellä, ja sitten peräkkäisillä tarkennuksilla päästä konkreettiseen malliin Adan tai C : n koodattavan kielen B osajoukossa , jonka suorittaa betonikone. Sen avulla järjestelmä ja sen ympäristö voidaan muodostaa abstraktilla tavalla, sitten peräkkäisillä tarkennuksilla lisätä yksityiskohdat järjestelmän malliin. Muodollinen todistustoiminta mahdollistaa abstraktin mallin yhdenmukaisuuden ja kunkin tarkennuksen yhteensopivuuden ylivoimaisen mallin kanssa (mikä osoittaa kaikkien konkreettisten toteutusten yhdenmukaisuuden abstraktin mallin kanssa).

Erotamme:

B: n historia

B-kielen on suunnitellut JRAbrial , joka oli yksi Z: n pääsuunnittelijoista 1980-luvulla G. Laffitte, F. Mejia ja I. Mc Nealin avustamana. Se perustuu EW Dijkstran , CAR Hoaren , CB Jonesin, C.Morganin ja He Jifengin (ohjelmoinnin tutkimusryhmän Oxfordin yliopistosta) tieteelliseen työhön .

B on osa pitkää perustutkimusta:

Ensimmäinen B-konferenssi pidettiin Ranskassa Nantesissa 25.26.27. marraskuuta vuonna 1996.

Menetelmää B on käytetty menestyksekkäästi useissa teollisissa sovelluksissa. Voimme mainita Pariisin metron ( METEOR ) linjan 14 sisäisen ohjelmiston kehittämisen, joka on mallinnettu, todistettu ja luotu muodollisista B-spesifikaatioista. Vuonna 2005 RATP päätti automatisoida linjan 1 ja vetoaa uudelleen menetelmään B. -tauluohjelmisto. Vuodesta 1995 lähtien on kehitetty monia metropysäkkejä, erityisesti Barcelona, ​​Delhi, Lausanne, Madrid, New York, Peking (olympialaisten yhteydessä), Soul ja Singapore. Charles de Gaullen lentokenttäkuljetuksen kantonin autopilotti on osa B-kehitystä. Lopuksi useat kehitteillä olevat tai uusittavat metrot käyttävät B-menetelmää aluksen ohjelmistojen kehittämiseen: Istanbul, Kairo, Milano, Sao Paulo, Shanghai tai jopa Toronto.

Vuonna 1996 JR Abrial julkaisi B-kirjan, Ohjelmien liittäminen merkityksiin . Vuonna 2010 hän julkaisi toisen kirjan tapahtumasta B: Mallinnus Event-B: ssä, kovakantinen .

B: n tavoitteet

Puhtaasti teoreettisesta näkökulmasta menetelmän B tavoitteena on todistaa, että määrityksen ja suoritetun koodin välillä ei ole aukkoa.

Vaikka testipohjaiset menetelmät sanovat vain, että testaajat eivät löytäneet mitään; ja tämä riippumatta testiskenaarioiden luomisen ja toteutettujen keinojen automatisointitasosta.

Siten ajan ja varojen puute (teollisuuden voimakas rajoitus) johtaa käyttökelvottomaan ohjelmaan (koska sitä ei ole osoitettu), jossa kilpailevat menetelmät johtavat "virheellisiin" ohjelmiin.

Tämän seurauksena loppukäyttäjä tai sponsori voi luottaa ohjelmaan hyvin. Tämä luottamus on erityisen välttämätöntä, jopa pakollista, liikennealalla, erityisesti ilmailualalla, jonka standardi on DO-178B, tai rautateillä (CENELEC EN 50128), koska käyttäjien turvallisuus on välttämätöntä.

B kattaa määrittelyn, suunnittelun peräkkäisillä tarkennuksilla, kerrostetun arkkitehtuurin ja käännöksen lähdekoodiksi (esimerkki: Ada, C); tämä mahdollistaa korkean tason optimointien toteuttamisen; esimerkiksi :

B ei kata lopullisen suoritettavan ohjelman (esim. Exe) luomista ja siten matalan tason optimointia, jättäen tämän erikoistuneille kääntäjille.

Esimerkkejä

Esimerkki abstraktista koneesta ja sen hienostuneisuudesta

Käytimme B: n ASCII-merkintää (":" edustaa joukon jäsenyyttä, "<:" sisällyttäminen "&" the "ja" looginen ": ::" "tulee" -joukkoon (epäselvä valinta joukon elementistä) , ”||” rinnakkaiskorvaus.) ”NAT” vastaa luonnollisten lukujen joukkoa.

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

Esimerkki koneen koostumuksen primitiivien käytöstä, SEES ja 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

Kansainväliset konferenssit B.

Viitteet

  1. JR. Abrial ja Dominique.Cansell, "  Click'n Prove: Interactive Proofs Within Theory Theory  ", Lause, joka osoittaa korkeamman asteen logiikkaa , Springer Berlin Heidelberg,2003, s.  1-24 ( lue verkossa )
  2. Jean-Raymond Abrial, B-kirja, ohjelmien liittäminen merkityksiin , Cambridge University Press, 1996, ( ISBN  0521496195 )
  3. http://www.atelierb.eu/  : kehitystyökalu B: ssä
  4. http://www.b-core.com/btoolkit.html  : kehitystyökalu B: ssä
  5. http://rodin-b-sharp.sourceforge.net/  : Rodin-projekti, jonka tavoitteena on kehittää avoin kehitysalusta

Bibliografia

  • Bibliografinen laskenta BibTeX-muodossa ( ulkoinen linkki )
  • B-kirja, Ohjelmien liittäminen merkityksiin , Cambridge University Press, Cambridge, 1996, ( ISBN  0521496195 ) , B-menetelmän perustyö .
  • Muodolliset menetelmät teollisiin sovelluksiin: höyrykattilan ohjauksen määrittely ja ohjelmointi, LNCS, Springer, 1997
  • Steve Schneider, B-menetelmä, johdanto , Palgrave, 2001, ( ISBN  033379284X ) ( ulkoinen linkki )
  • E. Sekerinski ja K. Sere (toimittajat), tapaustutkimukset B-menetelmällä , Springer, ( ISBN  0-52149619-5 )
  • John Wordsworth, ohjelmistotuotanto, B , Addison-Wesley ( ISBN  0201403560 )
  • Kevin Lano, B-kieli ja menetelmä: Opas käytännön muodolliseen kehitykseen , Springer Verlag London Ltd., ( ISBN  3-540-76033-4 )
  • Henri Habrias et ai., Virallinen erittely B: n kanssa , Hermes Lavoisier, ( ISBN  2-7462-0302-2 ) ( [1] )
  • JR Abrial, B: n laajentaminen muuttamatta sitä julkaisussa H.Habrias (edit), First B Conference, s. 160 - 170, 1996
  • JR Abrial, B-johdantokurssi, tapaustutkimukset sekä logiikka- ja todistuskurssi , videokasetit, jakelija IUT de Nantesin IT-osasto, 1997
  • JR Abrial, Modeling in Event-B, kovakantinen , Cambridge University Press, 2010, ( ISBN  9780521895569 ) ( [2] )
  • JR Abrial, kiinalainen B-kirja http://www.china-pub.com/19779

Aiheeseen liittyvät artikkelit

  • B-Toolkit , B-Core-yrityksen kehittämä työkalu

Ulkoiset linkit

Työkalut

  • ABTools Toinen B-työkalu: B-työkalupaketti, joka on kehitetty ANTLR: n avulla
  • Workshop B  : teollinen työkalu, joka mahdollistaa menetelmän B operatiivisen käytön ohjelmistokehitykseen.
  • B4free on AtelierB-ytimen ilmainen [vanhentunut] versio, jota käytetään Click'n Prove -palvelun kanssa. Hänet on korvattu vuodestaHelmikuu 2009 kirjoittanut Atelier B. -versioversio
  • Bart  : automaattinen tarkennustyökalu
  • Brama Graafinen mallinnustyökalu, jota käytetään muodollisiin menetelmiin. B.
  • ComenC B-mallien kääntäjä C-kielelle.
  • CompoSys- menetelmä ja työkalu järjestelmien virallisille kuvauksille.
  • RODIN , B-tapahtuma-alusta, joka perustuu Eclipseen
  • ABtyökalut
  • BATCAVE
  • BRILLANT : avoimen lähdekoodin kehitysprojekti työkaluille, jotka tukevat B-menetelmää.
  • jBtools
  • DumBeX B merkintöjen kääntäjälleLateksi