Rodinův nástroj - Rodin tool - Wikipedia

The Rodinův nástroj je nástroj pro formální modelování v Event-B. Událost-B je notace a metoda vyvinutá z B-metoda a je určen k použití s ​​přírůstkovým stylem modelování. Myšlenka přírůstkového modelování byla převzata z programování: moderní programovací jazyky přijít s integrované vývojové prostředí které usnadňují úpravy a vylepšování programů. Nástroj Rodin poskytuje takové prostředí pro událost-B. Dvě hlavní charakteristiky nástroje Rodin jsou jeho snadné použití a jeho rozšiřitelnost. Nástroj se zaměřuje na modelování. Je snadné modifikovat modely a vyzkoušet varianty modelu. Nástroj lze také snadno rozšířit. To umožňuje přizpůsobit nástroj konkrétním potřebám, takže lze nástroj přizpůsobit tak, aby vyhovoval stávajícím vývojovým procesům, místo aby vyžadoval opak. Událost-B wiki je užitečný zdroj pro uživatele a vývojáře.

Rodin (Rigorous Open Development Environment for Complex Systems) je příponou Zatmění IDE (založené na prostředí Java). Souřadnice Builderu Eclipse Builder:

  • Kontrola správného tvarování + typu
  • Generátor důkazních povinností (PO)
  • Proof manager (PM)
  • Šíření změn

Rodin Proof Manager (PM)

  • PM vytvoří kontrolní strom pro každou PO
  • Automatické a interaktivní režimy
  • PM řídí použité hypotézy
  • PM volá odůvodněné osoby
    • splnit cíl, nebo
    • rozdělit cíl na subgoals
  • Sbírka argumentů:
    • zjednodušující, na základě pravidel, rozhodovací postupy,…
  • Základní taktický jazyk pro definování PM a argumentů

Průmyslové aplikace a případové studie

Projekt Rodin zahrnoval pět průmyslových případových studií, které sloužily k ověření sady nástrojů a pomohly s vypracováním vhodné metodiky pro používání těchto nástrojů. Případové studie byly vedeny průmyslovými partnery projektu Rodin podporovanými ostatními partnery. Případové studie byly následující:

  • systém řízení poruch pro řadič motoru
  • součást platformy pro mobilní internetovou technologii
  • inženýrství komunikačních protokolů
  • systém zobrazení letového provozu
  • aplikace kampusu prostředí

Některé dostupné pluginy pro Rodina

  • Prověřovače B4free
    • Poskytovatel: ClearSy
    • Funkce: Věta dokazuje
  • UML-B
    • Poskytovatel: University of Southampton
    • Funkce: Grafické rozhraní typu UML pro Event-B podporující diagramy tříd a stavové grafy
  • ProB
    • Poskytovatel: University of Düsseldorf
    • Funkce: Animace a kontrola modelů modelů Event-B; Protiklady pro falešné důkazní cíle, zejména důkazní povinnosti
  • Brama
    • Poskytovatel: ClearSy
    • Funkce: Animace modelů B. Účel je dvojí:
      • experimentování s modelem k pozorování stavů a ​​přechodů
      • Flash animace modelů Event-B
  • Modularizace
    • Poskytovatel: Newcastle University
    • Funkce: Strukturování vývoje události B do logických jednotek modelování, nazývaných moduly; Složení modelu; Opětovné použití modelu

Reference

  • Jean-Raymond Abrial. Kniha B: Přiřazení programů významům. Cambridge University Press, 1996, (ISBN  0-521-49619-5).
  • Jean-Raymond Abrial, Michael Butler, Stefan Hallerstede a Laurent Voisin. Otevřené rozšiřitelné prostředí nástroje pro Event-B. V publikacích Z. Liu a J. He, ICFEM 2006, ročník 4260, strany 588–605. Springer, 2006.
  • Abdolbaghi ​​Rezazadeh, Neil Evans a Michael Butler. Sanace průmyslového odvětví, případová studie využívající Event-B a Rodin. Na setkání BCS-FACS Christmas 2007, 2007.
  • RODIN. Výstup D18: Průběžná zpráva o vývoji případových studií.
  • Michael Butler a Stefan Hallerstede: Nástroj pro formální modelování Rodin, výzkumný projekt EU IST 511599 RODIN
  • Zatmění. Domovská stránka platformy Eclipse.

Tento článek je založen na materiálu převzatém z Zdarma online slovník výpočetní techniky před 1. listopadem 2008 a začleněno pod "licencování" podmínek GFDL, verze 1.3 nebo novější.