It is desirable that any computer system meet its specifications,
and
for
some applications critical. However, verifying systems of realistic
size
and complexity in itself requires the help of computers. Techniques are
being developed which extend the classes of system which may be
reasoned
about using the CSP model checker FDR. Specifically, to include those
whose
parameterisations might lead to unboundedly large state spaces. Thus
enabling
the benefits of using a theorem prover to be gained in a model checking
environment for certain types of scalable system.
Related projects
CSP
Model Checking
Efficient
verification of software with replicated components