Building a refinement checker for Z
In previous work we have described how refinements can be checked using a temporal logic based model-checker, and how we have built a model-checker for Z by providing a translation of Z into the SAL input language. In this paper we draw these two strands of work together and discuss how we have impl...
| Principais autores: | , , |
|---|---|
| Formato: | Artigo |
| Idioma: | English |
| Publicado em: |
Open Publishing Association
2011-06-01
|
| coleção: | Electronic Proceedings in Theoretical Computer Science |
| Acesso em linha: | http://arxiv.org/pdf/1106.4092v1 |