Automating Refinement of Circus Programs

Frank ZeydaAna Cavalcanti

In previous work, we have presented a mechanisation of Circus for the theorem prover ProofPowerZ. Circus is a refinement language for state-rich reactive systems that combines Z and CSP. In this paper, we present techniques to automate the discharge of proof obligations typically generated by the Circus refinement laws. They eliminate most of the proofs that are imposed by the fact that the encoding has to be precise about typing and well-definedness issues, and leave just those that are expected in a pen-and-paper refinement. This allows us to concentrate on the proof of properties that are significant for the problem at hand, while benefiting from the increased assurance and efficiency afforded by the use of a theorem prover as well as high-level tactic languages for refinement. Our case study is a refinement strategy for verification of control systems; we present the result of several experiments.

Caso o link acima esteja inválido, faça uma busca pelo texto completo na Web: Buscar na Web

Biblioteca Digital Brasileira de Computação - Contato:
     Mantida por: