Epistemology, Software Engineering
C. Michael Holloway
Epistemology, Software Engineering
Epistemology, Software Engineering, and Formal Methods
The Role of Computers
C. Michael Holloway
One of the most basic questions anyone can ask is, "How do I know that what I think I know is true?" The study of this question is called epistemology. Traditionally, epistemology has been considered to be of legitimate interest only to philosophers, theologians, and three-year-old-children, who respond to every statement by asking, "Why?" Software engineers need to be interested in the subject, however, because a lack of sufficient understanding of epistemology contributes to many of the current problems in the field.
Epistemology is a complex subject, one to which many philosophers and theologians have devoted their entire careers. The discussion here is necessarily brief and incomplete; however, it should be sufficient to demonstrate the critical importance of the subject to software engineering.
To the fundamental question of how do we know what is true, there are three basic answers: authority, reason, and experience. An epistemology based on authority states that truth is given to us by someone more knowledgeable than ourselves. The two primary variations of authority-based epistemologies are omniscient authority (the authority is God), and human authority (the authority is a human expert).
An epistemology based on reason claims that what is true is that which can be proven using the rules of deductive logic. Finally, an epistemology based on experience claims that what is true is that which can be encountered through one or more of the senses.
Several different variations of experience-based epistemologies exist. The two variations relevant to this discussion are anecdotal experience and empirical evidence. The first states that truth for any particular individual or group of individuals is that which the individual, or group, personally experiences. The second states that truth is that which can be verified through carefully controlled experiments.
The relative strengths of these epistemological approaches are as follows. Omniscient authority provides absolute truth; if there is a God and He has spoken on something, then what He says must, by definition, be true. Reason yields conditional absolute truth; if the premises on which a valid deductive argument are known to be true, then the conclusion of the argument must also be true.
Empirical evidence provides probable truth; if controlled experiments are designed properly and repeated enough times, then it is highly probable that the results accurately describe reality. Anecdotal experience yields possible truth; if something happened for one person, it is possible it might happen to others also. Finally, human authority provides opinion.
On which of these approaches to epistemology is software engineering mostly based?
The software engineering literature is filled with pronouncements about how software should be developed (e.g., "Object-oriented development is the best way to obtain reusable software"). Rarely, if ever, are these pronouncements augmented with either logical or experimental evidence. Thus, one is forced to conclude that much of software engineering is based on a combination of anecdotal experience and human authority. That is, we know that a particular technique is good because John Doe, who is an expert in the field, says that it is good (human authority); John Doe knows that it is good because it worked for him (anecdotal experience). This is a weak epistemological foundation on which to base an entire discipline.
This current state should not be surprising; the development of software engineering is following the same pattern as the development of many other disciplines. Civil engineering, chemical engineering, aeronautical engineering, and others all had periods in which they relied almost exclusively on anecdotal experience and the subsequent authority of the "experts". Often, it took major disasters before practitioners in such fields began to investigate fully the foundations on which their field was based.
To date, although there have been many, many software problems, there have been no major disasters that have been directly attributed to software. However, unless a sound epistemological foundation is established for software engineering, disasters will come one day. To avoid this, research is needed to develop valid approaches to answering questions about both software products (e.g., are these requirements consistent?) and software processes (e.g., is method A better than method B?).
The Assessment Technology Branch (ATB), which is part of the Information and Electromagnetic Technology Division, Research and Technology Group, is currently investigating empirical methods to answer process-type questions and logical methods to answer product-type questions. The remainder of the presentation discusses the second of these two avenues of research.
A team led by Ricky W. Butler has been studying the discipline of formal methods for over 6 years. Other civil-servants on the team are Jim L. Caldwell, Victor A. Carre๑o, C. Michael Holloway, and Paul S. Miner. Vigyan, Inc., Stanford Research Institute International (SRI), Odyssey Research Associates (ORA), and Computational Logic, Incorporated (CLI) conduct research under contract.
Formal methods is the applied mathematics of computer systems engineering. Formal methods aims to be to software engineering what fluid dynamics is to aeronautical engineering and what classical mechanics is to civil engineering. The mathematics of formal methods includes predicate calculus (first order logic), recursive function theory, lambda calculus, programming language semantics, and discrete mathematics (e.g., number theory, abstract algebra). To this mathematical base, formal methods adds notions from programming languages such as data types, module structure, and generics.
There are many different types of formal methods with various degrees of rigor. The following is a useful classification of the possible degrees of rigor in the application of formal methods:
Level 0: No use of formal methods
Level 1: Formal specification (using mathematical logic or a specification language with formal semantics) of all or part of a system
Level 2: Formal specification at two or more levels of abstraction and paper-and-pencil proofs that the detailed specification satisfies the abstract one
Level 3: Like level 2, except paper-and-pencil proofs are replaced by formal proofs checked by a semi-automatic theorem prover.
Presently, a complete (level 3) verification of a large, complex system is impractical; however, application of formal methods to critical portions of a system is practical and useful.
The specification of a simple phone book provides a suitable simple example of many of the basic ideas and benefits of formal methods.
Interested individuals are encouraged to explore this collection.
A lot of ground has been covered in this presentation, but the most important point is simple:
Epistemology: It's important, learn about it
Software Engineering: It's immature, work on it
Formal Methods: It's promising, look for it
[Carlier and Chretienne, 1988]:
"Scheduling is to forecast the processing of a work by assigning resources to tasks and fixing their start times. [...] The different components of a scheduling problem are the tasks, the potential constraints, the resources and the objective function. [...] The tasks must be programmed to optimise a specific objective [...] Of course, often it will be more realistic in practice to consider several criteria."
Another definition has been put forward by [Pinedo, 1995]:
"Scheduling concerns the allocation of limited resources to tasks over time. It is a decision-making process that has as a goal the optimization of one or more objectives."
Sports scheduling is a particular area of scheduling theory which is closely related to timetabling problems: the aim in sports scheduling is usually to set a timetable of matches in a tournament or a championship. This kind of problem being hardly constrained it can be sometimes interesting to relax constraints into objectives, by the way leading to a multicriteria scheduling problem. [Wright, 2005] presents the particular case of the National Basketball League (NBL) of New Zealand.
Ten basket teams meet twice in home and away matches, leading for each team to eighteen matches in a season. As only fifteen week-ends are available to play the matches, all teams have at least one week-end with two matches, which does not simplify the problem 118 4. An approach to multicriteria scheduling problems because additional constraints exist on these "doubling up" week-ends (the two teams that meet in a doubling up week-end must meet away and must not be located too far from each other). Other constraints are also described.
Due to the complexity of the problem and the way a timetable is built by the NBL, most of the hard constraints are relaxed into objectives which are equal to 0 when the original related constraint is met. This leads to a total of twenty criteria minimised in a convex combination reflecting the total cost of constraint violation.
Why is schedule planning hard?
Traditional schedule planning processes utilize a stepwise, often manual, work-flow to allocate sport-venues and booking reservations constraints and match preferences. This approach is cumbersome, and does not flexibily adapt to changes in constraints, or sport-venues availability. Sport-venues and team availability are often not coordinated, and many systems do not consider home/away binding constraints. Thus, with this approach often convergent schedules cannot be obtained. However, despite attempts to move to the Constellation system, attempts have always been successful.