A proven translation from a UML state machine subset to timed automata

“

We want to extend our source model (SM) to take into account additional features that are not considered so far in our translation, such as final states, History pseudo-states, entry/exit/do behaviors and forks/joins. We also wish to minimize the number of timed automata clocks generated through our translation. A possible way is to create clocks dynamically as in time Petri Nets, or Stateful Timed CSP. We should also mention that in the current study, we mainly focused on the soundness of the translation and the timed bisimulation preservation. This explains some choices such as, for instance, regarding the syntax statement, to help us derive our proof. Nevertheless, some abstraction should be possible regarding the way the utilized syntaxes are stated. Moreover, to be able to conduct our translation and prove the equivalence, we had to fix several choices in terms of syntax and semantics in both the source and target models. Yet, regarding the possibility to adopt different choices and/or extend the subset of the UML SM specifications to consider, we believe that the present contribution can serve as a relevant basis. In addition, after having manually demonstrated the existence of a bisimulation relation between SMs and TA, we are paving the way for validating our translation process by theorem provers. Indeed, by bringing a completely (manual) formal translation, that is entirely based on set theory, we have shown that the translation is perfectly encodable using theorem prover tools. What may prove to be harder, nevertheless, is the handling of bisimulation and its proof. We believe that, if a support to our translation is set by means of a theorem prover, for instance, this would greatly simplify coping with different choices and/or extensions regarding the considered subset of UML SMs.

”