Jeudi 22 Janvier
Heure: 
16:00  17:00 
Lieu: 
Salle B107, bâtiment B, Université de Villetaneuse 
Résumé: 
Specification and verification of Time Petri Nets with Coq 
Description: 
Amal Chamakh Model checking and theorem proving, have long reached their limitation as generalpurpose techniques, and most of the research now is concentrated on efficient specialization of both approaches to relatively narrow problem domains. The state space explosion problem leaves little hope for automatic finitestate verification techniques like model checking to remain practical, especially when designs become parameterized. The use of theorem proving techniques is inevitable to cope with the new verification challenges. "Pure" theorem proving, on the other hand, can also be quite tedious and impractical for complex designs. Ideally, one would like to find an efficient combination of model checking and theorem proving, and the quest for such a combination has long been one of the major challenges in the field of formal verification. In this paper, we address the combination of model checking and theorem proving approaches in order to specify and to model check Time Petri Nets (TPN) modelbased systems. In particular, we show how a TPN is specified using the Coq proof assistant, and how the fireability/unfireability of a timed sequence of transitions can be proved. This allows, for instance, to prove the reachability of a given state by the firing of a given timed/untimed trace or to prove that a counterexample supplied by a given (untimed) model checker is a real counterexample of a timed system. %First, we provide a formalization of the net model in COQ via the parsing of its Petri Net Markup Language (PNML) description. Then the COQ proof assistant is used to prove the firability (or the opposite) of traces given by model checking as a counterexample when a propriety being checked is found to be nonvalid, hence, states reachability is proved. 

