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

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

1 2 next

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

1 2 next