Keynote Lecture
Formal Methods Europe
Berlin, March 14, 2001

Formal methods have offered great benefits, but often at a heavy
price. For everyday software development, in which the pressures
of the market don't allow full-scale formal methods to be applied,
a more lightweight approach is called for. I'll outline an
approach that is designed to provide immediate benefit at
relatively low cost. Its elements are a small and succinct
modelling language, and a fully automatic analysis scheme that can
perform simulations and find errors. I'll describe some recent
case studies using this approach, involving naming schemes,
architectural styles, and protocols for networks with changing
topologies. I'll make some controversial claims about this
approach and its relationship to UML and traditional formal
specification approaches, and I'll barbeque some sacred cows, such
as the belief that executability compromises abstraction.

Includes sneak preview of new version of Alloy, with structuring
mechanism and arbitrary-arity relations.

Downloads

Slides