This page shows all publications that appeared in the IASI annual research reports. Authors currently affiliated with the Institute are always listed with the full name.

You can browse through them using either the links of the following line or those associated with author names.

Show all publications of the year  ALL, with author Fioravanti F., in the category IASI Research Reports (or show them all):

---

IASI Research Report n. 11-23  (Previous    Next) 


Fioravanti F., Maurizio Proietti, Alberto Pettorossi, Senni V.

A Constraint-Based Transformation for Verifying Infinite State Systems

ABSTRACT

We address the problem of verifying safety properties of infinite state reactive systems that use unbounded integer variables. We consider systems specified by using linear constraints over the integers and we assume that, for verifying safety properties of these systems, one uses reachability analysis techniques. Our method improves the effectiveness of forward and backward reachability analyses by preprocessing the system specification. For forward reachability our method consists in: (i) transforming the system specification into an equivalent one (with respect to the safety property of interest) by a constraint propagation technique that works backward from the constraints representing the unsafe states, and then (ii) applying to the transformed system a reachability analysis that works forward from the constraints representing the initial states. For backward reachability our method works as for forward reachability, by interchanging the roles of the initial states and the unsafe states. We have implemented our method by using the MAP program transformation tool. Our implementation works as a preprocessor for infinite state systems specified in FASTer, a powerful tool for verifying safety properties of infinite state systems with integer variables. Through various experiments performed on several infinite state systems, we have shown that our constraint-based transformation of the system specifications considerably increases the number of successful verifica- tions without a significant degradation of the time performance.