• xmlui.mirage2.page-structure.header.title
    • français
    • English
  • Help
  • Login
  • Language 
    • Français
    • English
View Item 
  •   BIRD Home
  • LAMSADE (UMR CNRS 7243)
  • LAMSADE : Publications
  • View Item
  •   BIRD Home
  • LAMSADE (UMR CNRS 7243)
  • LAMSADE : Publications
  • View Item
JavaScript is disabled for your browser. Some features of this site may not work without it.

Browse

BIRDResearch centres & CollectionsBy Issue DateAuthorsTitlesTypeThis CollectionBy Issue DateAuthorsTitlesType

My Account

LoginRegister

Statistics

Most Popular ItemsStatistics by CountryMost Popular Authors
Thumbnail - Request a copy

Design and Evaluation of a Symbolic and Abstraction-Based Model Checker

Haddad, Serge; Ilié, Jean-Michel; Klai, Kais (2004), Design and Evaluation of a Symbolic and Abstraction-Based Model Checker, in Wang, Farn, Automated Technology for Verification and Analysis Second International Conference, ATVA 2004, Taipei, Taiwan, ROC, October 31 - November 3, 2004. Proceedings, Springer : Berlin, p. 196-210. http://dx.doi.org/10.1007/978-3-540-30476-0_19

Type
Communication / Conférence
Date
2004
Conference title
2nd International Symposium on Automated Technology for Verification and Analysis, ATVA 2004
Conference date
2004-10
Conference city
Taipei
Conference country
Taïwan
Book title
Automated Technology for Verification and Analysis Second International Conference, ATVA 2004, Taipei, Taiwan, ROC, October 31 - November 3, 2004. Proceedings
Book author
Wang, Farn
Publisher
Springer
Series title
Lecture Notes in Computer Science
Series number
3299
Published in
Berlin
ISBN
978-3-540-23610-8
Number of pages
506
Pages
196-210
Publication identifier
http://dx.doi.org/10.1007/978-3-540-30476-0_19
Metadata
Show full item record
Author(s)
Haddad, Serge
Ilié, Jean-Michel
Klai, Kais
Abstract (EN)
Symbolic model-checking usually includes two steps: the building of a compact representation of a state graph and the evaluation of the properties of the system upon this data structure. In case of properties expressed with a linear time logic, it appears that the second step is often more time consuming than the first one. In this work, we present a mixed solution which builds an observation graph represented in a non symbolic way but where the nodes are essentially symbolic set of states. Due to the small number of events to be observed in a typical formula, this graph has a very moderate size and thus the complexity time of verification is neglectible w.r.t. the time to build the observation graph. Thus we propose different symbolic implementations for the construction of the nodes of this graph. The evaluations we have done on standard examples show that our method outperforms the pure symbolic methods which makes it attractive.
Subjects / Keywords
OBDD; Model Checking; Abstraction

Related items

Showing items related by title and author.

  • Thumbnail
    Modular Verification of Petri nets properties: a Structure-based Approach 
    Klai, Kais; Haddad, Serge; Ilié, Jean-Michel (2005) Communication / Conférence
  • Thumbnail
    An Incremental Verification Technique using Decomposition of Petri Nets 
    Klai, Kais; Haddad, Serge; Ilié, Jean-Michel (2002) Communication / Conférence
  • Thumbnail
    Symbolic Reachability Graph and Partial Symmetries 
    Haddad, Serge; Ilié, Jean-Michel; Taghelit, Mohamed; Zouari, Belhassen (1995) Communication / Conférence
  • Thumbnail
    Exploiting Partial Symmetries in Well-formed nets for the Reachability and the Linear Time Model Checking Problems 
    Baarir, Souheib; Haddad, Serge; Ilié, Jean-Michel (2005) Communication / Conférence
  • Thumbnail
    A Model Checking Method for Partially Symmetric Systems 
    Haddad, Serge; Ilié, Jean-Michel; Ajami, Khalil (2000) Communication / Conférence
Dauphine PSL Bibliothèque logo
Place du Maréchal de Lattre de Tassigny 75775 Paris Cedex 16
Phone: 01 44 05 40 94
Contact
Dauphine PSL logoEQUIS logoCreative Commons logo