The compliance notation provides a cost-effective method where both formal and informal techniques can be employed in software verification. The notation has been successfully applied in verifying industrial safety-critical systems, but currently it has no support for verifying concurrent systems. This work extends the compliance notation with appropriate support for verifying concurrent systems. The new notation comprises: Circus, Ravenscar (a safe subset of Ada), and a refinement method from Circus specifications into Ravenscar programs.
Department of Computer Science
Deramore Lane, University of York, Heslington, York, YO10 5GH, UK
Tel: 01904 325500 | Fax: 01904 325599