Skip to Main content Skip to Navigation

Abstractions booléennes pour la vérification des systèmes temps-réel

Abstract : This thesis provides an efficient formal scheme for the tool-supported real-time system verification by combination of abstraction-based deductive and model checking techniques in order to handle the limitations of the applied verification techniques. This method is based on IAR (Iterative Abstract Refinement) to compute finite state abstractions. Given a transition system and a finite set of predicates, this method determines a finite abstraction, where each state of the abstract state space is a true assignment to the abstraction predicates. A theorem prover can be used to verify that the finite abstract model is a correct abstraction of a given system by checking conformance between an abstract and a concrete model by establishing/proving that a set of verification conditions are obtained during the IAR procedure. Then the safety/liveness properties are checked over the abstract model. If the verification condition holds successfully, IAR terminates its procedure. Otherwise more analysis is applied to identify if the abstract model needs to be more precise by adding extra predicates. As abstraction form, we adopt a class of predicate diagrams and define a variant of predicate diagram PDT (Predicate Diagram for Timed systems) that can be used to verify real-time and parameterized systems.
Document type :
Complete list of metadata

Cited literature [81 references]  Display  Hide  Download
Contributor : Thèses UL Connect in order to contact the contributor
Submitted on : Thursday, March 29, 2018 - 11:29:50 AM
Last modification on : Saturday, October 16, 2021 - 11:26:08 AM
Long-term archiving on: : Friday, September 14, 2018 - 7:43:56 AM


Files produced by the author(s)


  • HAL Id : tel-01748252, version 1



Eun-Young Kang. Abstractions booléennes pour la vérification des systèmes temps-réel. Autre [cs.OH]. Université Henri Poincaré - Nancy 1, 2007. Français. ⟨NNT : 2007NAN10089⟩. ⟨tel-01748252⟩



Record views


Files downloads