Yöntem B

Bu makalenin bilgisayarlardaki içeriği kontrol edilmelidir (Aralık 2016).

İyileştirin veya kontrol edilecek şeyleri tartışın . Pankartı yeni eklediyseniz, lütfen kontrol etmeniz gereken noktaları burada belirtin .

B yöntemi bir olan biçimsel yöntem hakkında akıl veriyor karmaşık sistemler yanı sıra yazılım geliştirme .

Metot B, bir yazılımın davranışını ve özelliklerini B dilinde soyut bir şekilde modellemeyi, ardından Ada veya C'de kod dönüştürülebilir B dilinin bir alt kümesinde somut bir modele ulaşmak için ardışık iyileştirmelerle veya C , yürütülebilir olarak modellemeyi mümkün kılar. beton bir makine ile. Sistemi ve çevresini soyut bir şekilde resmileştirmeye, ardından ardışık iyileştirmelerle, ayrıntıları sistem modeline eklemeye izin verir. Biçimsel bir ispat faaliyeti, soyut modelin tutarlılığını ve her iyileştirmenin üstün modele uygunluğunu doğrulamayı mümkün kılar (böylece tüm somut uygulamaların soyut modele uygunluğunu kanıtlar ).

Biz ayırt ediyoruz:

B'nin tarihi

