Skip to main content
SpringerLink
Log in

Abstraction and Idealization in the Formal Verification of Software Systems

  • Published:
Minds and Machines Aims and scope Submit manuscript

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.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3

Similar content being viewed by others

Notes

  1. Angius and Tamburrini (2011) maintain that in the field of computer science model checking can be acknowledged as an instantiation of the model-based reasoning approach (Magnani et al. 1999) characteristic of the examination of complex empirical systems. Accordingly, one provides a formal model representing a target software system, performs experiments within the model, and draws regularities about the target system behaviours that hold according to the model.

  2. Such distinction must be taken as a hypostatization of possible philosophical approaches in the inquiry of software systems more than actual attitudes of computer scientists: theoretical computer scientists do not disregard testing or other forms of experimentation on software but they stress the fact that, in principle, one is able to predict future behaviours of software by means of mathematical proofs. Engineers, on the other hand, do not ignore the capability of formal methodologies, but they just maintain that, since performing formal proofs on complex software is time consuming and often unfeasible, testing turns out to be the most practical and rapid way to ascertain the correctness of software before launching products into the market.

  3. Software models in model checking also include transition systems with action names (Baier and Katoen 2008, chapter 2) and Buchi automata (Clarke et al. 1999, chapter 9).

  4. The traffic light controller example used throughout this paper is liberally taken from Clarke et al. (1999, chapter 13).

  5. A KS might have more than one initial state; this is usually the case with KS for concurrent programs.

  6. In this case, the KS should represent the executions in all possible orderings.

  7. ACTL formulas are CTL statements that are quantified over all (A) possible paths.

  8. This result was first published in Clarke et al. (1994).

  9. Here, state S 0 corresponds to state S 0 in M; state S 1 is obtained by the collapse of states S 1 and S 2 in M which, according to abstract function h, become labelled with the same Stop label. It is worth noting how since a transition between S 1 and S 2 occurred in M, a self-loop on the corresponding collapsed state has been reported in M°.

  10. Nowak (1979) uses indifferently the word idealization and the word abstraction to indicate a process, in economic modelling, that involves the both of them. Humphreys (1995) highlights how the last step of an abstraction process of a given empirical system usually involves an idealization of Galilean type. This fact explains why concretization, i.e. the inverse operation of abstraction, does not simply consist of an adding back of the previously ignored data but it involves corrections and de-idealizations. Weisberg (2007) suggests how an Aristotelian abstraction and a Galilean idealization might even yield the very same model. What distinguishes the two approaches is rather their justification: the Galilean idealization is employed to make more tractable the examination of complex empirical systems; the Aristotelian abstraction is used to isolate causal factors and it is concerned with scientific explanation.

  11. ACTL* temporal logic is given by the union set of ACTL and LTL.

  12. For a complete introduction on algebraic relations between Kripke structures, see Fokkink (2000).

  13. It may also happen that the initial abstraction is an under-approximation, i.e. a structure that does not simulate all the paths of the starting KS. When checking universal formulas, a counterexample encountered in an under-approximated structure corresponds to an actual counterexample in the original KS. However, if the model checking algorithm does not find a counterexample in the end, this does not automatically mean that the formula holds true: the formula might, indeed, correspond to a false positive, and a counterexample might be present in the unreduced model (Lee et al. 1996).

  14. This example is taken from Clarke et al. (2000).

  15. One would aim to obtain the smallest structure not including spurious counterexamples in order to maintain a good proficiency of the checking algorithm. Unfortunately, computing the ‘coarsest refinement’ is NP-hard (Clarke et al. 2003, 778); Clarke et al. (2003) proposed a polynomial-time refinement algorithm that provides a refinement which is suitable for model checking.

  16. However, it should be carefully noticed how a Galilean idealization is an intentional introduction of false assumptions; in over-approximated Kripke structures non-actual paths are the unintentional result of the process of generating an abstract model which simulates the behaviours of the corresponding complex model.

  17. The practice of building an initial abstract model and, successively, of adding back previously omitted information, in order to improve prediction accuracy, characterizes economic modeling as well. The method of decreasing abstraction (Lindenberg 1990) aims at obtaining the simplest model among those that possess successful predictive capabilities.

  18. The thesis that CP clauses are better conceived as counterfactual claims is also shared by Niiniluoto (1990), Smith (2005), Rol (2008).

  19. In Cartwright’s view, Newton’s law of gravitation f = G m1m2/r2 is untrue since bodies are often under the influence of different forces or gravitational fields. For this reason, Cartwright argues that formulations of physical laws must include ceteris paribus modifiers. Newton’s gravitational law should be formulated in this way: if there are no forces exerted on the two bodies except gravity, then f = G m1m2/r 2 (Cartwright 1983, 58).

