# HG changeset patch # User Eugen Sawin # Date 1311302039 -7200 # Node ID 46709047b260365493d0894c0ca0a6975c0eb2cd # Parent c03845978e24347d23d230e263f62cb70f080537 Notes. diff -r c03845978e24 -r 46709047b260 slides/images/airbag.jpg Binary file slides/images/airbag.jpg has changed diff -r c03845978e24 -r 46709047b260 slides/images/atc.jpg Binary file slides/images/atc.jpg has changed diff -r c03845978e24 -r 46709047b260 slides/images/intel.jpg Binary file slides/images/intel.jpg has changed diff -r c03845978e24 -r 46709047b260 slides/notes.txt --- a/slides/notes.txt Fri Jul 22 01:22:59 2011 +0200 +++ b/slides/notes.txt Fri Jul 22 04:33:59 2011 +0200 @@ -1,2 +1,117 @@ 1. Guten Morgen! Mein Name ist Eugen Sawin und ich werde jetzt den einführenden Vortrag halten zum Seminar Automatenkonstruktionen im Model Checking. +2. Was ich ihnen erzählen werde, wird die Meisten von euch bei der Bearbeitung des Themas in irgendeiner Form tangiert haben. + +3. Meine Präsentation soll einen Überblick geben über die algorithmische Verifikation reaktiver Systeme basierend auf dem automaten-theoretischen Ansatz des Model Checkings. + +==> 2 + +4. PHI ist erfüllt in Modell M, oder Modell M modelliert PHI. +Das ist der Kern unserer Bemühungen. +Doch was bedeutet das? +Wir übersetzen das in die Problemstellung der Verifikation von Systemen. + +==> 3 + +5. Gegeben sei ein Programm und dessen Spezifikation, das Problem lautet: +erfüllt jeder Durchlauf des Programms die Spezifikation? + +Bevor wir an die Tat schreiten um das Problem zu lösen, +möchte ich eine andere Frage beantworten. + +Wieso das Ganze? Was ist der praktische Nutzen der Verifikation? + +==> 4 + +Hard- und Softwaresysteme haben alle Bereiche der Industrie und damit auch unseren Alltag durchdrungen. +Sie bilden die Infrastruktur unserer Kommunikation, bieten Sicherheit und retten sogar Leben. +Und sie werden immer komplexer. +Die Industrie investiert viel Zeit und Geld in die Verifikation sicherheitskritischer Systeme und der Kernkomponenten anderer Systeme. +Die automatisierte Verifikation hat bereits in der Chip-Verifikation ihre praktische Anwendbarkeit gezeigt und ist in der Softwareindustrie stark gefragt. + +Also fangen wir an. + +==> 5 + +Wenn ich sage: "Es ist dunkel." ist es nicht eindeutig, was ich damit ausdrücken möchte. + +Ich könnte damit meinen "Es ist immer dunkel.", doch das spricht gegen unsere Intuition. +Wir denken als Erstes eher an "Es ist im Moment dunkel.", was auch stimmt, wenn ich damit die Folien referenziere (oder das Wetter draußen). + +Wenn wir nach draußen schauen, können wir aus Erfahrung behaupten, dass es "notwendigerweise irgendwann dunkel wird." + +Unsere Sprache erlaubt es uns auch kausale Zusammenhänge zu bilden, wie z.B. "Es ist dunkel, bis Jemand das Licht an macht." + +Wir sehen, dass die natürliche Sprache nicht eindeutig ist und somit zur formalen Beschreibung ungeeignet. +Wie können wir unsere Sprache zähmen, ohne die Ausdruckskraft zu verlieren. +Nun, als Ersten machen wir das Licht wieder an! + +==> 6 + +Nehmen wir den letzten Satz in einer allgemeineren Form als Beispiel. +Dieser Satz sollte allgemeingültig sein. +Wie können wir die Aussage dieses Satzes formal festhalten? +Wir bedienen uns der Aussagenlogik und erweitern diese um eine weitere Verknüpfung. + +==> 6(2) + +Dabei sind p0 und p1 Elementaraussagen, sog. Atome, die entsprechend für "Es is dunkel" und "Es gibt licht" stehen. +Die neue Verknüpfung nennen wir trivialerweise "until" und notieren sie mit dem kalligraphischen U. +Halten wir das formal fest. + +==> 7 + +Wir definieren die Syntax der linearen temporalen Logik mit Hilfe dieser Produktionen in Backus-Naur-Form. +Somit ist eine LTL-Formel entweder ein aussagenlogisches Atom, eine negierte Formel oder eine Disjunktion zweier Formeln. +Das kannten wir bereits aus der Aussagenlogik. +Die Erweiterung sind das kalligraphische X, welches für "Next" steht und das "Until" aus dem Beispiel. +Diese Syntaxdefinition bildet das Fundament für weitere abgeleitete Verknüpfungen. + +==> 8 + +Wir interpretieren LTL-Formeln über unendliche Sequenzen von Aussagen. +Die Sequenz entspricht der zeitlichen Abfolge von Ereignissen in einem vorwärts gerichteteten diskreten Zeitverlauf. +Diese Interpretation heißt die Kripke-Semantik. +Das Kripke-Modell der LTL-Semantik besteht aus einer abzählbaren Menge von Zuständen, verknüpft duch die Erreichbarkeitsrelation und der Bewertungsfunktion V. +Da wir nur lineare Abfolgen betrachten, fällt die Erreichbarkeitsrelation einfach aus. +Von einem beliebigen Zustand ist jeweils nur dessen Nachfolger erreichbar. +Die Bewertungsfunktion liefert uns die Menge aller gültigen Atome für einen bestimmten Zustand. +Intuitiv sagt man, ein Atom p ist wahr zum Zeitpunkt i gdw. p in der Menge V(i) ist. + +==> 9 + +Hier ist eine Veranschaulichung eines Beispielmodells. +Man sieht die Zustände s0 bis si und den Zeitverlauf durch die Relation R. +Für jeden Zustand ist die Rückgabe der Bewertungsfunktion als Menge positiver Atome abgebildet. + +==> 10 + +Die Erfüllbarkeit einer Formel zu einem Zeitpunkt i im Modell M ist folgendermaßen definiert: +- ein Atom p ist erfüllbar gdw. und p in der Menge V(i) ist +- eine negierte Formel PHI ist erfüllbar gdw. PHI nicht erfüllbar ist +- eine Disjunktion von PHI und PSI ist erfüllbar gdw. PHI oder PSI erfüllbar ist +- Next PHI ist erfüllbar gdw. PHI im darauffolgenden Zeitpunkt erfüllbar ist +- PHI Until PSI ist erfüllbar gdw. es einen Zeitpunkt k gibt, ab dem PSI erfüllbar ist und für alle Zeitpunkte vor k PHI erfüllbar ist. + +Mit Hilfe der linearen temporalen Logik lassen sich Programmeigenschaften und derren zeitliche Abhängigkeiten genau beschreiben. +Als nächstes werden wir uns den Automaten widmen, die auf unendlichen Eingaben operieren. + +==> 11 + +Wieso sind unsere Eingaben überhaupt unendlich? +Im Gegensatz zu terminierenden Programmen sind reaktive Systeme fortlaufende Prozesse. +Ein mal initiiert, verbleiben reaktive Systeme in einem aktiven Zustand und reagieren auf nebenläufige Eingaben. +Theoretisch betrachtet, arbeiten solche Systeme somit auf unendlichen Eingabesequenzen. + +==> 12 + +Hier ist ein Beispielautomat, der auf unendlichem Input arbeitet. +Sieht jemand auf Anhieb welche Sprache dieser Automate akzeptiert? +w1 ist eine Eingabe, der Überstrich soll eine periodische Wiederholung der Sequenz darstellen. +.... + + + + + + diff -r c03845978e24 -r 46709047b260 slides/src/slides.tex --- a/slides/src/slides.tex Fri Jul 22 01:22:59 2011 +0200 +++ b/slides/src/slides.tex Fri Jul 22 04:33:59 2011 +0200 @@ -89,25 +89,138 @@ \begin{frame} \frametitle{Motivation} -\framesubtitle{Model Checking} +\framesubtitle{Model Checking 1/2} \begin{center} %\only<1>{\colorbox{black}{\makebox(35,10){\color{white} $\M \models \varphi$}}} -\only<1>{\[\M \models \varphi\]} -\only<2->{Given a program $P$ and specification $\varphi$:\\ -\colorbox{black}{\makebox(150,10){\color{white} does every run of $P$ satisfy $\varphi$?}}} +\[\M \models \varphi\] \end{center} \end{frame} \begin{frame} \frametitle{Motivation} +\framesubtitle{Model Checking 2/2} +\begin{center} +Given a program $P$ and specification $\varphi$:\\ +\colorbox{black}{\makebox(150,10){\color{white} does every run of $P$ satisfy $\varphi$?}} +\end{center} +\end{frame} + +\begin{frame} +\frametitle{Motivation} +\framesubtitle{Industry} \begin{figure} \centering -\subfigure{\includegraphics[width=100pt,height=70pt]{images/intel.jpg}} -\subfigure{\includegraphics[width=100pt,height=70pt]{images/airbag.jpg}} -\subfigure{\includegraphics[width=100pt,height=70pt]{images/atc.jpg}} +\subfigure{\includegraphics[width=70pt,height=50pt]{images/intel.jpg}} +\subfigure{\includegraphics[width=70pt,height=50pt]{images/airbag.jpg}} +\subfigure{\includegraphics[width=70pt,height=50pt]{images/atc.jpg}} \end{figure} \end{frame} +{ +\setbeamercolor{normal text}{bg=black, fg=white} +\setbeamercolor{frametitle}{fg=white!30!black} +\usebeamercolor*{normal text} +\usebeamercolor*{frametitle} +\begin{frame} +\frametitle{Linear Temporal Logic} +\framesubtitle{Motivation 1/2} +\begin{center} +``It is dark.''\\ +\visible<2->{``It is \emph{always} dark.''\\} +\visible<3->{``It is \emph{currently} dark.''\\} +\visible<4->{``It will \emph{eventually} be dark.''\\} +\visible<5->{``It is dark \emph{until} someone puts the light on.''} +\end{center} +\end{frame} +} + +\begin{frame} +\frametitle{Linear Temporal Logic} +\framesubtitle{Motivation 2/2} +\begin{center} +\only<1->{ +\color{white} +\colorbox{black}{\makebox(50,10){It is dark}} \colorbox{orange}{\makebox(30,10){until}} \colorbox{black!30}{\makebox(50,10){there is light}}\\ +\visible<2->{ +\colorbox{black}{\makebox(50,10){$p_0$}} \colorbox{orange}{\makebox(30,10){$\U$}} \colorbox{black!30}{\makebox(50,10){$p_1$}}} +} +\end{center} +\end{frame} + +\begin{frame} +\frametitle{Linear Temporal Logic} +\framesubtitle{Syntax} +\begin{def:syntax} +Let $\Prop$ be the countable set of \emph{atomic propositions}, LTL-formulae $\varphi$ are defined using following productions: +\[\varphi ::= p \in \Prop \,|\, \neg \varphi \,|\, \varphi \lor \varphi \,|\, \X \varphi \,|\, \varphi \U \varphi\] +\begin{itemize} +\item $\neg, \lor$ corresponds to the Boolean \emph{negation} and \emph{disjunction}. +\item $\X$ reads \emph{next}. +\item $\U$ reads \emph{until}. +\end{itemize} +\end{def:syntax} +\end{frame} + +\begin{frame} +\frametitle{Linear Temporal Logic} +\framesubtitle{Semantics} +\begin{def:frames} +An LTL-\emph{frame} is a tuple $\F = (S, R)$: +\begin{itemize} +\item $S = \{s_i \mid i \in \N\}$ is the set of states. +\item $R = \{(s_i, s_{i+1}) \mid i \in \N\}$ is the accessibility relation. +\end{itemize} +\end{def:frames} + +\begin{def:models} +An LTL-\emph{model} is a tuple $\M = (\F, V)$: +\begin{itemize} +\item $\F$ is a \emph{frame}. +\item $V: S \to 2^\Prop$ is a \emph{valuation function}. +\item Intuitively we say $p \in \Prop$ is \emph{true} at time instant $i$ iff $p \in V(i)$. +\end{itemize} +\end{def:models} +\end{frame} + +\begin{frame} +\frametitle{Linear Temporal Logic} +\framesubtitle{Model Example} +\begin{figure} +\centering +\begin{tikzpicture}[shorten >=1pt, node distance=2.5cm, auto, semithick, >=stealth + ,accepting/.style={fill, gray!50!black, text=white}] +\node[state, initial, initial text=] (s_0) {$\{p_0\}$}; +\path (s_0) [late options={label=below:$s_0$}]; +\node[state] (s_1) [right of= s_0] {$\{p_0, p_2\}$}; +\path (s_1) [late options={label=below:$s_1$}]; +\node[state] (s_2) [right of= s_1] {$\{p_1\}$}; +\path (s_2) [late options={label=below:$s_2$}]; +\node[state] (s_i) [right of= s_2] {$\{p_1\}$}; +\path (s_i) [late options={label=below:$s_i$}]; +\path[->] +(s_0) edge node {$R$} (s_1) +(s_1) edge node {$R$} (s_2); +\path[dashed,->] +(s_2) edge node {$R$} (s_i); +\end{tikzpicture} +\end{figure} +\end{frame} + +\begin{frame} +\frametitle{Linear Temporal Logic} +\framesubtitle{Satisfiability} +\begin{def:satisfiability} +A model $\M = (\F, V)$ \emph{satisfies} a formula $\varphi$ at time instant $i$ is denoted by $\M,i \models \varphi$: +\begin{itemize} +\item $\M,i \models p$ for $p \in \Prop \iff p \in V(i)$ +\item $\M,i \models \neg \varphi \iff$ not $\M,i \models \varphi$ +\item $\M,i \models \varphi \lor \psi \iff \M,i \models \varphi$ or $\M,i \models \psi$ +\item $\M,i \models \X \varphi \iff \M,i+1 \models \varphi$ +\item $\M,i \models \varphi \U \psi \iff \exists{k \geq i}: \M,k \models \psi$ and $\forall{i \leq j < k}: \M,j \models\varphi$ +\end{itemize} +\end{def:satisfiability} +\end{frame} + \begin{frame} \frametitle{Infinity} \framesubtitle{Word as function} @@ -386,125 +499,9 @@ \end{prop:general equiv} \end{frame} -{ -\setbeamercolor{normal text}{bg=black, fg=white} -\setbeamercolor{frametitle}{fg=white!30!black} -\usebeamercolor*{normal text} -\usebeamercolor*{frametitle} -\begin{frame} -\frametitle{Linear Temporal Logic} -\framesubtitle{Motivation 1/2} -\begin{center} -``It is dark.''\\ -\visible<2->{``It is \emph{always} dark.''\\} -\visible<3->{``It is \emph{currently} dark.''\\} -\visible<4->{``It will \emph{eventually} be dark.''\\} -\visible<5->{``It is dark \emph{until} someone puts the light on.''} -\end{center} -\end{frame} -} - -\begin{frame} -\frametitle{Linear Temporal Logic} -\framesubtitle{Motivation 2/2} -\begin{center} -\only<1->{ -\color{white} -\colorbox{black}{\makebox(50,10){It is dark}} \colorbox{orange}{\makebox(30,10){until}} \colorbox{black!30}{\makebox(50,10){there is light}}\\ -\visible<2->{ -\colorbox{black}{\makebox(50,10){$p_0$}} \colorbox{orange}{\makebox(30,10){$\U$}} \colorbox{black!30}{\makebox(50,10){$p_1$}}} -} -\end{center} -\end{frame} - -\begin{frame} -\frametitle{Linear Temporal Logic} -\framesubtitle{Syntax} -\begin{def:syntax} -Let $\Prop$ be the countable set of \emph{atomic propositions}, LTL-formulae $\varphi$ are defined using following productions: -\[\varphi ::= p \in \Prop \,|\, \neg \varphi \,|\, \varphi \lor \varphi \,|\, \X \varphi \,|\, \varphi \U \varphi\] -\begin{itemize} -\item $\neg, \lor$ corresponds to the Boolean \emph{negation} and \emph{disjunction}. -\item $\X$ reads \emph{next}. -\item $\U$ reads \emph{until}. -\end{itemize} -\end{def:syntax} -\end{frame} - -\begin{frame} -\frametitle{Linear Temporal Logic} -\framesubtitle{Semantics} -\begin{def:frames} -An LTL-\emph{frame} is a tuple $\F = (S, R)$: -\begin{itemize} -\item $S = \{s_i \mid i \in \N\}$ is the set of states. -\item $R = \{(s_i, s_{i+1}) \mid i \in \N\}$ is the accessibility relation. -\end{itemize} -\end{def:frames} - -\begin{def:models} -An LTL-\emph{model} is a tuple $\M = (\F, V)$: -\begin{itemize} -\item $\F$ is a \emph{frame}. -\item $V: S \to 2^\Prop$ is a \emph{valuation function}. -\item Intuitively we say $p \in \Prop$ is \emph{true} at time instant $i$ iff $p \in V(i)$. -\end{itemize} -\end{def:models} -\end{frame} - -\begin{frame} -\frametitle{Linear Temporal Logic} -\framesubtitle{Model Example} -\begin{figure} -\centering -\begin{tikzpicture}[shorten >=1pt, node distance=2.5cm, auto, semithick, >=stealth - ,accepting/.style={fill, gray!50!black, text=white}] -\node[state, initial, initial text=] (s_0) {$\{p_0\}$}; -\path (s_0) [late options={label=below:$s_0$}]; -\node[state] (s_1) [right of= s_0] {$\{p_0, p_2\}$}; -\path (s_1) [late options={label=below:$s_1$}]; -\node[state] (s_2) [right of= s_1] {$\{p_1\}$}; -\path (s_2) [late options={label=below:$s_2$}]; -\node[state] (s_i) [right of= s_2] {$\{p_1\}$}; -\path (s_i) [late options={label=below:$s_i$}]; -\path[->] -(s_0) edge node {$R$} (s_1) -(s_1) edge node {$R$} (s_2); -\path[dashed,->] -(s_2) edge node {$R$} (s_i); -\end{tikzpicture} -\end{figure} -\end{frame} - -\begin{frame} -\frametitle{Linear Temporal Logic} -\framesubtitle{Satisfiability} -\begin{def:satisfiability} -A model $\M = (\F, V)$ \emph{satisfies} a formula $\varphi$ at time instant $i$ is denoted by $\M,i \models \varphi$: -\begin{itemize} -\item $\M,i \models p$ for $p \in \Prop \iff p \in V(i)$ -\item $\M,i \models \neg \varphi \iff$ not $\M,i \models \varphi$ -\item $\M,i \models \varphi \lor \psi \iff \M,i \models \varphi$ or $\M,i \models \psi$ -\item $\M,i \models \X \varphi \iff \M,i+1 \models \varphi$ -\item $\M,i \models \varphi \U \psi \iff \exists{k \geq i}: \M,k \models \psi$ and $\forall{i \leq j < k}: \M,j \models\varphi$ -\end{itemize} -\end{def:satisfiability} -\end{frame} - \begin{frame} \frametitle{Model Checking} -\framesubtitle{Definition 1/2} -\begin{center} -%\only<1>{\colorbox{black}{\makebox(35,10){\color{white} $\M \models \varphi$}}} -\only<1>{\[\M \models \varphi\]} -\only<2->{Given a program $P$ and specification $\varphi$:\\ -\colorbox{black}{\makebox(150,10){\color{white} does every run of $P$ satisfy $\varphi$?}}} -\end{center} -\end{frame} - -\begin{frame} -\frametitle{Model Checking} -\framesubtitle{Definition 2/2} +\framesubtitle{Definition} \begin{thm:model checking} \label{thm:model checking} Let $\A_P$ be the automaton for program $P$ and let $\A_\varphi$ be the automaton for formula $\varphi$.\\