| Using
SMV |
|
|
|
|
|
|
|
|
|
|
| • | SMV
is a BDD-based model checker |
||||||||
| • | It
checks CTL formulas |
||||||||
| – | A
specific temporal logic |
||||||||
| • | We
developed reasonably efficient |
||||||||
| techniques
for mapping RSML to SMV, |
|||||||||
| including
the state hierarchies |
|||||||||
