Towards a verification flow across abstraction levels verifying implementations against their formal specification

Pablo Gonzalez-De-Aledo, Nils Przigoda, Robert Wille, Rolf Drechsler, Pablo Sanchez

Research output: Contribution to journalArticlepeer-review

7 Citations (Scopus)


The use of formal models to describe early versions of the structure and the behavior of a system has become common practice in industry. UML and OCL are the de-facto specification languages for these tasks. They allow for capturing system properties and module behavior in an abstract but still formal fashion. At the same time, this enables designers to detect errors or inconsistencies in the initial phases of the design flow-even if the implementation has not already started. Corresponding tools for verification of formal models got established in the recent past. However, verification results are usually not reused in later design steps anymore. In fact, similar verification tasks are applied again, e.g., after the implementation has been completed. This is a waste of computational and human effort. In this paper, we address this problem by proposing a method which checks a given implementation of a system against its corresponding formal method. This allows for transferring verification results already obtained from the formal model to the implementation and, eventually, motivates a new design flow which addresses verification across abstraction levels. This paper describes the applied techniques as well as their orchestration. Afterwards, the applicability of the proposed methodology is demonstrated by means of examples as well as a case study from an industrial context.

Original languageEnglish
Pages (from-to)475-488
Number of pages14
JournalIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems
Issue number3
Publication statusPublished - Mar 2017


  • C/C++/SystemC
  • model checking
  • SAT/SMT solvers
  • symbolic execution
  • verification


Dive into the research topics of 'Towards a verification flow across abstraction levels verifying implementations against their formal specification'. Together they form a unique fingerprint.

Cite this