Georges Morbé, Dr.
Fakultät für angewandte Wissenschaften
Albert-Ludwigs-Universität
Georges Köhler Allee, Gebäude 51
79110 Freiburg im Breisgau
Deutschland
Gebäude 51, Raum 02..032
+49 761 203 8149
morbe@informatik.uni-freiburg.de

Liste filtern : Jahre: 2015 |

2014 |

2013 |

2012 |

2011 | alle anzeigen nach oben zur Jahresübersicht Georges Morbé, Christoph SchollFully 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. nach oben zur Jahresübersicht Georges Morbé, Christian Miller, Christoph Scholl, Bernd BeckerCombined 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 SchollFully Symbolic TCTL Model Checking for Complete and Incomplete Real-Time Systems 2014 AVACS Technical Report, Nummer 104 » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung In this paper we introduce a new formal model, called finite state machines with time (FSMT), to represent real-time systems. We present a model checking algorithm for FSMTs, which works on fully symbolic state sets containing both the clock values and the state variables. Besides complete networks of FSMTs our algorithm can verify incomplete real-time systems in form of incomplete FSMTs, and is able to prove that a TCTL property is violated or satisfied regardless of the implementation of unknown components in the system. For that purpose the algorithm
computes over-approximations of sets of states fulfilling a TCTL property Φ for at least one implementation of the unknown components and under-approximations of sets of states fulfilling Φ for all possible implementations of the unknown components. In order to verify timed automata with our model checking algorithm, we present two different methods to convert timed automata to FSMTs. In addition to pure interleaving semantics we can convert timed automata to FSMTs having a parallelized interleaving behaviour which allows parallelism of transitions causing no conflicts. This can dramatically reduce the number of steps during verification. In our experimental results on complete systems our prototype implementation outperforms the state-of-the-art model checkers UPPAAL and RED, and on incomplete systems our tool is able to prove interesting properties at early stages of the design when parts of the overall system
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. nach oben zur Jahresübersicht Georges Morbé, Christoph SchollFully Symbolic Model Checking for Incomplete Systems of Timed Automata 2013 Electronic Communications of the EASST, Proceedings of AVOCS 2013 , Band : 66 nach oben zur Jahresübersicht nach oben zur Jahresübersicht Georges Morbé, Florian Pigorsch, Christoph SchollFully Symbolic Model Checking for Timed Automata 2011 CAV , Springer, Band : 6806, Seiten : 616 - 632 Georges Morbé, Christoph SchollFully Symbolic Model Checking for Timed Automata 2011 MBMV , Seiten : 9 - 18