You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
64 lines
2.5 KiB
64 lines
2.5 KiB
\documentclass{llncs} |
|
|
|
%\usepackage{graphicx} |
|
% |
|
\begin{document} |
|
|
|
|
|
\title{Formal Safety Verification of Temporal Model Properties via Model-Checking Mots clés Titre à trouver |
|
|
|
\author{Alexandre Albore, Silvano Dal Zillo, Guillaume Infantes, Christel Seguin, Pierre Virelizier} |
|
|
|
\institute{alexandre.albore@irt-saintexupery.com , IRT Saint Exupéry, |
|
118, route de Narbonne - CS 44248 |
|
31432 Toulouse cedex 4 (France) } |
|
\maketitle |
|
|
|
\begin{abstract} |
|
|
|
Abstract is here. |
|
|
|
\end{abstract} |
|
|
|
\section{Introduction}\label{sec:Introduction} |
|
|
|
Ce qu’on présente : méthode et chaine outillée pour la vérification formelle à travers model-checking de propriétés temporelles dans des modèles avec des retards dans la transmission des messages d’erreur. Par exemple, s’assurer de la fiabilité d’une fonction d’alarme quand des délais affectent les temps de la propagation des pannes. Traiter des modèles temporisés et en valider les propriétés temporelles de façon formelle est un enjeu fondamental dans le domaine de la safety. |
|
. : cf. PV |
|
Mo |
|
|
|
\section{Study case}\label{sec:Others} |
|
|
|
Élément de retard avec Dirac |
|
Propriétés qu’on veut vérifier (temporisation et délai sur les messages. Hypothèses sur les délais pour les pertes dans la chaîne précédente, c-à-d s’assurer de la fiabilité de la fonction d’alarme) ; on sait que si on a un retard différent sur les lignes, l’alarme n’est pas garanti, e.g. r1 + r2 <> r2 + r3. |
|
|
|
\section{Altarica and Fiacre} |
|
Tina / Fiacre et Petri temporisé et les propriétés que ça rajoute\\ |
|
Altarica vu à travers l’exemple\\ |
|
Traduction Altarica -> Fiacre |
|
|
|
\section{Empirical evaluation - Fiacre} |
|
Example sans délais (delta 0) : loss -> alarme et $F4_{loss}$\\ |
|
Example avec délais (delta N) : loss -> !alarme et $!F4_{loss}$\\ |
|
Example avec délais non-déterministe (pourrait identifier le temps minimum) |
|
|
|
\section{Conclusion}\label{sec:Conclusion} |
|
|
|
État de l’art (model-checking temporisé, model-checking temporisé paramétrique, …) |
|
Conclusion : plus-value (une suite outillée, fournir un cadre unifié d’outils) |
|
|
|
|
|
|
|
\section*{Acknowledgments}\label{sec:Acknowledgments} |
|
|
|
Authors would like to thank YYYYY. |
|
|
|
\begin{thebibliography}{1} |
|
|
|
\bibitem{Einstein} |
|
A. Einstein, On the movement of small particles suspended in stationary liquids required by the molecular-kinetic theory of heat, Annalen der Physik 17, pp. 549-560, 1905. |
|
|
|
\end{thebibliography} |
|
|
|
\end{document} |
|
|
|
|
|
|