Grupo de Ingeniería Microelectrónica

Grupo de Ingeniería Microelectrónica

Departamento de Tecnología Electrónica, Ingeniería de Sistemas y Automática Universidad de Cantabria
Home   Personas   Investigación   Docencia   Doctorado   Publicaciones   Herramientas   Bolsa de Empleo   english version Sun 08-Dec-24 . 10:27



Mapa Web


Localización

Noticias

Info Santander



Gestión BD

GIM>Investigación>Publicación
   PUBLICACION
 
   Ficha completa
Título:Towards a Verification Flow Across Abstraction Levels: Verifying Implementations Against Their Formal Specification
Tipo:Articulo en revista internacional
Lugar:TCAD
Fecha:2017-03
Autores: Pablo González
Pablo Pedro Sánchez
Líneas: Verificación de sistemas embebidos
Proyectos:
ISBN:
Fichero:
Resumen: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 re-used 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 work, 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. The 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.
© Copyright GIM (TEISA-UC)    ¤    Todos los derechos Reservados.    ¤    Términos LegalesE-Mail Webmaster