Rodin verktøy - Rodin tool

The Rodin verktøyet er et verktøy for formell modellering i hendelses-B. Event-B er en notasjon og metode utviklet fra B-metoden og er ment å brukes med en inkrementell modelleringsstil . Ideen om inkrementell modellering er hentet fra programmering: moderne programmeringsspråk har integrert utviklingsmiljø som gjør det enkelt å endre og forbedre programmer. Rodin-verktøyet gir et slikt miljø for Event-B. De to viktigste egenskapene til Rodin-verktøyet er brukervennligheten og utvidbarheten. Verktøyet fokuserer på modellering. Det er enkelt å endre modeller og prøve ut varianter av en modell. Verktøyet kan også utvides enkelt. Dette gjør det mulig å tilpasse verktøyet til spesifikke behov, slik at verktøyet kan tilpasses for å passe inn i eksisterende utviklingsprosesser i stedet for å kreve det motsatte. Event-B wiki er en nyttig bruker- og utviklerressurs.

Rodin (Rigorous Open Development Environment for Complex Systems) er en utvidelse av Eclipse IDE (Java-basert). Rodin Eclipse Builder koordinater:

  • Velformet + kontrollør av typen
  • Proof duty (PO) generator
  • Proof manager (PM)
  • Formering av endringer

Rodin Proof Manager (PM)

  • PM konstruerer korrekturstre for hver PO
  • Automatiske og interaktive modus
  • PM administrerer brukte hypoteser
  • PM ringer resonnenter til
    • utslippsmål, eller
    • del mål i undergrunner
  • Innsamling av resonnementer:
    • forenkler, regelbaserte, beslutningsprosedyrer, ...
  • Grunnleggende taktikkspråk for å definere PM og resonnementer

Industrielle applikasjoner og casestudier

Rodin-prosjektet inkluderte fem industrielle casestudier som tjente til å validere verktøyet og hjalp til med utarbeidelsen av en passende metodikk for bruk av verktøyene. Casestudiene ble ledet av industripartnere i Rodin-prosjektet støttet av de andre partnerne. Casestudiene var som følger:

  • et feilstyringssystem for en motorkontroller
  • del av en plattform for mobil Internett-teknologi
  • prosjektering av kommunikasjonsprotokoller
  • et visningssystem for flytrafikk
  • en ambient campus-applikasjon

Noen tilgjengelige plugins for Rodin

  • B4free provers
    • Tilbyder: ClearSy
    • Funksjon: Teorem beviser
  • UML-B
    • Tilbyder: University of Southampton
    • Funksjon: UML-lignende grafisk frontend for Event-B som støtter klassediagrammer og tilstandsdiagrammer
  • prob
    • Tilbyder: University of Düsseldorf
    • Funksjon: Animasjon og modellkontroll av Event-B-modeller; Moteksempler for falske bevismål, spesielt bevisforpliktelser
  • Brama
    • Tilbyder: ClearSy
    • Funksjon: Animasjon av B-modeller. Hensikten er todelt:
      • eksperimentering med en modell for å observere tilstander og overganger
      • Flash-animasjon av Event-B-modeller
  • modularisering
    • Tilbyder: Newcastle University
    • Funksjon: Strukturere utviklingen av Event-B til logiske modelleringsenheter, kalt moduler; Modelsammensetning; Gjenbruk av modeller

referanser

  • Jean-Raymond Abrial . B-boken: Tilordne programmer til betydning. Cambridge University Press, 1996, ( ISBN  0-521-49619-5 ).
  • Jean-Raymond Abrial , Michael Butler, Stefan Hallerstede og Laurent Voisin. Et åpent, utvidbart verktøymiljø for Event-B. I Z. Liu og J. He, redaktører, ICFEM 2006, bind 4260, side 588–605. Springer, 2006.
  • Abdolbaghi ​​Rezazadeh, Neil Evans og Michael Butler. Omutvikling av en industriell casestudie ved bruk av Event-B og Rodin. I BCS-FACS julemøte 2007, 2007.
  • Rodin. Leverbar D18: Delrapport om utvikling av casestudier.
  • Michael Butler og Stefan Hallerstede: Rodin Formal Modelling Tool, EUs forskningsprosjekt IST 511599 RODIN
  • Formørkelse . Eclipse-plattformens hjemmeside.

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