Reusing of Properties after Discretization of Hybrid Automata

In the recent years, the use of hybrid automata has achieved a great success in the early design and verification of embedded systems. Once the hybrid model defined by means of hybrid automata has been verified, it would be valuable to reuse it to refine a corresponding hardware/software implementation. Some works have proposed the automatic refinement of hybrid automata specifications into HW/SW implementations, but they refine in a systematic way only particular classes of hybrid automata. Thus, in general, the manual refinement of an implementation is still required. In this context, the reuse of formal properties defined for verifying the hybrid model is still an interesting open issue. This paper is intended to fill in the gap by proposing a methodology that refines the set of properties defined for hybrid automata to check the correctness of their corresponding SystemC implementations. Experimental results show the applicability and the effectiveness of the proposed methodology.