This paper presents a methodology to integrate computer-assisted theorem proving into a standard workflow for model-based development that uses a block-based language as a modeling and simulation tool. The theorem prover provides confidence in the results of the analysis as it guides the developers towards a correct formalization of the system under development.
Block-Based Models and Theorem Proving in Model-Based Development
Bernardeschi C.;Domenici A.;Palmieri M.
2020-01-01
Abstract
This paper presents a methodology to integrate computer-assisted theorem proving into a standard workflow for model-based development that uses a block-based language as a modeling and simulation tool. The theorem prover provides confidence in the results of the analysis as it guides the developers towards a correct formalization of the system under development.File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
1116-3390-1-PB.pdf
accesso aperto
Descrizione: Articolo principale
Tipologia:
Versione finale editoriale
Licenza:
Creative commons
Dimensione
209.37 kB
Formato
Adobe PDF
|
209.37 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
