Formal Verification of Stateflow Diagrams Using SMV
Testing and verification in industry is normally accomplished using
either trial and error or with random test vector generation. These
techniques are not guaranteed to be successful. Formal verification
is a field of study that IS guaranteed for success.
There are two categories of formal verification, model checking and
theorem proving. Model checking exhaustively searches all
paths and checks against all invariants. Theorem proving
interatively forms a mathematical proof and then checks the invariants
against the proof.
SF2SMV uses the model checking approach to formally verify Stateflow
diagrams.
News
03/12/2002
I just graduated, so I am leaving for my full
time job. I posted my thesis for your viewing pleasure. It's available
in the downloads section.
03/12/2002
I finally decided to get a real HTML editor and the
updates are going well. There will be some real improvements soon. On
another note: In order to be as confusing as possible, I changed the name
of SM2SMV back to SF2SMV. SM2SMV originally supported state machines only,
but it eventually acquired some characteristics not associated with pure
state machines. In the end, it's better this way.
03/07/2002
After a long delay, a new major version of SM2SMV
is now available. It includes some major performance improvements.
It has been posted on the downloads page.
8/22/2001
A small update today. Along with a bug fix
(and corresponding new version), we also have a user's guide! How
snazzy. The new user's guide has two parts, installation and
GUI description. --This has been temporarily removed--
Also, SMV has a new version. So, go
download it.
8/7/2001
Well, here it is. SM2SMV v1.0 is available
on the downloads page. Please note
that you must have Matlab 6.0 and SMV installed on your computer before
using this software.
6/14/2001
After a short break (ok, long break), the site has
been updated. Check the downloads section for 2 new additions: Poster
layouts from the ICES Symposium last October and the PITA Advisory Board
Meeting earlier today.
4/27/2001
Revamped the overall organization of the page to
make it more intuitive. Any comments or suggestions would be appreciated.
4/5/2001
New section, SM2SMV, was added.
3/1/2001
Synopsis and Sponsors added.
2/22/2001
This is the new and improved SF2SMV website. Please be
patient while I continue to update it.
2/22/2001
First order of business: The links on the left side
of the page will point to separate pages (at least that is the plan).