2019/05/14 by Rebeka Farkas, Farkas, Rebeka, Tamás Tóth +5
Computer Science · Engineering · #Formal Methods in Verification #Fuel Cells and Related Materials #Software Testing and Debugging Techniques
paper · doi:10.14279/tuj.eceasst.76.1076
openalex publication_date 2024/03/25 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/01
Efficient techniques for reachability analysis of timed automata are zone-based methods that explore the reachable state space from the initial state, and SMT-based methods that perform backward search from the target states. It is also possible to perform backward exploration based on zones, but calculating predecessor states for systems with data variables is computationally expensive, prohibiting the successful application of this approach so far. In this paper we overcome this limitation by combining zone-based backward exploration with the weakest precondition operation for data variables. This combination allows us to handle diagonal constraints efficiently as opposed to zone-based forward search where most approaches require additional operations to ensure correctness. We demonstrate the applicability and compare the efficiency of the algorithm to existing forward exploration approaches by measurements performed on industrial case studies. Although the large number of states often prevents successful verification, we show that data variables can be efficienlty handled by the weakest precondition operation. This way our new approach complements existing techniques.