Carlos Olarte
Associated Professor
Université Sorbonne Paris Nord, France
Rewriting Modulo SMT Techniques for Parametric Analysis (joint work with J.
Arias, K. Bae, P. Ölveczky, L. Petrucci and F. Rømming).
Many computer systems today are real-time systems whose correctness depend
crucially on time and on the correct values of their parameters. However,
in system design we often do not know in advance the concrete values of key
system parameters, and want to find those values that make the system
behave as desired. Parametric timed automata (PTA) extend timed automata to
the case where the values of some system parameters are unknown. Similarly,
Parametric time Petri nets (PITPN) extend time Petri nets to the setting
where bounds on when transitions can fire are (partially) unknown.
In this talk, we will see how the behavior of PTAs and PITPNs can be
adequately captured in the framework of rewriting logic modulo SMT. The
proposed rewriting semantics is correct with respect to the standard
semantics of PTAs and PITPNs, and it is executable in the Maude system
connected with SMT solvers. Different analyses including EF-synthesis
(computing values for the parameters to reach a state satisfying a
property) and AG-safety-synthesis (values for the parameters to avoid some
states) can be solved by Maude. Furthermore, our approach also supports
analysis combined with user-defined execution strategies and full LTL model
checking.