Istituto di Scienza e Tecnologie dell'Informazione     
Camilleri A., Inverardi P., Nesi M. Combining interaction and automation in process algebra verification. In: TAPSOFT '91 - International Joint Conference on Theory and Practice of Software Development. (Brighton, UK, 8 - 12 April 1991). Proceedings, pp. 283 - 296. S. Abramsky, T.S.E. Maibaum (eds.). (Lecture notes in computer science, vol. 494). Springer, 1991.
Most existing verification tools for process algebras allow the correctness of specifcations to be checked in a fully automatic fashion. These systems have the obvious advantage of being easy to use, but unfortunately they also have some drawbacks. In particular, they do not always succeed in completing the verification analysis, due to the problem of state explosion, and they do not provide any insight into the meaning of the intended specifications. In this paper we consider an alternative approach, in which both interactive and automatic techniques are combined in the hope that the advantages of automation are retained, and that some of its disadvantages are overcome. To achieve our goal, we use the interactive theorem prover HOL as a framework for supportiug the theory of observational congruence of CCS, and provide a set of automatic proof tools, based on the algebraic axiomatization of the language, which can be used interactive1y. To illustrate how interaction and automation can be intermixed, we describe two verification strategies which exhibit different degrees of user interaction.
Subject Process Algebra

Icona documento 1) Download Document PDF

Icona documento Open access Icona documento Restricted Icona documento Private


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional