ProjectDEVS is made of a Java GUI for designing prototypes with an abstract syntax, a set of correct transformations of the abstract syntax and their semantics to TPN, TPN players embedded in different target and a controller mastering the commnication.

Take a look at the poster presenting the Project DEVS summary:

ProjectDEVS features:

Modularity: a model is constructed by coupling concurrent components exchanging data through ports. The TPN model preserves the modularity with a formal background for correct decomposition, synchronisation and communication of the model parts to be deployed on different platforms.

Syntax-Semantic separation: model components have an abstract syntax based on input/output timed automata. Their interations can be driven by differents semantics.

Bi-similar transformations: designed model is automatically transformed into a correct TPN. Each semantics are formally specified using timed transition system to verify the correctness of the implementation.

Semantics: sequential, conservative parallel, time warp optimistic parallel, riskfree optimistic parallel

System application :  control/command, computer network, digital circuit, physical systems

Discrete-event simulation of hybrid systems : QSS numerical integrators libraries are coupled with discrete-event simulation to offer an efficient mechanism for asynchronous hybrid systems simulation.

Component heterogeneity : a component has heterogeneous form. It can be a variable, an equation, a finite state machine, a library, a Fonctional Mockup Unit, a software object.

Cosimulation and Model Exchange : FMI wrapper to synchronise discrete-time simulators (matlab, modelica...) with discrete-event simulators using FMI++. Only import functionnalities (for cosimulation and model exchange) are implemented. No FMI export.

Hardware : VHDL code is generated in a synthesizable form which can be used on a FPGA. Interfaces for buses used by Xilinx and Altera, AXI and Avalon, are generated along with the model code.

Model checking : abstract semantics covers all the possible cases of the concrete semantics such that traces, marking, state and branching are preserved. Model checking to verify absence of deadlock, detect non determinism,  ensure reachability  or safety, can be performed onto the abstract model domain using the TINA toolbox. This feature is limited to every model that contains only finite state machines with bounded integers domain of value.