We offer to implement in hardware a Sleptsov Net Machine, which we recently implemented as software machines on many platforms, including multicore CPU, and GPU. Please see presentation of its recent implementation for Arduino on
Using formal methods of embedded system design allows us to use formal verification of a control system alone and integrated with the plant model that yields reliable embedded systems. Application graphical languages of embedded system design was a success for years with Siemens's ladder diagrams.
An Sleptsov net (SN) is a Turing-complete graphical language able to specify any given concurrent algorithm. There is a wide range of formal techniques to verify an SN, both specific and inherited from Petri nets, which an SN generalizes. Please see our example of robotic plant control with Petri nets.