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.

Reusing of Properties after Discretization of Hybrid Automata

DI GUGLIELMO, Luigi;FUMMI, Franco;PRAVADELLI, Graziano
2011-01-01

Abstract

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.
2011
9781457721014
embedded systems; hybrid automata; hybrid systems implementation; verification
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11562/376619
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
  • ???jsp.display-item.citation.isi??? 0
social impact