References

  • Ammann, P., & Offutt, J. (2008). Introduction to software testing. Cambridge: Cambridge University Press.

    Book  MATH  Google Scholar 

  • Angius, N., & Tamburrini, G. (2011). Scientific theories of computational systems in model checking. Minds and Machines, 21(2), 323–336.

    Article  Google Scholar 

  • Baier, C., & Katoen, J. P. (2008). Principles of model checking. Cambridge, MA: The MIT Press.

    MATH  Google Scholar 

  • Batterman, R. W. (2002). Asymptotics and the role of minimal models. British Journal for the Philosophy of Science, 53(1), 21–38.

    Article  MathSciNet  MATH  Google Scholar 

  • Cartwright, N. (1983). How the laws of physics lie. Oxford New York: Oxford University Press.

    Book  Google Scholar 

  • Cartwright, N. (1989) [1994]. Nature’s capacities and their measurement. Oxford, New York: Oxford University Press.

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

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

    Article  MathSciNet  Google Scholar 

  • Clarke, E. M., Grumberg, O., & Long, D. E. (1994). Model checking and abstraction. ACM Transaction on Programming Languages and Systems, 16(5), 1512–1542.

    Article  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 

  • Earman, J., & Roberts, J. (1999). Ceteris paribus, there is no problem of provisos. Synthese, 118(3), 439–478.

    Article  Google Scholar 

  • Eden, H. A. (2007). Three paradigms of computer science. Minds and Machines, 17(2), 135–167.

    Article  Google Scholar 

  • Eden, H. A., & Turner, R. (2007). Problems in the ontology of computer programs. Applied Ontology, 2(1), 13–36.

    Google Scholar 

  • Fodor, J. (1989). More on making matter more. Philosophical Topics, 17(1), 59–79.

    Article  Google Scholar 

  • Fokkink, W. (2000). Introduction to process algebra. Berlin: Springer.

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

  • 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 

  • Humphreys, P. (1995). Abstract and concrete. Philosophy and Phenomenological Research, LV(1), 157–161.

    Article  MathSciNet  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 

  • Joseph, G. (1980). The many sciences and the one world. Journal of Philosophy, 77(12), 773–790.

    Article  Google Scholar 

  • Kesten, Y., & Pnueli, A. (2000). Control and data abstraction: Cornerstones of the practical formal verification. Software Tools and Technology Transfer, 2(4), 328–342.

    Article  MATH  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 

  • Lange, M. (1993). Natural laws and the problem of provisos. Erkenntnis, 38(2), 233–248.

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

  • 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 

  • Magnani, L., Nersessian, N., & Thagard, P. (1999). Model based reasoning in scientific discovery. Dordrecht: Kluwer.

    Book  Google Scholar 

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

    Article  Google Scholar 

  • McMullin, E. (1985). Galilean idealization. Studies in the History and Philosophy of Science, 16(3), 247–273.

    Article  MathSciNet  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 

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

    Article  Google Scholar 

  • Persky, J. (1990). Retrospectives: Ceteris paribus. The Journal of Economic Perspectives, 4(2), 187–193.

    Article  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  • Rol, M. (2008). Idealization, abstraction, and the policy relevance of economic theories. Journal of Economic Methodology, 15(1), 69–98.

    Article  Google Scholar 

  • Schiffer, S. (1991). Ceteris paribus laws. Mind, 100(397), 1–17.

    Article  Google Scholar 

  • Schurz, G. (2002). Ceteris paribus laws: Classification and deconstruction. Erkenntnis, 57(3), 351–372.

    Article  MathSciNet  MATH  Google Scholar 

  • Smith, M. (2005). Ceteris paribus conditionals and comparative normalcy. Journal of Philosophical Logic, 36(1), 97–121.

    Article  Google Scholar 

  • Tedre, M. (2011). Computing as a science: A survey of competing viewpoints. Minds and Machines, 21(3), 361–387.

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

  • Valmari, A. (1998). The state explosion problem. Lectures on Petri Nets I: Basic models Lecture Notes in Computer Science, 1491, 429–528.

    Article  Google Scholar 

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

  • Weisberg, M. (2006). Forty years of ‘the strategy’: Levins on model building and idealizations. Biology and Philosophy, 21(5), 623–645.

    Article  MathSciNet  Google Scholar 

  • Weisberg, M. (2007). Three kinds of idealization. The Journal of Philosophy, 104(12), 639–659.

    Google Scholar 

  • Woodward, J. (2002). There is no such thing as a ceteris paribus law. Erkenntnis, 57(3), 303–328.

    Article  MathSciNet  MATH  Google Scholar 

Download references

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.

Author information

Authors and Affiliations

  1. Dipartimento di Storia, Scienze dell’Uomo e della Formazione, Università di Sassari, Sassari, Italy

    Nicola Angius

Authors
  1. Nicola Angius
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Nicola Angius.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Angius, N. Abstraction and Idealization in the Formal Verification of Software Systems. Minds & Machines 23, 211–226 (2013). https://doi.org/10.1007/s11023-012-9289-8

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s11023-012-9289-8

Keywords

Search

Navigation