Istituto di Scienza e Tecnologie dell'Informazione     
Boreale M., Ferro G., Ristori G. A model checking tool for the-calculus based on automata. Internal note IEI-B4-52, 1995.
We consider an extension to the if-calculus of the Hennessy-Milner Logic. Relying on a finite representation of the if-calculus operational semantics (if-automat,a), we propose for this logic a model checking method by which, contrary to previous decision strategies, properties are staticaliy checked on operat.ional models explicitly built. from if-calculus t.erms. The complexity of the method is linear in Ip!''';I, where IPI and I~I denote, respect.ively, the syntactical sizes of the process and of the formula to be verified. We also prove that the problem of checking whether a if-calculus process P satisfies a formula r/> is NP-hard, even in the simple case when P does not contain restriction, parallel composit.ion and matching operat.ors. We also describe a verification tool, PMC, based on the method we have developped, and we present an example of verification with it..
Subject Model checking
D.2.4 Software/Program Verification. Formal methods

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