laboratoire IBISC, bat. IBGBI, 23 bd de France, Evry, amphi du rez-de-chaussée: comment y aller
Il est possible de garer sa voiture dans le parking souterrain en appelant la loge à partir de la borne d'entrée
Abstract : We discuss important characteristics of finite generating sets for F, the set of all semiflows with integer coordinates of a Petri Net, then particularly, for F+ the set of semiflows with non-negative coordinates. We endeavor to regroup a number of algebraic results dispersed throughout the Petri Nets literature and also to better position the results while considering semirings such as N or Q+ then fields such as Q. As accurately as possible, we provide a range of new algebraic results on minimal semiflows, minimal supports, and finite minimal generating sets for a given family of semiflows. Minimality of semiflows and of support are critical to develop effective analysis of invariants and behavioral properties of Petri Nets such as boundedness or liveness. We succinctly present a methodology to analyze a Petri Nets by refinement of home spaces directly deduced from semiflows. We conclude with the analysis of an example drawn from the telecommunication industry underlining the efficiency brought by using minimal semiflows of minimal supports. Keywords: Formal verification, Petri Nets, invariant, home spaces, linear algebra, semiflow, generating set
Abstract : Among harmful information leaks, the timing information leakage is the ability for an attacker to deduce internal information depending on timing information. In this presentation, I focus on timing leakage through the total execution time, i. e., when a system works as an almost black-box and the ability of the attacker is limited to know the model and observe the total execution time. I will present the formalization we introduced with timed automata and how we can verify security properties in timed systems.