Essential traits of model checking, a prominent formal method utilized in computer science to predict future behaviours of software systems, are examined here in the framework of the model-based paradigm of scientific reasoning. Models that model checking techniques enable one to develop are shown to satisfy logical re-quirements expressed by the set-theoretic view of scientific models. It is highlighted how model checking algorithms are able to isolate law-like generalizations holding in the model under given ceteris paribus conditions and concerning software executions. Further-more, abstraction methodologies utilized in model checking to de-crease the state space of complex models are taken to be instantia-tions of the general process known as Aristotelian abstraction char-acterizing empirical modelling. Finally, the methodological interest of the model-checking techniques is emphasized in connection with the debate concerning the epistemological status of computer sci-ence.

Software Verification and Scientific Methodology: Models, Regularities, Idealizations

ANGIUS, NICOLA
2011-01-01

Abstract

Essential traits of model checking, a prominent formal method utilized in computer science to predict future behaviours of software systems, are examined here in the framework of the model-based paradigm of scientific reasoning. Models that model checking techniques enable one to develop are shown to satisfy logical re-quirements expressed by the set-theoretic view of scientific models. It is highlighted how model checking algorithms are able to isolate law-like generalizations holding in the model under given ceteris paribus conditions and concerning software executions. Further-more, abstraction methodologies utilized in model checking to de-crease the state space of complex models are taken to be instantia-tions of the general process known as Aristotelian abstraction char-acterizing empirical modelling. Finally, the methodological interest of the model-checking techniques is emphasized in connection with the debate concerning the epistemological status of computer sci-ence.
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/11584/76706
 Attenzione

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

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