Modeling Concurrent Systems with Shared Resources

Herranz Nieva, Ángel; Mariño Carballo, Julio; Carro Liñares, Manuel y Moreno Navarro, Juan José (2009). Modeling Concurrent Systems with Shared Resources. En: "14th International Workshop on Formal Methods for Industrial Critical Systems", 02/11/2009 - 03/11/2009, Eindhoven, Holanda. ISBN 978-3-642-04570-7.

Descripción

Título: Modeling Concurrent Systems with Shared Resources
Autor/es:
  • Herranz Nieva, Ángel
  • Mariño Carballo, Julio
  • Carro Liñares, Manuel
  • Moreno Navarro, Juan José
Tipo de Documento: Ponencia en Congreso o Jornada (Artículo)
Título del Evento: 14th International Workshop on Formal Methods for Industrial Critical Systems
Fechas del Evento: 02/11/2009 - 03/11/2009
Lugar del Evento: Eindhoven, Holanda
Título del Libro: Proceedings of 14th International Workshop on Formal Methods for Industrial Critical Systems
Fecha: 2009
ISBN: 978-3-642-04570-7
Volumen: 5825
Materias:
Escuela: Facultad de Informática (UPM) [antigua denominación]
Departamento: Lenguajes y Sistemas Informáticos e Ingeniería del Software
Licencias Creative Commons: Reconocimiento - Sin obra derivada - No comercial

Texto completo

[img]
Vista Previa
PDF (Document Portable Format) - Se necesita un visor de ficheros PDF, como GSview, Xpdf o Adobe Acrobat Reader
Descargar (325kB) | Vista Previa

Resumen

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.

Más información

ID de Registro: 5712
Identificador DC: http://oa.upm.es/5712/
Identificador OAI: oai:oa.upm.es:5712
URL Oficial: http://www.springerlink.com/content/b83m037648436667/
Depositado por: Memoria Investigacion
Depositado el: 18 Ene 2011 08:33
Ultima Modificación: 20 Abr 2016 14:27
  • Open Access
  • Open Access
  • Sherpa-Romeo
    Compruebe si la revista anglosajona en la que ha publicado un artículo permite también su publicación en abierto.
  • Dulcinea
    Compruebe si la revista española en la que ha publicado un artículo permite también su publicación en abierto.
  • Recolecta
  • e-ciencia
  • Observatorio I+D+i UPM
  • OpenCourseWare UPM