CMC

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 31 articles )

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

1 2 next