Formal methods have a great potential of application in the development of industrial critical systems. in certain application fields, formal methods are even becoming part of standards. Among formal methods, Model Checking is proving particularly effective, especially thanks to its ability to automatically analyze complex designs and to produce counterexamples. However, the application of formal methods in the industrial development practice is by no means trivial. Formal methods can be costly, slow down the development, and require training and changes to the development cycle. In this paper, the application of Model Checking techniques in the development of the application of Model Checking techniques in the development of industrial critical systems is discussed, by focusing on two projects where Model Checking has been successfully applied under different conditions.

Industrial Applications of Model Checking

Cimatti, Alessandro
2001-01-01

Abstract

Formal methods have a great potential of application in the development of industrial critical systems. in certain application fields, formal methods are even becoming part of standards. Among formal methods, Model Checking is proving particularly effective, especially thanks to its ability to automatically analyze complex designs and to produce counterexamples. However, the application of formal methods in the industrial development practice is by no means trivial. Formal methods can be costly, slow down the development, and require training and changes to the development cycle. In this paper, the application of Model Checking techniques in the development of the application of Model Checking techniques in the development of industrial critical systems is discussed, by focusing on two projects where Model Checking has been successfully applied under different conditions.
2001
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11582/141
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
social impact