Block-Based Models and Theorem Proving in Model-Based Development

Cinzia Bernardeschi, Andrea Domenici, Adriano Fagiolini, Maurizio Palmieri

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.


Full Text:

PDF


DOI: http://dx.doi.org/10.14279/tuj.eceasst.79.1116

DOI (PDF): http://dx.doi.org/10.14279/tuj.eceasst.79.1116.1067

Hosted By Universit├Ątsbibliothek TU Berlin.