i2smv - A Interactors to SMV translation tool
i2smv - Ferramenta de tradução de Interactors para SMV
- Description
- i2smv is a prototype tool for the translation of Interactors to the SMV input language. Interactor behaviour is specified using Modal Action Logic (MAL). i2smv enables interactive systems models expressed with the MAL Interactors notation to be analysed using the SMV model checker.
- We are currently developing a new version of the tool which will include a models' editor.
- Related publications
- J. C. Campos and M. D. Harrison (1999) Using automated reasoning in the design of an audio-visual communication system. In D. J. Duke and A. Puerta, editors, Design, Specification and Verification of Interactive Systems '99, Springer Computer Science, pages 167-188. Springer-Verlag/Wien.
abstract
- J. C. Campos and M. D. Harrison (1999) From Interactors to SMV: A Case Study in the Automated Analysis of Interactive Systems. Technical Report YCS-99-317, Department of Computer Science, University of York.
gzip'ed postscript
- J. C. Campos (1999) Automated Deduction and Usability Reasoning. DPhil thesis, Department of Computer Science, University of York.
(Also available as Technical Report YCST 2000/9, Department of Computer Science, University of York)
gzip'ed postscript
- J. C. Campos and M. D. Harrison (2001) Model Checking Interactor Specifications. Automated Software Engineering, 8(3/4):275-310, August.
abstract
| link
- Downloads
- i2smv tool: send a request to
