CMC: A Tool for Compositional Model-Checking of Real-Time Systems. In this paper we present a tool (CMC) for compositional model-checking of real-time systems. CMC is based on a completely different method compared to existing real-time verification tools (HYTECH, KRONOS, UPPAAL). After a description of the method, we illustrate its efficiency by considering two examples: the Fischer’s mutual exclusion protocol and a railroad crossing system.

References in zbMATH (referenced in 28 articles )

Showing results 1 to 20 of 28.
Sorted by year (citations)

1 2 next

  1. Garavel, Hubert; Lang, Frédéric; Mateescu, Radu: Compositional verification of asynchronous concurrent systems using CADP (2015)
  2. Byg, Joakim; Jacobsen, Morten; Jacobsen, Lasse; Jørgensen, Kenneth Yrke; Møller, Mikael Harkjær; Srba, Jiří: TCTL-preserving translations from timed-arc Petri nets to networks of timed automata (2014)
  3. Lang, Frédéric; Mateescu, Radu: Partial model checking using networks of labelled transition systems and Boolean equation systems (2013)
  4. Timo, Omer Landry Nguena; Reynier, Pierre-Alain: On characteristic formulae for event-recording automata (2013)
  5. Waez, Md Tawhid Bin; Dingel, Juergen; Rudie, Karen: A survey of timed automata for the development of real-time systems (2013)
  6. Aceto, Luca; Birgisson, Arnar; Ingólfsdóttir, Anna; Mousavi, MohammadReza: Decompositional reasoning about the history of parallel processes (2012)
  7. Bouyer, Patricia; Cassez, Franck; Laroussinie, François: Timed modal logics for real-time systems. Specification, verification and control (2011)
  8. Larsen, Kim Guldstrand: Symbolic and compositional reachability for timed automata (2010)
  9. Boniol, Frédéric; Ermont, Jér^ome; Pagetti, Claire: Verification of real-time systems with preemption: negative and positive results (2009) ioport
  10. Srba, Jiří: Comparing the expressiveness of timed automata and timed extensions of Petri nets (2008)
  11. Cassez, Franck: Efficient on-the-fly algorithms for partially observable timed games (2007)
  12. Cassez, Franck; David, Alexandre; Larsen, Kim G.; Lime, Didier; Raskin, Jean-François: Timed control with observation based and stuttering invariant strategies (2007)
  13. Dierks, Henning; Kupferschmid, Sebastian; Larsen, Kim G.: Automatic abstraction refinement for timed automata (2007)
  14. Carcenac, Francois; Boniol, Frederic: A formal framework for verifying distributed embedded systems based on abstraction methods (2006) ioport
  15. Cassez, Franck; Chatain, Thomas; Jard, Claude: Symbolic unfoldings for networks of timed automata (2006)
  16. Bérard, Beatrice; Cassez, Franck; Haddad, Serge; Lime, Didier; Roux, Olivier H.: Comparison of the expressiveness of timed automata and time Petri nets (2005)
  17. Cassez, Franck; Roux, Olivier H.: Structural translation from time Petri nets to timed automata (2005)
  18. Srba, Jiří: Timed-arc Petri nets vs. networks of timed automata (2005)
  19. Bouyer, Patricia; Dufourd, Catherine; Fleury, Emmanuel; Petit, Antoine: Updatable timed automata (2004)
  20. Aceto, Luca; Bouyer, Patricia; Burgueño, Augusto; Larsen, Kim G.: The power of reachability testing for timed automata (2003)

1 2 next