|
|
 |
|
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
general-purpose 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
finite-state 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) model-based 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
counter-example 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 counter-example
when a propriety being checked is found to be non-valid, hence, states
reachability is proved. |
|
|
