Yakindu Statecharts
Yakindu is a statechart modeling tool that provides an environment for specification and development of event-driven systems. It can be used to design, simulate, and develop systems based on views defined by finite automata. The system behaviors are specified based on the active states. In Yakindu, the actions can be associated with both transitions and states.
Yakindu's meta models are similar to the concept of a finite automation as expressed in the UML notation. While Yakindu models are self contained with interfaces specified by events and variables. Yakindu's execution semantics are cycle driven as opposed to event driven, which allows processing concurrent events. Its execution semantics can also enable definition of event driven behaviors on top.
The syntax of events and actions in Yakindu is defined by a textual description language. While Yakindu provides live validation, it lacks formal verification of models as provided by model checking tools such as UPPAAL.
UPPAAL Timed Automata
UPPAAL is a tool that provides an environment for system design, simulation, validation, and verification. It is based on timed automata. UPPAAL is especially useful for systems that can be modeled as a combination of nondeterministic processes with finite control structure and realvalued clocks, communicating through channels or shared variables. The typical UPPAAL applications include real-time controllers, communication protocols, multimedia applications, and other domain applications where satisfying timing requirements is critical.
The model-checker in UPPAAL is based on timed automata theory, with its modeling language providing features such as bounded integer variables and urgency. UPPAAL's query language is used to define properties that need to be checked, which is a subset of Timed Computation Tree Logic (TCTL). Unlike Yakindu, the main purpose of UPPAAL is for model checking, and for verifying models with regards to requirement specifications.
