Boreale M., Ferro G., Ristori G. A model checking tool for the-calculus based on automata. Internal note IEI-B4-52, 1995. |

Abstract (English) |
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 |

1) Download Document PDF |

Open access Restricted Private