Distributed behavioral cartography of timed automata

Real-time systems, characterized by a set of timings con-stants (internal delays, timers, clock speeds), need to be perfectly reliable. Formal methods can prove their correct-ness but, if one of the timing constants changes, verifica-tion needs to be restarted from scratch. Also, variations of some delays (even infinitesimal) may lead to the specifica-tion violation. It is thus interesting to reason parametrically, and synthesize constraints on the timing constants seen as parameters to formally guarantee the specification. We pro-pose here an attempt to distribute a synthesis algorithm, the behavioral cartography, and we evaluate two work distribu-tion algorithms. The parallelization gives promising results and opens perspectives toward verification of larger models