of the software produces and uses real-time information about the world, and monitors and partly controls its behavior to provide required functionality and to satisfy required constraints.

Such systems pose a particular challenge, arising from the interaction between the quasi-formal nature of the software and the nonformal nature of its human and physical problem world outside the computer. The software in execution can be regarded as a formal system: for all but the most extremely critical systems the computer behavior can be assumed to conform to the program semantics. The nonformal problem world, in contrast, has many parts—human, natural, and engineered—whose properties and behavior are far less reliable. For a dependable system, there must be an adequate formal model of the problem world, and the software must be designed to reflect the assumption that the world conforms to this model. In executing its program, the computer always behaves as if the world model is valid; if the world deviates from the model, the system will fail in some way. The problem world, being nonformal, has unbounded possible behaviors and properties that can invalidate any formal model. Fault-tolerant techniques in which the model is weakened in suitably chosen respects can mitigate the difficulty, but they cannot eliminate it: the world can still invalidate the weakened model. How, then, can a dependable system be designed?

Development of the formal model is, above all, an engineering task. In the established engineering branches, the challenge is met by experience accumulated in each particular product class and captured in a normal design discipline. The aeronautical engineer W. G. Vincenti explains normal design: “The engineer knows at the outset how the device in question works, what are its customary features, and that, if properly designed along such lines, it has a good likelihood of accomplishing the desired task.” Family cars, for example, are the product of an industry-wide normal design discipline. Different manufacturers’ products are strikingly similar both in their external appearance and in their internal workings because their designers adhere closely to the current normal design. This normal design embodies the accumulated knowledge of the

models—both of the product itself and of its environment or problem world— that is adequate for a desired level of dependability: which deviations from a model are sufficiently improbable to be ignored; which are implicitly handled by the normal design configuration; and which must be explicitly considered in the calculations and checks mandated by the discipline of the normal design practice.

The engineer lacking an applicable normal design discipline must inevitably engage in radical design. In Vincenti’s words: “In radical design, how the device should be arranged or even how it works is largely unknown. The designer has never seen such a device before and has no presumption of success. The problem is to design something that will function well enough to warrant further development.” In short, radical design has a low expectation of dependability: it can be a good choice only in purely experimental work or where novelty and excitement are of the highest importance and dependability is little valued.

A normal design discipline does not arise easily or by chance. It rests on a culture of specialization, in which a community of organizations and individuals is devoted to gradual, long-term evolution of normal design in a particular product class and of the scientific and engineering knowledge it embodies. The prerequisites for this culture of specialization are two: the continuing existence of specialized communities, with their research and production facilities and their journals and conferences; and the desire of individual highly talented engineers in each generation to dedicate their professional careers to working within just one specialization. This infrastructure of a specialized community and the advances needed to evolve a successful normal design discipline are not achievable or sustainable by floating populations of itinerant generalists.

Software engineering and computer science already have many specializations: some in complexity theory, concurrency, real-time systems, programming languages, model checking, program proving, and distributed computing; and some in system software components such as compilers, database systems, virus checkers, and SAT (Boolean satisfiability problem)

solvers. These specializations, however, are not enough. To build dependable software-intensive systems, we must emulate the established engineering branches, developing many more specializations that are sharply focused on narrow classes of end products and their component subsystems. Only the product-oriented specialist can achieve dependability by bringing together the contributions of specialists in all the different aspects, parts, and dimensions of the design task.

What particular specializations, then, are needed? We cannot answer this question in advance, or in any systematic or authoritative way. In a society that insists on dependable systems, with a software-engineering culture that values and motivates specialization, particular specializations will emerge and evolve in response to opportunities and challenges as they are recognized.

In sum, dependability in an engineering product must be based on a normal design discipline. Only in a product-oriented normal design discipline can all the necessary knowledge—tacit and explicit—be brought together to build a dependable system. This normal discipline in turn must be the product of a long-term community of engineers specializing in systems of the particular product class. For a critical software-intensive system, specialization is not optional.

Patrick cousot: the Role of abstract
interpretation in formal methods

Formal Verification Methods. In computer science and software engineering, formal methods are mathematically based techniques for the specification, development, and verification of software and hardware systems. They establish the satisfaction of a required property (called the specification) by a formal model (called the semantics) of the behavior of a system (for example, a program and its physical environment). The semantic domain is a set of all such formal models of system behaviors.

A property of the system is a set of semantic models that satisfy this property. The satisfaction of a specification by a system (more precisely by its semantics), which can equivalently be defined as the proof that its strongest property is a property of the system, is called its collecting semantics.