Observatorio de I+D+i UPM

Memorias de investigación
Research Publications in journals:
Modeling Concurrent Systems with Shared Resources
Year:2009
Research Areas
  • Programming language
Information
Abstract
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.
International
Si
JCR
No
Title
Lecture Notes in Computer Science
ISBN
0302-9743
Impact factor JCR
0
Impact info
Volume
5825
Journal number
0
From page
102
To page
116
Month
ENERO
Ranking
Participants
  • Autor: Angel Herranz Nieva (UPM)
  • Autor: Juan Jose Moreno Navarro (UPM)
  • Autor: Manuel Carro Liñares (UPM)
  • Autor: Julio Mariño Carballo (UPM)
Research Group, Departaments and Institutes related
  • 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 2019 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)