Summer School on Specification, Refinement and Verification
Lecture abstracts
|
Martin Abadi
Refinement and verification techniques
in security
|
|
Because the development of secure systems is notoriously error-prone,
a number of techniques have been applied to proving properties
such as authenticity and secrecy. For example, in the last decade,
formal and semi-formal methods have been helpful in the analysis
of cryptographic protocols and mobile code. Principled methods
have also been proposed and employed for the design of secure
systems; even stepwise refinement is sometimes viable, despite
fundamental difficulties. These lectures will review some design
and verification methods in the context of security. The main
examples will be authentication protocols and mobile Java code.
The formalisms used will include logics, type systems, and process
calculi.
| |
Jean-Raymond Abrial
Practical Techniques for the Automatization of Mechanical Proofs
|
- Why automatize mechanical proofs (figures in industrial formal
developments).
- Some logical concepts (formula, sequent, inference). Practical
application to Propositional Calculus proofs.
- More logical concepts (quantification, substitution). Practical
application to Predicate Calculus proofs.
- Some set-theoretic concepts (axioms, definitions). Practical
application to set-theoretic proofs.
- Some arithmetic concepts. Practical application to arithmetic
proofs.
Each step will be illustrated with corresponding automatic proofs that
will be demonstrated to the students.
| |
Ralph-Johan Back
Refinement Calculus as a framework for program construction
|
|
We give an overview of the basic notions underlying the refinement calculus
approach to program construction. This calculus provides a unified approach
to the rigorous derivation of correct and efficient programs that satisfy a
given specification. The refinement calculus is formalized in higher order
logic, while its mathematical basis is lattice theory. The calculus is
very versatile: in addition to ordinary programs it also allows us to model
interactive programs, games and general contracts between two or more
parties, to refine these and to analyze their correctness. We show the
applicability of the calculus with a few case studies.
| |
Orna Grumberg
Model Checking techniques for Hardware and
Software Verification
|
|
We will consider the verification of finite-state systems (such as
digital circuits and communication protocols) with respect to
specifications written in propositional temporal logics.
For such systems the verification problem can be decided efficiently
using model checking algorithms.
Temporal logic model checking is a procedure that given a finite-state
system and a temporal logic formula determines whether the
system satisfies the formula or not.
We will define several temporal logics, compare their expressive power, and
survey model checking algorithms for them. We will show how to avoid
the high space requirements of these algorithms by representing
the verified system as a Binary Decision Diagram (BDD).
The necessary background on temporal logics, binary decision diagrams,
and model checking will be introduced.
Other methods to reduce space requirements, such as abstraction
and modularity will be presented.
| |
Eric Hehner
A practical theory of programming
|
|
Theories come in different strengths for different purposes. I
will present a simple theory that is adequate for most programming. I hope
to cover sequential and parallel constructs, batch and interactive
computation, terminating and nonterminating behaviors, and data
transformation, with emphasis on time and space complexity. The theory
uses boolean expressions for specifications and program semantics, and
implication for refinement; proofs remain within ordinary first-order
logic. I will mention the limitations of the theory: a stronger theory
(predicate transformers, higher-order logic) is required for loop semantics
(but not loop proofs).
Eric C.R. Hehner: a Practical Theory of Programming. Springer,
New York, 1993. 244 pages.
| |
Reino Kurki-Suonio
Incremental specification in a TLA-based approach to object systems
|
|
The lectures are based on the following observations/claims: (1) managing
the complexity of interactive systems requires rigorous specification and
design methods, (2) interactive behaviors are generated by closed systems
only, (3) decomposition does not reduce complexity, (4) logical modularity
can be imposed by layers that provide closed-system abstractions of the
final system. Using a TLA-based formal basis and an execution model of
multi-object actions, the lectures describe two-dimensional specification
architectures, where component structure is orthogonal to logical
modularity. The topics include refinement and synthesis of specification
layers, component refinement in closed systems, and generalization of
object-oriented inheritance to multi-object actions.
| |
Kaisa Sere
System Design with Action Systems
|
|
Action systems is a framework intended for the systematic development
of parallel and distributed systems. The theoretical basis for the
formalism is the Refinement Calculus within which we can verify,
transform, and refine action systems. During this series of
lectures we will introduce the action systems formalism together with
the needed refinement notions. The focus will be on the s.c. data
refinement techniques. Therafter we will present applications of
action systems in system design mainly within specification,
development of distributed and control systems as well as within
hardware design.
| |
Joakim von Wright
Program Refinement and Theorem Proving: Modeling and Tool Support
|
|
Theorem proving systems allow us to embed the syntax and the semantics
of a theory in a mechanised logic, and to do computer-supported
formal reasoning within the embedded theory. We show how the
refinement calculus is formalised in higher-order logic, which is
the object-logic of the HOL theorem proving system. Furthermore, we
show how the reasoning paradigms of program refinement are modeled.
Finally, we discuss experiments with a program refinement tool based
on the HOL formalisation of the refinement calculus.
| |
Pamela Zave
Specification and verification of telecommunication services
|
|
Telecommunication systems are communication networks intended for
real-time transmission of continuous media such as voice and video.
Telecommunication systems are distributed, long-lived, and complex.
Telecommunication software suffers from all the usual problems of
legacy software, plus a host of more specialized problems including
chaotic feature interaction, a critical need for interoperability,
a critical need for separation of user-oriented from resource-oriented concerns,
and an ongoing revolution in communication technology.
There is no doubt that telecommunication software could benefit in many
ways from formal methods, and there has been much research activity in this
area, but until recently no formalization has emerged with the ability to
describe the behavior of a realistic system at a level of abstraction
significantly above that of the implementation.
Distributed Feature Composition (DFC) is a new
technology for describing telecommunication services.
It is based on a virtual
architecture that is designed specifically for feature modularity, and
that offers benefits analogous to those of a pipe-and-filter
architecture in other application domains.
The DFC virtual architecture is first presented informally, with numerous
examples to show its potential for managing behavioral complexity and
for addressing other telecommunication problems.
Next the DFC virtual architecture is presented formally, for the
purpose of laying a foundation for future work on verification.
This presentation includes placing the architecture in a context
relating it to the concepts of
requirements, specification, and implementation as
they are widely understood.
It also includes the use of several formal languages.
Finally the subject of verification of telecommunication requirements
is addressed.
Examples of these properties partial requirements rather
than complete ones are presented, and possible proof strategies
are discussed.
It is easiest to think about verifying closed telecommunication systems, but
the DFC virtual architecture has a composition property that might
make open (interoperating) telecommunication systems verifiable as
well.
| |
|