A tool for checking CSP||B specifications
Résumé
This paper reports about our experience with building a simple tool to assist us in the verification of CSP||B specifications. We present the Control Loop Invariant technique to check the consistency of a CSP||B specification. From this, we deduce the requirements of an assistant tool. The tool was developed in Ocaml. We discuss several issues observed during the development.
Domaines
Génie logiciel [cs.SE]
Origine : Fichiers produits par l'(les) auteur(s)
Loading...