Jump to : Download | Abstract | Contact | BibTex reference | EndNote reference |
Download paper Gziped Postscript (.ps.gz)
Copyright noticeThis material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.
This works deals with the verification by algorithmic methods of safety properties of synchronous systems, or more generally reactive systems, that exhibit both Boolean and numerical aspects. It proposes an original technique that allows the size of verified systems to be noticeably augmented. We first recall the theoretical framework we use, which is the abstract interpretation theory, and one of its applications, the linear relation analysis, that discovers linear relations linking numerical variables of a program in each of its control points. This analysis was applied to the verification of numerical synchronous programs and linear hybrid systems. In this context, two problems arise: the first one is that the explicit control structure of these systems is often of prohibitive size, and the second one is that the analysis is not precise enough for the proof of some properties. These two problems are in fact related, and we propose a solution to obtain a suitable tradeoff between complexity and precision. We use an abstract domain combining Boolean and numerical properties, and we exploit a control structure to adjust the precision of the analysis. The analysis uses the property to be proved in order to automatically refine an initial rough control structure, until the obtained precision enables the proof of the property. A verification tool based on these principles was implemented and experimented on several and significative examples, some of which being unaffordable with other automatic verification techniques.
Bertrand Jeannet
Bertrand.Jeannet@irisa.fr
@PhdThesis{jeannet00b,
Author = {Jeannet, B.},
Title = {partitionnement Dynamique dans l'Analyse de Relations Linéraires et Application à la Vérification de Programmes Synchrones},
School = {Institut National Polytechnique de Grenoble},
Month = {September},
Year = {2000}
}
Get EndNote Reference (.ref)