We use a railway-related case study to illustrate the differences that can be encountered while modeling and verifying a system using an academic formal verification framework and an industrial model-based framework. The different roles and structures of the two approaches are illustrated. We analyze instances where the exclusive use of interactive simulation cannot replicate the formal verification activity, and we derive some future research directions.
Comparing model checking and model-based simulation
Basile D.
;Mazzanti F.Writing – Original Draft Preparation
2025
Abstract
We use a railway-related case study to illustrate the differences that can be encountered while modeling and verifying a system using an academic formal verification framework and an industrial model-based framework. The different roles and structures of the two approaches are illustrated. We analyze instances where the exclusive use of interactive simulation cannot replicate the formal verification activity, and we derive some future research directions.File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
RSSRail_2025.pdf
accesso aperto
Descrizione: pre-print
Tipologia:
Documento in Pre-print
Licenza:
Altro tipo di licenza
Dimensione
986.03 kB
Formato
Adobe PDF
|
986.03 kB | Adobe PDF | Visualizza/Apri |
|
Basile_ComparingModelChecking_2025.pdf
solo utenti autorizzati
Descrizione: Comparing Model Checking and Model-Based Simulation
Tipologia:
Versione Editoriale (PDF)
Licenza:
NON PUBBLICO - Accesso privato/ristretto
Dimensione
2.35 MB
Formato
Adobe PDF
|
2.35 MB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
