Y2U: A Tool for Transforming Yakindu Statecharts to UPPAAL Timed Automata
Introduction
Statechart is a widely used model in designing complex systems, such as automobile, avionics, and medical systems. Yakindu statechart tool is an open-source tool kit based on the concept of statecharts and has been applied in realworld applications such as autonomous driving smart cars and Lego Mindstorms robot kits. It has a well-designed user interface and simulation and code generation functionality and hence enables rapid prototyping and validation with domain experts. Since validation by domain experts is not adequate for guaranteeing correctness and safety of safety-critical systems, formal verification, such as model checking, is required. Unfortunately, Yakindu does not provide formal verification capability.
Many safety-critical systems need special techniques to ensure the safety and correctness. Formal model based approach is appealing because it provides a unified basis for formal analysis to achieve the expected level of correctness and safety guarantees. It has been applied in many safetycritical areas such as automotive and aviation. However, one of the disadvantages of model checking tools, such as UPPAAL, is that it does not provide code generation functionality, therefore, system designers must manually translate formal models, such as the timed automata, into an executable model or executable computer language source code, which is known to be error-prone.
The research community has drawn great attention to transform system modeling specifications/languages to UPPAAL timed automata, such as UML (unified modeling language) statecharts, hierarchical timed automata (HTA), discrete event system specification for real-time (RTDEVS), and parallel object-oriented specification language (POOSL) [10]. Yakindu statecharts are similar to UML statecharts, but still have some differences. Therefore, existing tools can not be directly applied to transform Yakindu statecharts to UPPAAL timed automata.
To bridge the gap between formal verification and system modeling/simulation/implementation, we present the Y2U tool which automatically translates Yakindu statecharts to UPPAAL timed automata. As both the syntax and semantics of Yakindu and UPPAAL are different, to bridge the gap between Yakindu and UPPAAL models is a challenge. Our strategies are to build transformation rules for each element used in the two models and use these rules as the foundation for the transformation.
We use a simplified Sepsis medical model, which is derived from the Surviving Sepsis Campaign Guideline and val- idated by the physicians, as our case study to demonstrate the usage of the developed tool. With the Y2U, the system design process can be described as the following. The system designers use Yakindu to develop a statechart model and simulate the behaviors for their applications so that the domain experts can validate the model. Once a statechart model is validated, it is translated into UPPAAL timed automata using the Y2U tool and be formally verified to ensure that the correctness and safety properties always hold. If the model passes the formal verification, the system designers use Yakindu to generate Java or C code. Otherwise, the system designers modify the statechart model according to the verification results and start another design cycle until the formal verification is passed.
In this section, we present the design of the Y2U tool. As both the syntax and semantics of Yakindu and UPPAAL are different, the design strategies are to build transformation rules for each element used in the two models and use these rules as the foundation for the transformation.
Study Cases
Download
Download Link
