Observatorio de I+D+i UPM

Memorias de investigación
Artículos en revistas:
Modeling Concurrent Systems with Shared Resources
Año:2009
Áreas de investigación
  • Lenguaje de programación
Datos
Descripción
Testing is the more widely used approach to (partial) system validation in industry. The introduction of concurrency makes exhaustive testing extremely costly or just impossible, requiring shifting to formal verification techniques. We propose a methodology to design and verify a concurrent system that splits the verification problem in two independent tasks: internal verification of shared resources, where some concurrency aspects like mutual exclusion and conditional synchronisation are isolated, and external verification of processes, where synchronisation mechanisms are not relevant. Our method is language independent, non-intrusive for the development process, and improves the portability of the resulting system. We demonstrate it by actually checking several properties of an example application using the TLC model checker.
Internacional
Si
JCR del ISI
No
Título de la revista
Lecture Notes in Computer Science
ISSN
0302-9743
Factor de impacto JCR
0
Información de impacto
Volumen
5825
DOI
Número de revista
0
Desde la página
102
Hasta la página
116
Mes
ENERO
Ranking
Esta actividad pertenece a memorias de investigación
Participantes
  • Autor: Angel Herranz Nieva (UPM)
  • Autor: Juan Jose Moreno Navarro (UPM)
  • Autor: Manuel Carro Liñares (UPM)
  • Autor: Julio Mariño Carballo (UPM)
Grupos de investigación, Departamentos, Centros e Institutos de I+D+i relacionados
  • Creador: Grupo de Investigación: BABEL: Desarrollo de Software Fiable y de Alta Calidad a partir de Tecnología Declarativa
  • Grupo de Investigación: Computación lógica, Lenguajes, Implementación y Paralelismo (CLIP)
  • Departamento: Lenguajes y Sistemas Informáticos e Ingeniería de Software
S2i 2021 Observatorio de investigación @ UPM con la colaboración del Consejo Social UPM
Cofinanciación del MINECO en el marco del Programa INNCIDE 2011 (OTR-2011-0236)
Cofinanciación del MINECO en el marco del Programa INNPACTO (IPT-020000-2010-22)