Mapa Web
Localización
Noticias
Info Santander
Gestión BD
|
| GIM>Investigación>Verificación de sist... |
| LINEA DE INVESTIGACION: |
| | Verificación de sistemas embebidos |
| Seguir estos links para ver los PROYECTOS o PUBLICACIONES dentro de esta línea de investigación |
| |
| PERSONAS: |
Pablo Pedro Sánchez (Responsable de esta línea de investigación)
Eugenio Villar
Iñigo Ugarte
Fernando Herrera
|
| CAMPOS DE TRABAJO: |
Como se ha comentado previamente, esta línea de investigación nace de la experiencia adquirida en el desarrollo de técnicas de síntesis para test y esta fuertemente ligada con otras líneas de investigación del grupo, como las de especificación y co-diseño de sistemas embebidos. En este sentido se han desarrollado varios "planes de verificación" en proyectos de diseño [UgSV02][BCHP03a][BCHP03b].
El desarrollo de técnicas de verificación de sistemas embebidos se inició durante la estancia del Profesor Pablo Sánchez en la Universidad de San Diego (USA). Durante dicha estancia, se exploraron técnicas aplicables a sistemas que pudiesen ser descritos mediante polinomios [SaDe99]. El objetivo de dichas técnicas es encontrar valores de las entradas que violen algunas de las propiedades o restricciones introducidas por el usuario en la especificación del sistema. Se han estudiado dos formas diferentes de afrontar el problema. La primera que se ha estudiado se basa en una aritmética de intervalos modificada [UgSa03a]. Dicha aritmética ha sido utilizada para verificar sistemas descritos a nivel algorítmico sin lazos [UgSa03b],[UgSa03c], como con lazos [UgSa04a],[UgSa04b], [UgSa05f]. Esta actividad se desarrolló dentro del proyecto CICYT anteriormente citado [PRO03]. La segunda forma de afrontar el problema se basa en la utilización de un solucionador de ecuaciones no lineales para descripciones de un sólo proceso [UgSa05a], [UgSa05b].
Otro de los campos de estudio es la exploración de métodos que proporcionen un significado formal de las métricas de cobertura en verificación de diseños hardware basado en simulación con vectores aleatorios [UgSa05c], [UgSa05d], [UgSa05e].
La experiencia en el simulador SystemC ha permitido realizar una modificación del mismo al objeto de asegurar una selección pseudo-aleatoria de los procesos. La técnica propuesta permite mejorar la calidad del proceso de verificación al explorar distintos modos posibles de ejecución de los procesos concurrentes del sistema [HeVi06b]. Esta actividad se desarrolló dentro del proyecto CICYT [PRO05]. En el proyecto IST 033511 ANDRES se desarrolló una extensión del núcleo de simulación estándar de SystemC al objeto de soportar la cobertura exhaustiva de planificaciones de partes críticas de la especificación SystemC en las que la actividad concurrente puede causar indeterminismo [HeVi09].
|
|
|
