| This area concerns the use of the formal reasoning in the area of verification and testing of software (and hardware) systems, and the implementation of these formal reasoning systems in software tools. Foundational research in this area is concerned with axiomatic and algebraic approaches, most often rendered as deductive systems. A paradigm case is that of the lambda-calculus with its various typed extentions, as well as the general framework of rewriting (including term graph rewriting). Also the family of pi-calculi for mobile systems in concurrency are situated here. Often the framework of the deductive systems in this section is equational, as is the case in the axiom systems for process algebra; but a non-equational style of established importance is found in the SOS paradigm. The equational style is in many instances fruitfully employed to yield executable calculi corresponding to the axiomatizations based on deductions. The equational framework has turned out to be flexible enough to facilitate many extensions in a smooth way, in particular the inclusion of non-functional aspects such as time, probability, mobility etc. We distinguish three types of formal reasoning: Logical reasoning. This concerns the implementation and use of proof checkers and theorem provers such as PVS, COQ, HOL and others. Steadily, the power of these systems and their user-friendliness is improved. They are applied to mathematical proofs, and to correctness proofs of communication protocols and distributed algorithms. Algebraic reasoning. This concerns research on the algebraic verification of systems and its support by software tools, such as the Chi, mCRL2 and LOTOS toolkits. Industrial contacts in manufacturing and embedded systems are fostered in institutions like the Laboratory for Quality Software (LaQuSo) at the TU/e and RU, and the Embedded Systems Institute (ESI) in Eindhoven. Operational reasoning. Many industries (such as AT &T, Intel) nowadays use model checkers to verify formal models of their systems. Much research in this area concerns dealing with state explosion, by means of parallel verification algorithms, abstraction, partial order reduction, and symbolic methods. Often, formal verification is only applied to well-chosen key elements of a system, or instead of full verification, model-based testing is used. An important new development is software model checking, where not a model of the software is verified, but the software itself. Classic application areas of formal methods are embedded, distributed, hybrid and safety-critical systems. System properties that are verified mostly concern functional behavior, timing requirements, and probabilistic aspects. An important new application area is security. Formal reasoning is used in the analysis of security protocols, software security, and smartcards. Notable security issues (e.g. in on-line banking) that play an important role are confidentiality (protected, private data or communications should not be visible to unauthorized parties), integrity (private data should be protected against modification by unauthorized parties), availability (data and services should be protected against Denial of Service attacks, so that they are accessible by authorized parties), authenticity (parties involved in communication should have certainty about each other's identity), and non-repudiation (parties involved in communication should not be able to deny the actions that they performed). We envision that a key application area for the near future will be life sciences (e.g.\ formally specifying and analyzing the computational aspects of a living cell). |
