Hardware Behavioural Modelling, Verification and Synthesis with UML 2.x Activity Diagrams

Modelling of hardware behavior is the fundamental process of hardware design project. Possible specification techniques, like UML 2.x Activity Diagrams or Control Interpreted Petri Nets, all have its advantages and disadvantages. Combing the accessibility of UML and full support for formal verification of Petri nets may significantly improve design quality. The article propose a system supporting logic controllers development, starting from a specification, going through formal verification (including model checking), and ending with synthesis.