HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

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
Complete list of metadata

Cited literature [18 references]  Display  Hide  Download

Contributor : Eunyoung Kang Connect in order to contact the contributor
Submitted on : Thursday, November 10, 2005 - 2:37:34 PM
Last modification on : Friday, February 4, 2022 - 3:30:16 AM
Long-term archiving on: : Friday, April 2, 2010 - 5:45:20 PM


  • HAL Id : inria-00000641, version 1



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⟩



Record views


Files downloads