B dili, 1980'lerde Z'nin ana tasarımcılarından biri olan JRAbrial tarafından G. Laffitte, F. Mejia ve I. Mc Neal'ın yardımıyla tasarlandı. EW Dijkstra , CAR Hoare , CB Jones, C. Morgan, He Jifeng'in (Oxford Programlama Araştırma Grubu Üniversitesi'nden) bilimsel çalışmasına dayanmaktadır .

B, uzun bir temel araştırmanın parçasıdır:

B ile ilgili ilk konferans 25.26'da Fransa'da Nantes'te gerçekleşti,27 Kasım 1996'da.

Yöntem B, çeşitli endüstriyel uygulamalar için başarıyla kullanılmıştır. Resmi B spesifikasyonlarından modellenen, kanıtlanan ve üretilen Paris metrosunun ( METEOR ) 14. hattı için yerleşik yazılımın geliştirilmesinden bahsedebiliriz . 2005 yılında, RATP 1. hattı otomatikleştirmeye karar verdi ve -board yazılımı. 1995'ten beri Barselona, ​​Delhi, Lozan, Madrid, New York, Pekin (Olimpiyat Oyunları vesilesiyle), Seul ve Singapur dahil olmak üzere birçok metro otopilotları geliştirildi. Charles de Gaulle havaalanı servisinin kanton otopilotu, B gelişmelerinin bir parçasıdır.Son olarak, geliştirilmekte veya yenilenmekte olan birkaç metro, yerleşik yazılımın geliştirilmesi için B yöntemini kullanır: İstanbul, Kahire, Milano, Sao Paulo, Şangay ve hatta Toronto.

1996'da JR Abrial , anlamlara programlar atamak için B-Kitap yayınladı . 2010'da B olayı üzerine başka bir kitap yayınladı: Event-B'de Modeling, Hardback .

B'nin Hedefleri

Tamamen teorik bir bakış açısından, B yönteminin amacı, şartname ile yürütülen kod arasında bir boşluk olmadığını kanıtlamaktır.

Test tabanlı yöntemler sadece testçilerin bulamadıklarını söylese de; ve bu, test senaryolarının üretilmesinin otomasyon seviyesi ve uygulanan araçlar ne olursa olsun.

Bu nedenle, zaman ve araç eksikliği (endüstrideki güçlü kısıtlama), rakip yöntemlerin "hatalı" programlara yol açtığı, kullanılamaz bir programa (çünkü kanıtlanmadığı için) yol açacaktır.

Sonuç olarak, son kullanıcı veya sponsor programa büyük bir güven duyabilir. Bu güven özellikle ulaştırma sektöründe, özellikle standart DO- 178B'ye sahip havacılıkta veya demiryollarında (CENELEC EN 50128) kullanıcı güvenliği çok önemli olduğundan zorunludur, hatta zorunludur .

B, spesifikasyon, ardışık iyileştirmelerle tasarım, katmanlı mimari ve kaynak koduna çeviriyi kapsar (örnek: Ada, C); bu, "yüksek seviyeli" optimizasyonların uygulanmasına izin verir; Örneğin :

B, son çalıştırılabilir programın (örn. .Exe) oluşturulmasını ve dolayısıyla düşük seviyeli optimizasyonu kapsamaz ve bunu özel derleyicilere bırakır.

Örnekler

Soyut bir makine ve onun iyileştirilmesine bir örnek

B'nin ASCII gösterimini kullandık (":" küme üyeliğini temsil eder, "<:" dahil etme "&" the "ve" mantıksal "::" "aittir" (bir kümenin bir öğesinin belirsiz seçimi) , "||" paralel ikame.) "NAT", doğal sayılar kümesine karşılık gelir.

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

Makine bileşimi ilkelleri, SEES ve INCLUDES kullanımına bir örnek

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

B üzerine uluslararası konferanslar

Referanslar

  1. JR. Abrial and Dominique.Cansell, "  Click'n Prove: Interactive Proofs within Set Theory  ", Teorem yüksek mertebeden mantıkla kanıtlıyor , Springer Berlin Heidelberg,2003, s.  1-24 ( çevrimiçi okuyun )
  2. Jean-Raymond Abrial, The B-Book, Atanma Programları Anlamlara , Cambridge University Press, 1996, ( ISBN  0521496195 )
  3. http://www.atelierb.eu/  : B'de bir geliştirme aracı
  4. http://www.b-core.com/btoolkit.html  : B'de bir geliştirme aracı
  5. http://rodin-b-sharp.sourceforge.net/  : Açık bir geliştirme platformu geliştirmeyi amaçlayan Rodin projesi

Kaynakça

  • BibTeX biçiminde bibliyografik sayım ( harici bağlantı )
  • The B Book, Assigning Programs to Anlamları , Cambridge University Press, Cambridge, 1996, ( ISBN  0521496195 ) , B yönteminin kurucu çalışması.
  • Endüstriyel Uygulamalar için Biçimsel Yöntemler: Buhar Kazanı Kontrolünün Belirlenmesi ve Programlanması, LNCS, Springer, 1997
  • Steve Schneider, B-yöntemi, bir giriş , Palgrave, 2001, ( ISBN  033379284X ) ( harici bağlantı )
  • E. Şekerinski ve K. Sere (editörler), B Yöntemini Kullanan Örnek Olaylar , Springer, ( ISBN  0-52149619-5 )
  • John Wordsworth, B ile Yazılım Mühendisliği , 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 ve diğerleri, B , Hermes Lavoisier ile resmi belirtim , ( ISBN  2-7462-0302-2 ) ( [1] )
  • JR Abrial, B'yi değiştirmeden genişletmek , H. Habrias (değiştir), First B Conference, s. 160-170, 1996
  • JR Abrial, B'ye Giriş kursu, Vaka çalışmaları ve Mantık ve Kanıt kursu , Video kasetler, IUT de Nantes BT departmanı tarafından dağıtılır, 1997
  • JR Abrial, Event-B'de Modelleme, Hardback , Cambridge University Press, 2010, ( ISBN  9780521895569 ) ( [2] )
  • JR Abrial, Çince B Kitabı http://www.china-pub.com/19779

İlgili Makaleler

  • B-Toolkit , B-Core şirketi tarafından geliştirilen araç

Dış bağlantılar

Aletler

  • ABTools Another B Tool: ANTLR ile geliştirilen B araçları paketi
  • Atölye B  : Yazılım geliştirmeleri için B yönteminin operasyonel kullanımına izin veren endüstriyel araç.
  • B4free , Click'n Prove ile kullanılmak üzere atelierB çekirdeğinin ücretsiz [eski] sürümüdür. O zamandan beri değiştirildiŞubat 2009 Atelier B'nin topluluk sürümü tarafından
  • Bart  : otomatik iyileştirme aracı
  • Biçimsel yöntemlere uygulanan Brama Grafik modelleme aracı. B.
  • B modellerinin C diline ComenC Çevirmeni.
  • CompoSys Yöntemi ve sistemlerin resmi açıklamaları için araç.
  • RODIN , Eclipse'e dayalı B etkinlikleri platformu
  • ABtools
  • BATCAVE
  • BRILLANT : B yöntemini destekleyen araçlar için açık kaynaklı geliştirme projesi.
  • jBtools
  • DumBeX B'den Gösterim Çeviriciye\Lateks