Abstraction and Idealization in the Formal Verification of Software Systems

Minds and Machines 23 (2):211-226 (2013)
Authors
Abstract
Questions concerning the epistemological status of computer science are, in this paper, answered from the point of view of the formal verification framework. State space reduction techniques adopted to simplify computational models in model checking are analysed in terms of Aristotelian abstractions and Galilean idealizations characterizing the inquiry of empirical systems. Methodological considerations drawn here are employed to argue in favour of the scientific understanding of computer science as a discipline. Specifically, reduced models gained by Dataion are acknowledged as Aristotelian abstractions that include only data which are sufficient to examine the interested executions. The present study highlights how the need to maximize incompatible properties is at the basis of both Abstraction Refinement, the process of generating a cascade of computational models to achieve a balance between simplicity and informativeness, and the Multiple Model Idealization approach in biology. Finally, fairness constraints, imposed to computational models to allow fair behaviours only, are defined as ceteris paribus conditions under which temporal formulas, formalizing software requirements, acquire the status of law-like statements about the software systems executions
Keywords Philosophy of computer science  Model checking  State space reduction techniques  Aristotelian abstraction  Multiple model idealization  Galilean idealization
Categories (categorize this paper)
DOI 10.1007/s11023-012-9289-8
Options
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

Our Archive


Upload a copy of this paper     Check publisher's policy     Papers currently archived: 37,100
Through your library

References found in this work BETA

How the Laws of Physics Lie.Nancy Cartwright - 1983 - Oxford University Press.
Three Kinds of Idealization.Michael Weisberg - 2007 - Journal of Philosophy 104 (12):639-659.
Ceteris Paribus Conditionals and Comparative Normalcy.Martin Smith - 2006 - Journal of Philosophical Logic 36 (1):97-121.
Galilean Idealization.Ernan McMullin - 1985 - Studies in History and Philosophy of Science Part A 16 (3):247-273.

View all 27 references / Add more references

Citations of this work BETA

Add more citations

Similar books and articles

Analytics

Added to PP index
2012-11-05

Total downloads
40 ( #165,467 of 2,308,247 )

Recent downloads (6 months)
5 ( #130,932 of 2,308,247 )

How can I increase my downloads?

Monthly downloads

My notes

Sign in to use this feature