Automates à file réactifs embarqués - Application à la vérification de systèmes temps-réels

Abstract:

We are concern in our thesis by the verification of ELECTRE programs and Embedded Reactive Fiffo Systems (Embedded RFS). These two formalisms allow to model asynchronous reactive systems with event memorization, along with their environment. Particularly, we focus on the boundedness problem which is seen as a correctness criterion for reactive systems. We prove that this problem is undeciable, thus we provide a testing method as a partial solution. We also prove that the reachability problem is decidable for Lossy Embedded RFS, a usual extension of models. This positive result allows to model-check safety properties on Lossy Embedded RFS, and, when they are satisfied, to deduce their satisfaction of the corresponding Embedded RFS. Then, we introduce Linear Hybrid RFS for the modelling of Real-time systems, an quantitative-timed extension of RFS. The boundedness problem is undecidable again, thus we adapt our testing method is this new context. Finally, even when an Embedded RFS is bounded, model-checking is untractable since the RFS is too big. We provide a reduction method for Embedded RFS which amazingly reduce the memorizing queue (when it applies) while preserving most of the verification results.

Keywords:

ELECTRE, Embedded Reactive Fiffo Systems, Model-checking, Boundedness, Infinite systems, Test.

Download: (the manuscript is written in French)

[ps.gz | pdf] (Last modification: feb 4th, 2003)

BibTeX entry:

@Phdthesis{Her:PHD01, title = "Automates {\`a} file r{\'e}actifs embarqu{\'e}s - Application {\`a} la v{\`e}rification de syst{\`e}mes temps-r{\'e}el", author = "Herbreteau, F.", year = "2001", school = "{\'E}cole Centrale de Nantes and Universit{\'e} de Nantes", note = "In french", }