Next: Grading Up: Concurrent and Real-Time Systems Previous: Instructor and Venue
Formal methods is an umbrella term that encompasses all the various formalisms and techniques for specifying and then verifying the behaviour of computing systems in a formal (or mathematical) way. They have had their share of success and failure. Formal methods are not fullproof and they cannot ever be foolproof since the problem of program verification is intimately related to the halting problem, which is in turn mathematically proven as being unsolvable, but in practice they have been tremendously successful. In particular formal methods are widely used in mission critical computing systems (whole incorrect behaviour can cause harm to humans or huge material losses or often both).
Formal methods techniques can be broadly classified in two categories. Like the name implies, algebraic methods use various algebraic formalisms. The most common formalism for specifying the behaviour of computing systems is a process algebra, with transition systems as the most common underlying semantical model. This lays the basis of comparing behaviours using several implementation relations; multiple such relations exist based on what behaviour of a system is (and is not) deemed observable; for example we can assume that we can only observe a system (so that we can check out its traces), but we can also assume that we can interact with the system by not allowing it to perform certain actions (case in which we can also check out its failures). The most successful practical application of formal methods is model-based testing.
Logical formal methods on the other hand use temporal logic for the specification of the desired properties of a system. Traditionally they also use a slightly different model of the behaviour of a system (but nonetheless pretty similar with transition systems) namely, Kripke structures. An algorithm then is used to establish whether the given logical formula (or specification) is observed by the system under test. The process is called model checking. There are in fact two main classes of temporal logic (linear and branching time, both with advantages and disadvantages) and therefore two main classes of model checking.
On top of all of the above real-time information can be introduced for the specification and verification of those systems for which correct behaviour is not given only by the right sequence of actions but also by the timing of these actions (real-time systems).
This course is an introduction in formal methods. Algebraic methods will be given a thorough consideration. For this purpose we use a particular process algebra called CSP (“Communicating Sequential Processes”). We pay special attention to model-based testing throughout this presentation. Next we cover temporal logic (both linear and branching time). A brief presentation of model checking algorithms is also planned. Time permitting, a (likely superficial) presentation of the additional issues and methods introduced by real time will also be given.
The following is a however tentative schedule:
| Introduction to formal methods | 1 week |
| Syntax and semantics of CSP | 2 weeks |
| System analysis using CSP | 3 weeks |
| Model-based testing | 1 week |
| Temporal logic | 2 weeks |
| Model checking | 1 week |
| Real-time specification and verification | 2 weeks |