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.Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
