Modellazione in Event-B

Questo libro si concentra sull’uso di Event-B come metodo formale per la modellazione e la verifica del software. Il nostro caso di studio è il sistema di controllo degli ascensori (ECS). I requisiti dell’ascensore vengono tradotti in modelli matematici Event-B. Utilizziamo RODIN per sviluppare, testare e verificare i modelli Event-B dell’ECS prima di poter implementare il sistema in un programma software. La modellazione Event-B è così fondamentale che ci permette di identificare i requisiti mancanti, gli errori nella nostra progettazione e di dimostrare che il modello di sistema funzionerà come previsto, rispetto a quanto accadrebbe se sviluppassimo un sistema immediatamente dopo aver ricevuto i requisiti dal cliente. Questi requisiti sono infatti incompleti e ambigui. Con l’uso di Event-B, riduciamo il costo dello sviluppo del sistema poiché gli errori vengono sempre individuati nelle prime fasi dello sviluppo. Il passaggio dalla fase dei requisiti alla fase delle specifiche formali è uno dei passaggi più impegnativi. Infatti, la creazione di modelli iniziali a partire dai requisiti di sistema richiede un alto livello di competenza e abilità pratiche nella modellazione Event-B. Poiché non esiste un processo ben definito per guidare gli ingegneri di sistema, questo libro fornisce un approccio pratico su come sviluppare buoni sistemi software.