Advertisement

Minds and Machines

, Volume 23, Issue 2, pp 211–226 | Cite as

Abstraction and Idealization in the Formal Verification of Software Systems

  • Nicola Angius
Article

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 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.

Keywords

Philosophy of computer science Model checking State space reduction techniques Aristotelian abstraction Multiple model idealization Galilean idealization 

Notes

Acknowledgments

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.

References

  1. Ammann, P., & Offutt, J. (2008). Introduction to software testing. Cambridge: Cambridge University Press.MATHCrossRefGoogle Scholar
  2. Angius, N., & Tamburrini, G. (2011). Scientific theories of computational systems in model checking. Minds and Machines, 21(2), 323–336.CrossRefGoogle Scholar
  3. Baier, C., & Katoen, J. P. (2008). Principles of model checking. Cambridge, MA: The MIT Press.MATHGoogle Scholar
  4. Batterman, R. W. (2002). Asymptotics and the role of minimal models. British Journal for the Philosophy of Science, 53(1), 21–38.MathSciNetMATHCrossRefGoogle Scholar
  5. Cartwright, N. (1983). How the laws of physics lie. Oxford New York: Oxford University Press.CrossRefGoogle Scholar
  6. Cartwright, N. (1989) [1994]. Nature’s capacities and their measurement. Oxford, New York: Oxford University Press.Google Scholar
  7. 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
  8. Clarke, E. M., Grumberg, O., Jha, S., Lu, Y., & Veith, H. (2003). Counterexample-guided abstraction refinement for symbolic model-checking. Journal of the ACM, 50(5), 752–794.MathSciNetCrossRefGoogle Scholar
  9. Clarke, E. M., Grumberg, O., & Long, D. E. (1994). Model checking and abstraction. ACM Transaction on Programming Languages and Systems, 16(5), 1512–1542.CrossRefGoogle Scholar
  10. Clarke, E. M., Grumberg, O., & Peled, D. A. (1999). Model checking. Cambridge, MA: The MIT Press.Google Scholar
  11. 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
  12. Earman, J., & Roberts, J. (1999). Ceteris paribus, there is no problem of provisos. Synthese, 118(3), 439–478.CrossRefGoogle Scholar
  13. Eden, H. A. (2007). Three paradigms of computer science. Minds and Machines, 17(2), 135–167.CrossRefGoogle Scholar
  14. Eden, H. A., & Turner, R. (2007). Problems in the ontology of computer programs. Applied Ontology, 2(1), 13–36.Google Scholar
  15. Fodor, J. (1989). More on making matter more. Philosophical Topics, 17(1), 59–79.CrossRefGoogle Scholar
  16. Fokkink, W. (2000). Introduction to process algebra. Berlin: Springer.MATHCrossRefGoogle Scholar
  17. Frigg, R., & Hartman, S. (2006). Models in science. Resource document. Stanford Encyclopedia of Philosophy. http://plato.stanford.edu/entries/models-science/.
  18. 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
  19. 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
  20. Humphreys, P. (1995). Abstract and concrete. Philosophy and Phenomenological Research, LV(1), 157–161.MathSciNetCrossRefGoogle Scholar
  21. 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
  22. Joseph, G. (1980). The many sciences and the one world. Journal of Philosophy, 77(12), 773–790.CrossRefGoogle Scholar
  23. Kesten, Y., & Pnueli, A. (2000). Control and data abstraction: Cornerstones of the practical formal verification. Software Tools and Technology Transfer, 2(4), 328–342.MATHCrossRefGoogle Scholar
  24. Kröger, F., & Merz, S. (2008). Temporal logics and state systems. Berlin: Springer.Google Scholar
  25. Kurshan, R. P. (1994). Computer-aided verification of coordinating processes. Princeton, NJ: Princeton University Press.Google Scholar
  26. Lange, M. (1993). Natural laws and the problem of provisos. Erkenntnis, 38(2), 233–248.CrossRefGoogle Scholar
  27. 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
  28. Levins, R. (1966). The strategy of model building in population biology. American Scientist, 54(4), 421–431.Google Scholar
  29. 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
  30. Magnani, L., Nersessian, N., & Thagard, P. (1999). Model based reasoning in scientific discovery. Dordrecht: Kluwer.CrossRefGoogle Scholar
  31. Mäki, U. (2004). Theoretical isolation and explanatory progress: Transaction cost economics and the dynamics of dispute. Cambridge Journal of Economics, 28(3), 319–346.CrossRefGoogle Scholar
  32. McMullin, E. (1985). Galilean idealization. Studies in the History and Philosophy of Science, 16(3), 247–273.MathSciNetCrossRefGoogle Scholar
  33. 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
  34. Nowak, L. (1979). The structure of idealization. Towards a systematic interpretation of marxian idea of science. Dordrecht: Kluwer.Google Scholar
  35. Orzack, S. H., & Sober, E. (1993). A critical assessment of levins’s strategy of model building in population biology (1966). Quarterly Review of Biology, 68(4), 533–546.CrossRefGoogle Scholar
  36. Persky, J. (1990). Retrospectives: Ceteris paribus. The Journal of Economic Perspectives, 4(2), 187–193.CrossRefGoogle Scholar
  37. Pietroski, P., & Rey, G. (1995). When other things aren’t equal: Saving ceteris paribus laws from vacuity. The British Journal for the Philosophy of Science, 46(1), 81–110.MathSciNetMATHCrossRefGoogle Scholar
  38. Rol, M. (2008). Idealization, abstraction, and the policy relevance of economic theories. Journal of Economic Methodology, 15(1), 69–98.CrossRefGoogle Scholar
  39. Schiffer, S. (1991). Ceteris paribus laws. Mind, 100(397), 1–17.CrossRefGoogle Scholar
  40. Schurz, G. (2002). Ceteris paribus laws: Classification and deconstruction. Erkenntnis, 57(3), 351–372.MathSciNetMATHCrossRefGoogle Scholar
  41. Smith, M. (2005). Ceteris paribus conditionals and comparative normalcy. Journal of Philosophical Logic, 36(1), 97–121.CrossRefGoogle Scholar
  42. Tedre, M. (2011). Computing as a science: A survey of competing viewpoints. Minds and Machines, 21(3), 361–387.CrossRefGoogle Scholar
  43. Turner, R., & Eden, A. (2008). The philosophy of computer science. Resource document. Stanford Encyclopedia of Philosophy. http://plato.stanford.edu/entries/computer-science/.
  44. Valmari, A. (1998). The state explosion problem. Lectures on Petri Nets I: Basic models Lecture Notes in Computer Science, 1491, 429–528.CrossRefGoogle Scholar
  45. Wang, C., Hachtel, G. D., & Somenzi, F. (2006). Abstraction refinement for large scale model checking. Berlin: Springer.Google Scholar
  46. Wegner, P. (1976). Research paradigm in computer science. Proceedings of 2nd international conference. Software engineering. 322–330.Google Scholar
  47. Weisberg, M. (2006). Forty years of ‘the strategy’: Levins on model building and idealizations. Biology and Philosophy, 21(5), 623–645.MathSciNetCrossRefGoogle Scholar
  48. Weisberg, M. (2007). Three kinds of idealization. The Journal of Philosophy, 104(12), 639–659.Google Scholar
  49. Woodward, J. (2002). There is no such thing as a ceteris paribus law. Erkenntnis, 57(3), 303–328.MathSciNetMATHCrossRefGoogle Scholar

Copyright information

© Springer Science+Business Media Dordrecht 2012

Authors and Affiliations

  1. 1.Dipartimento di Storia, Scienze dell’Uomo e della FormazioneUniversità di SassariSassariItaly

Personalised recommendations