Métodos Formais em Engenharia de Software

MIEIC — 4º ano

2013/14

Links úteis:

Alloy

Alloy web site: http://alloy.mit.edu/

 

             Livro:  http://tuyendungit.files.wordpress.com/2011/05/software-abstractions-logic-language-and-analysis.pdf

 

VDM:

VDM information web site: http://www.vdmtools.jp/en/index.php

 

VDM site: http://www.vdmportal.org/twiki/bin/view

 

VDM++: Manual da linguagem

 

VDMTools: Manual da ferramenta

 

VDMTools: ligação ao Rational Rose

 

VDMTools: Tutorial for Overture/VDM++

 

The VDM Examples Repository: http://www.csr.ncl.ac.uk/vdm/examples/examples.html

 

More examples:

http://lml.ls.fi.upm.es/rsd/Papers/Presentation-Topics/VDM/vdm-examples/examples.html

 

VDM versão 8.1 Academic

Spin

Spin Model Checking: http://spinroot.com/spin/whatispin.html

 

Basic Spin Manual: http://www.spinroot.com/spin/Man/Manual.html 

 

Spin online references: http://www.spinroot.com/spin/Man/index.html

 

Promela: http://www.dai-arc.polito.it/dai-arc/manual/tools/jcat/main/node168.html

Coq

Coq proof assistant: http://coq.inria.fr/

 

Coq’Art: http://www.labri.fr/perso/casteran/CoqArt/coqart80.tar.gz

Jape

Jape proof assistant: http://jape.comlab.ox.ac.uk:8080/jape/

Krakatoa

Krakatoa tool for Java Programs Verification: http://krakatoa.lri.fr/krakatoa0.html

Caduceus

Caduceus tool for C Programs Verification: http://caduceus.lri.fr/

e mais ….

Formal Methods Europe