Estamos realizando la búsqueda. Por favor, espere...

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

Abstract: 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.

 Autoría: Gonzalez-De-Aledo P., Przigoda N., Wille R., Drechsler R., Sanchez P.,

 Fuente: IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2017, 36(3), 475-488

 Editorial: Institute of Electrical and Electronics Engineers

 Fecha de publicación: 01/03/2017

 Nº de páginas: 14

 Tipo de publicación: Artículo de Revista

 DOI: 10.1109/TCAD.2016.2611494

 ISSN: 1937-4151,0278-0070

 Proyecto español: TEC2014-58036-C4-3-R ; BES-2012-055572

 Url de la publicación: https://doi.org/10.1109/TCAD.2016.2611494