Tools for modeling and deploying hardware architectures
Petri nets: Theory and implementation

ROMÉO and TINA are toolboxes offering modeling, simulation, state-space abstraction generation and verification facilities for Petri and temporal networks. Both enable structural analysis, and include model-checkers (a fragment of TCTL for ROMÉO, SE-LTL and µcalculus for TINA). Both can interface with the C language. Differences include the ability to manipulate parameters with ROMEO and to compose Petri nets with TINA, as well as the use of priorities. ROMEO and TINA are free software programs under GPL license (CeCILL compatible for ROMEO). They both run on Windows, Linux...