Conclusion and Future
Easy-to-use verification tool for Esterel
- User-friendly GUI, BDD-based (TiGeR)
- Model minimization for early verification of small module
- Model-checking for non-expert users
Future
- Real industrial systems (Dassault Aviation)
- Forward liveness property checking (implemented, no interface yet)
- Exploit structural information from source
- Guided state space search
- Datapath, modularity, etc..
http://www.inria.fr/meije/esterel/verification