opaal model checker

opaal

opaal is a distributed/parallel (discrete time) model checker for networks of timed automata implemented in Python using MPI. opaal is designed to be easily extendible, such that different approaches can be prototyped quickly.

Architecture

Click to see large version

Presentations