Y2U: A Tool for Transforming Yakindu Statecharts to UPPAAL Timed Automata

Sepsis Test Case

We have evaluated and tested the Y2U tool on a proof of concept test case with 14 states, 25 transitions, and 10 shared variables specified as transformation requirements. The test case we evaluated is the transformaton of a simplified Yakindu Sepsis disease model. It involves a main executable disease model communicating with two organ automata systems through shared variables and interfaces.
The model is extracted from Sepsis pathophysiological models written in medical guidelines. The model can be executed by physicians. We are to formally verify the model to ensure their desirable behaviors always hold.

The Sepsis test case is available here.