IFIP WG 2.9

I explained the motivation behind lightweight formal methods, and
presented Alloy, a new lightweight object modelling language. I
illustrated the simplicity of aspect by showing how it treats
partial functions. I showed how to use Alloy and its automatic
analyzer Alcoa to investigate the placement of gates in the BART
system, and to check that a gate policy has the intended safety
consequences. Finally, I explained why the problem of analyzing
Alloy models is hard -- often involving the consideration of
10^100 states -- but in practice usually possible in seconds.

Slides