Real-Time system verification techniques based on abstraction/deduction and model checking

Eunyoung Kang 1
1 MOSEL - Proof-oriented development of computer-based systems
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Our research focuses on verification techniques for real-time systems based on predicate abstractions. These techniques aim to combine abstract interpretation, model checking, and theorem proving in order to obtain a powerful and highly automatic verification environment for real-time systems. One drawback of current real-time model checking approaches is the limited size of the systems that can be analyzed. For the computation of finite abstractions in the way of infinite-state systems analysis, we propose an Iterative-Abstract-Refinement algorithm. Using our algorithm, we can reduce the aforementioned drawbacks associated with the application of real-time model checking such as the limited applicability due to state space explosion characteristics
Document type :
Conference papers
Liste complète des métadonnées

Cited literature [18 references]  Display  Hide  Download

https://hal.inria.fr/inria-00000641
Contributor : Eunyoung Kang <>
Submitted on : Thursday, November 10, 2005 - 2:37:34 PM
Last modification on : Thursday, January 11, 2018 - 6:19:52 AM
Document(s) archivé(s) le : Friday, April 2, 2010 - 5:45:20 PM

Identifiers

  • HAL Id : inria-00000641, version 1

Collections

Citation

Eunyoung Kang. Real-Time system verification techniques based on abstraction/deduction and model checking. Doctoral Symposium of the Fifth International Conference on Integrated Formal Methods - IFM'2005, Judi Romijn, Nov 2005, Eindhoven/The Netherlands. ⟨inria-00000641⟩

Share

Metrics

Record views

212

Files downloads

191