We present an experiment of applying existing verification tools for process algebra, namely ACTL model checker and AUTO, to a system based on parallel logic programming: Extended Shared Prolog (ESP). The constructed tool ESP-MC (a semi-automatic model checker for ESP) models value passing by suitably expanding all the data that influence the control part of the specification. The same expansion of data is performed both in the generated model and in the logic formulae. In this way symbolic formulae can be proved on a finite model of the ESP program, which provides the base for the analysis of the properties in the infinite ESP models.

ESP-MC: An Experiment in the Use of Verification Tools

INVERARDI, PAOLA;
1995-01-01

Abstract

We present an experiment of applying existing verification tools for process algebra, namely ACTL model checker and AUTO, to a system based on parallel logic programming: Extended Shared Prolog (ESP). The constructed tool ESP-MC (a semi-automatic model checker for ESP) models value passing by suitably expanding all the data that influence the control part of the specification. The same expansion of data is performed both in the generated model and in the logic formulae. In this way symbolic formulae can be proved on a finite model of the ESP program, which provides the base for the analysis of the properties in the infinite ESP models.
3-540-60688-2
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11697/40726
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
  • ???jsp.display-item.citation.isi??? ND
social impact