May-happen-in-parallel analysis of ESL models using UPPAAL model checking

In this paper, we propose an approach for May-Happen-in-Parallel (MHP) analysis of electronic system level (ESL) design which models parallel discrete event simulation with concurrent automaton processes and formally identify those MHP states. Our MHP analysis utilizes formal verification by use of the UPPAAL model checker. The proposed approach converts the system model in SpecC SLDL into an UPPAAL model and generates a set of queries that automatically and completely finds all possible MHP pairs. The experimental results show our approach can report more precise MHP analysis results compared to other works at the cost of extended analysis run time.