2015

 nach oben zur Jahresübersicht

• Georges Morbé, Christoph Scholl
  Fully symbolic TCTL model checking for complete and incomplete real-time systems
  2015 Science of Computer Programming
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  In this paper we present a fully symbolic TCTL model checking algorithm for real-time systems represented in a formal model called finite state machine with time (FSMT), which works on fully symbolic state sets containing both the clock values and the state variables. Our algorithm is able to verify TCTL properties on complete and incomplete FSMTs containing unknown components. For that purpose over-approximations of state sets fulfilling a TCTL property φ for at least one implementation of the unknown components and under-approximations of state sets fulfilling φ for all possible implementations of the unknown components are computed. We present two different methods to convert timed automata to FSMTs. In addition to FSMTs simulating pure interleaving behaviour of timed automata we can produce FSMTs with a parallelized interleaving behaviour which allows parallelism of conflict-free transitions. This can dramatically reduce the number of steps during verification. Our prototype implementation outperforms the state-of-the-art model checkers UPPAAL and RED on complete systems, and on incomplete systems our tool is able to prove interesting properties when parts of the system are unknown.

2014

 nach oben zur Jahresübersicht

• Georges Morbé, Christian Miller, Christoph Scholl, Bernd Becker
  Combined Bounded and Symbolic Model Checking for Incomplete Timed Systems
  2014 Haifa Haifa Verification Conference (HVC), Yahav, Eran, Band: 8855, Seiten: 30 - 47
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  We present a hybrid model checking algorithm for incomplete timed systems where parts of the system are unspecified (so-called black boxes). Here, we answer the question of unrealisability, i.e., “Is there a path violating a safety property regardless of the implementation of the black boxes?” Existing bounded model checking (BMC) approaches for incomplete timed systems exploit the power of modern SMT solvers, but might be too coarse as an abstraction for certain problem instances. On the other hand, symbolic model checking (SMC) for incomplete timed systems is more accurate, but may fail due to the size of the explored state space. In this work, we propose a tight integration of a backward SMC routine with a forward BMC procedure leveraging the strengths of both worlds. The symbolic model checker is hereby used to compute an enlarged target which we then try to hit using BMC. We use learning strategies to guide the SMT solver’s search into the right direction and manipulate the enlarged target to improve the overall accuracy of the current verification run. Our experimental results show that the hybrid approach is able to verify incomplete timed systems which are out of the scope for BMC and can neither be solved in reasonable time using SMC. Furthermore, our approach compares favourably with UPPAAL-TIGA when considering timed games as a special case of the unrealisability problem.
• Georges Morbé, Christoph Scholl
  Fully Symbolic TCTL Model Checking for Complete and Incomplete Real-Time Systems
  2014 AVACS Technical Report, Nummer 104
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  may not yet be finished. Additionally, fading out components of a large system may dramatically reduce the complexity of the system and thus the effort for verification.

2013

 nach oben zur Jahresübersicht

• Georges Morbé, Christoph Scholl
  Fully Symbolic Model Checking for Incomplete Systems of Timed Automata
  2013 Electronic Communications of the EASST, Proceedings of AVOCS 2013, Band: 66

2012

 nach oben zur Jahresübersicht

• Georges Morbé, Christoph Scholl
  Fully Symbolic Model Checking for Incomplete Systems of Timed Automata
  2012 MBMV, Seiten: 97 - 108
• Georges Morbé, Christoph Scholl
  Guaranteeing Termination of Fully Symbolic Timed Forward Model Checking
  2012 MTV, IEEE Computer Society, Seiten: 35 - 40

2011

 nach oben zur Jahresübersicht

• Georges Morbé, Florian Pigorsch, Christoph Scholl
  Fully Symbolic Model Checking for Timed Automata
  2011 CAV, Springer, Band: 6806, Seiten: 616 - 632
• Georges Morbé, Christoph Scholl
  Fully Symbolic Model Checking for Timed Automata
  2011 MBMV, Seiten: 9 - 18