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

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

1 2 next

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

1 2 next