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.
File in questo prodotto:
Non ci sono file associati a questo prodotto.