Modeling Concurrent Systems with Shared Resources

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

Description

Title: Modeling Concurrent Systems with Shared Resources
Author/s:
  • Herranz Nieva, Ángel
  • Mariño Carballo, Julio
  • Carro Liñares, Manuel
  • Moreno Navarro, Juan José
Item Type: Presentation at Congress or Conference (Article)
Event Title: 14th International Workshop on Formal Methods for Industrial Critical Systems
Event Dates: 02/11/2009 - 03/11/2009
Event Location: Eindhoven, Holanda
Title of Book: Proceedings of 14th International Workshop on Formal Methods for Industrial Critical Systems
Date: 2009
ISBN: 978-3-642-04570-7
Volume: 5825
Subjects:
Faculty: Facultad de Informática (UPM)
Department: Lenguajes y Sistemas Informáticos e Ingeniería del Software
Creative Commons Licenses: Recognition - No derivative works - Non commercial

Full text

[img]
Preview
PDF - Requires a PDF viewer, such as GSview, Xpdf or Adobe Acrobat Reader
Download (325kB) | Preview

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.

More information

Item ID: 5712
DC Identifier: http://oa.upm.es/5712/
OAI Identifier: oai:oa.upm.es:5712
Official URL: http://www.springerlink.com/content/b83m037648436667/
Deposited by: Memoria Investigacion
Deposited on: 18 Jan 2011 08:33
Last Modified: 20 Apr 2016 14:27
  • Logo InvestigaM (UPM)
  • Logo GEOUP4
  • Logo Open Access
  • Open Access
  • Logo Sherpa/Romeo
    Check whether the anglo-saxon journal in which you have published an article allows you to also publish it under open access.
  • Logo Dulcinea
    Check whether the spanish journal in which you have published an article allows you to also publish it under open access.
  • Logo de Recolecta
  • Logo del Observatorio I+D+i UPM
  • Logo de OpenCourseWare UPM