Abstraction and Idealization in the Formal Verification of Software Systems
- 234 Downloads
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 Data Abstraction 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.
KeywordsPhilosophy of computer science Model checking State space reduction techniques Aristotelian abstraction Multiple model idealization Galilean idealization
I am grateful to the reviewer for insightful and constructive comments. I would also like to thank Alberto Mario Mura and Guglielmo Tamburrini for helpful suggestions on an early draft of this paper. This work was founded by the Regione Autonoma della Sardegna.
- Cartwright, N. (1989) . Nature’s capacities and their measurement. Oxford, New York: Oxford University Press.Google Scholar
- Clarke, E. M., Grumberg, O., Jha, S., Lu, Y., & Veith, H. (2000). Counterexample-guided Abstraction Refinement. Proceedings of the 12th international conference for computer-aided verification. Lecture Notes in Computer Science. 1855, 154–169.Google Scholar
- Clarke, E. M., Grumberg, O., & Peled, D. A. (1999). Model checking. Cambridge, MA: The MIT Press.Google Scholar
- Colburn, T. (2004). Methodology of computer science. In L. Floridi (Ed.), The blackwell guide to the philosophy of computing and information (pp. 318–326). Malden: Blackwell.Google Scholar
- Eden, H. A., & Turner, R. (2007). Problems in the ontology of computer programs. Applied Ontology, 2(1), 13–36.Google Scholar
- Frigg, R., & Hartman, S. (2006). Models in science. Resource document. Stanford Encyclopedia of Philosophy. http://plato.stanford.edu/entries/models-science/.
- Hausman, D. M. (1988). Ceteris paribus clauses and causality in economics. PSA: Proceedings of the Biennial Meeting of the Philosophy of Science Association. 2, 308–316.Google Scholar
- Hempel, C. G. (1988). Provisos. In A. Grünbaum & W. Salmon (Eds.), The limitations of deductivism (pp. 19–36). Berkley: University of California Press.Google Scholar
- Jones, M. R. (2005). Idealization and abstraction: A framework. In M. R. Jones & N. Cartwright (Eds.), Idealization XII: Correcting the model. Idealization and abstraction in the sciences (pp. 173–217). Amsterdam: Rodopi.Google Scholar
- Kröger, F., & Merz, S. (2008). Temporal logics and state systems. Berlin: Springer.Google Scholar
- Kurshan, R. P. (1994). Computer-aided verification of coordinating processes. Princeton, NJ: Princeton University Press.Google Scholar
- Lee, W., Pardo, A., Jang, J., Hachtel, G., & Somenzi, F. (1996). Tearing based abstraction for CTL model checking. Proceedings of the international conference of computer-aided design (ICCAD). (pp. 76–81).Google Scholar
- Levins, R. (1966). The strategy of model building in population biology. American Scientist, 54(4), 421–431.Google Scholar
- Lindenberg, S. (1990). A new push in the theory of organization. A commentary on O. E. Williamson’s comparison of alternative approaches to economic organization. Journal of Institutional and Theoretical Economics, 146(1), 76–84.Google Scholar
- Niiniluoto, I. (1990). Theories, approximations, and idealizations. In J. Brzeziński, F. Coniglione, T. A. F. Kuipers, & L. Nowak (Eds.), Idealization I: General problems (pp. 9–58). Amsterdam, Atlanta: Rodopi.Google Scholar
- Nowak, L. (1979). The structure of idealization. Towards a systematic interpretation of marxian idea of science. Dordrecht: Kluwer.Google Scholar
- Turner, R., & Eden, A. (2008). The philosophy of computer science. Resource document. Stanford Encyclopedia of Philosophy. http://plato.stanford.edu/entries/computer-science/.
- Wang, C., Hachtel, G. D., & Somenzi, F. (2006). Abstraction refinement for large scale model checking. Berlin: Springer.Google Scholar
- Wegner, P. (1976). Research paradigm in computer science. Proceedings of 2nd international conference. Software engineering. 322–330.Google Scholar
- Weisberg, M. (2007). Three kinds of idealization. The Journal of Philosophy, 104(12), 639–659.Google Scholar