1.1 Binary file slides/images/airbag.jpg has changed
2.1 Binary file slides/images/atc.jpg has changed
3.1 Binary file slides/images/intel.jpg has changed
4.1 --- a/slides/notes.txt Fri Jul 22 01:22:59 2011 +0200
4.2 +++ b/slides/notes.txt Fri Jul 22 04:33:59 2011 +0200
4.3 @@ -1,2 +1,117 @@
4.4 1. Guten Morgen! Mein Name ist Eugen Sawin und ich werde jetzt den einführenden Vortrag halten zum Seminar Automatenkonstruktionen im Model Checking.
4.5
4.6 +2. Was ich ihnen erzählen werde, wird die Meisten von euch bei der Bearbeitung des Themas in irgendeiner Form tangiert haben.
4.7 +
4.8 +3. Meine Präsentation soll einen Überblick geben über die algorithmische Verifikation reaktiver Systeme basierend auf dem automaten-theoretischen Ansatz des Model Checkings.
4.9 +
4.10 +==> 2
4.11 +
4.12 +4. PHI ist erfüllt in Modell M, oder Modell M modelliert PHI.
4.13 +Das ist der Kern unserer Bemühungen.
4.14 +Doch was bedeutet das?
4.15 +Wir übersetzen das in die Problemstellung der Verifikation von Systemen.
4.16 +
4.17 +==> 3
4.18 +
4.19 +5. Gegeben sei ein Programm und dessen Spezifikation, das Problem lautet:
4.20 +erfüllt jeder Durchlauf des Programms die Spezifikation?
4.21 +
4.22 +Bevor wir an die Tat schreiten um das Problem zu lösen,
4.23 +möchte ich eine andere Frage beantworten.
4.24 +
4.25 +Wieso das Ganze? Was ist der praktische Nutzen der Verifikation?
4.26 +
4.27 +==> 4
4.28 +
4.29 +Hard- und Softwaresysteme haben alle Bereiche der Industrie und damit auch unseren Alltag durchdrungen.
4.30 +Sie bilden die Infrastruktur unserer Kommunikation, bieten Sicherheit und retten sogar Leben.
4.31 +Und sie werden immer komplexer.
4.32 +Die Industrie investiert viel Zeit und Geld in die Verifikation sicherheitskritischer Systeme und der Kernkomponenten anderer Systeme.
4.33 +Die automatisierte Verifikation hat bereits in der Chip-Verifikation ihre praktische Anwendbarkeit gezeigt und ist in der Softwareindustrie stark gefragt.
4.34 +
4.35 +Also fangen wir an.
4.36 +
4.37 +==> 5
4.38 +
4.39 +Wenn ich sage: "Es ist dunkel." ist es nicht eindeutig, was ich damit ausdrücken möchte.
4.40 +
4.41 +Ich könnte damit meinen "Es ist immer dunkel.", doch das spricht gegen unsere Intuition.
4.42 +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).
4.43 +
4.44 +Wenn wir nach draußen schauen, können wir aus Erfahrung behaupten, dass es "notwendigerweise irgendwann dunkel wird."
4.45 +
4.46 +Unsere Sprache erlaubt es uns auch kausale Zusammenhänge zu bilden, wie z.B. "Es ist dunkel, bis Jemand das Licht an macht."
4.47 +
4.48 +Wir sehen, dass die natürliche Sprache nicht eindeutig ist und somit zur formalen Beschreibung ungeeignet.
4.49 +Wie können wir unsere Sprache zähmen, ohne die Ausdruckskraft zu verlieren.
4.50 +Nun, als Ersten machen wir das Licht wieder an!
4.51 +
4.52 +==> 6
4.53 +
4.54 +Nehmen wir den letzten Satz in einer allgemeineren Form als Beispiel.
4.55 +Dieser Satz sollte allgemeingültig sein.
4.56 +Wie können wir die Aussage dieses Satzes formal festhalten?
4.57 +Wir bedienen uns der Aussagenlogik und erweitern diese um eine weitere Verknüpfung.
4.58 +
4.59 +==> 6(2)
4.60 +
4.61 +Dabei sind p0 und p1 Elementaraussagen, sog. Atome, die entsprechend für "Es is dunkel" und "Es gibt licht" stehen.
4.62 +Die neue Verknüpfung nennen wir trivialerweise "until" und notieren sie mit dem kalligraphischen U.
4.63 +Halten wir das formal fest.
4.64 +
4.65 +==> 7
4.66 +
4.67 +Wir definieren die Syntax der linearen temporalen Logik mit Hilfe dieser Produktionen in Backus-Naur-Form.
4.68 +Somit ist eine LTL-Formel entweder ein aussagenlogisches Atom, eine negierte Formel oder eine Disjunktion zweier Formeln.
4.69 +Das kannten wir bereits aus der Aussagenlogik.
4.70 +Die Erweiterung sind das kalligraphische X, welches für "Next" steht und das "Until" aus dem Beispiel.
4.71 +Diese Syntaxdefinition bildet das Fundament für weitere abgeleitete Verknüpfungen.
4.72 +
4.73 +==> 8
4.74 +
4.75 +Wir interpretieren LTL-Formeln über unendliche Sequenzen von Aussagen.
4.76 +Die Sequenz entspricht der zeitlichen Abfolge von Ereignissen in einem vorwärts gerichteteten diskreten Zeitverlauf.
4.77 +Diese Interpretation heißt die Kripke-Semantik.
4.78 +Das Kripke-Modell der LTL-Semantik besteht aus einer abzählbaren Menge von Zuständen, verknüpft duch die Erreichbarkeitsrelation und der Bewertungsfunktion V.
4.79 +Da wir nur lineare Abfolgen betrachten, fällt die Erreichbarkeitsrelation einfach aus.
4.80 +Von einem beliebigen Zustand ist jeweils nur dessen Nachfolger erreichbar.
4.81 +Die Bewertungsfunktion liefert uns die Menge aller gültigen Atome für einen bestimmten Zustand.
4.82 +Intuitiv sagt man, ein Atom p ist wahr zum Zeitpunkt i gdw. p in der Menge V(i) ist.
4.83 +
4.84 +==> 9
4.85 +
4.86 +Hier ist eine Veranschaulichung eines Beispielmodells.
4.87 +Man sieht die Zustände s0 bis si und den Zeitverlauf durch die Relation R.
4.88 +Für jeden Zustand ist die Rückgabe der Bewertungsfunktion als Menge positiver Atome abgebildet.
4.89 +
4.90 +==> 10
4.91 +
4.92 +Die Erfüllbarkeit einer Formel zu einem Zeitpunkt i im Modell M ist folgendermaßen definiert:
4.93 +- ein Atom p ist erfüllbar gdw. und p in der Menge V(i) ist
4.94 +- eine negierte Formel PHI ist erfüllbar gdw. PHI nicht erfüllbar ist
4.95 +- eine Disjunktion von PHI und PSI ist erfüllbar gdw. PHI oder PSI erfüllbar ist
4.96 +- Next PHI ist erfüllbar gdw. PHI im darauffolgenden Zeitpunkt erfüllbar ist
4.97 +- 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.
4.98 +
4.99 +Mit Hilfe der linearen temporalen Logik lassen sich Programmeigenschaften und derren zeitliche Abhängigkeiten genau beschreiben.
4.100 +Als nächstes werden wir uns den Automaten widmen, die auf unendlichen Eingaben operieren.
4.101 +
4.102 +==> 11
4.103 +
4.104 +Wieso sind unsere Eingaben überhaupt unendlich?
4.105 +Im Gegensatz zu terminierenden Programmen sind reaktive Systeme fortlaufende Prozesse.
4.106 +Ein mal initiiert, verbleiben reaktive Systeme in einem aktiven Zustand und reagieren auf nebenläufige Eingaben.
4.107 +Theoretisch betrachtet, arbeiten solche Systeme somit auf unendlichen Eingabesequenzen.
4.108 +
4.109 +==> 12
4.110 +
4.111 +Hier ist ein Beispielautomat, der auf unendlichem Input arbeitet.
4.112 +Sieht jemand auf Anhieb welche Sprache dieser Automate akzeptiert?
4.113 +w1 ist eine Eingabe, der Überstrich soll eine periodische Wiederholung der Sequenz darstellen.
4.114 +....
4.115 +
4.116 +
4.117 +
4.118 +
4.119 +
4.120 +
5.1 --- a/slides/src/slides.tex Fri Jul 22 01:22:59 2011 +0200
5.2 +++ b/slides/src/slides.tex Fri Jul 22 04:33:59 2011 +0200
5.3 @@ -89,25 +89,138 @@
5.4
5.5 \begin{frame}
5.6 \frametitle{Motivation}
5.7 -\framesubtitle{Model Checking}
5.8 +\framesubtitle{Model Checking 1/2}
5.9 \begin{center}
5.10 %\only<1>{\colorbox{black}{\makebox(35,10){\color{white} $\M \models \varphi$}}}
5.11 -\only<1>{\[\M \models \varphi\]}
5.12 -\only<2->{Given a program $P$ and specification $\varphi$:\\
5.13 -\colorbox{black}{\makebox(150,10){\color{white} does every run of $P$ satisfy $\varphi$?}}}
5.14 +\[\M \models \varphi\]
5.15 \end{center}
5.16 \end{frame}
5.17
5.18 \begin{frame}
5.19 \frametitle{Motivation}
5.20 +\framesubtitle{Model Checking 2/2}
5.21 +\begin{center}
5.22 +Given a program $P$ and specification $\varphi$:\\
5.23 +\colorbox{black}{\makebox(150,10){\color{white} does every run of $P$ satisfy $\varphi$?}}
5.24 +\end{center}
5.25 +\end{frame}
5.26 +
5.27 +\begin{frame}
5.28 +\frametitle{Motivation}
5.29 +\framesubtitle{Industry}
5.30 \begin{figure}
5.31 \centering
5.32 -\subfigure{\includegraphics[width=100pt,height=70pt]{images/intel.jpg}}
5.33 -\subfigure{\includegraphics[width=100pt,height=70pt]{images/airbag.jpg}}
5.34 -\subfigure{\includegraphics[width=100pt,height=70pt]{images/atc.jpg}}
5.35 +\subfigure{\includegraphics[width=70pt,height=50pt]{images/intel.jpg}}
5.36 +\subfigure{\includegraphics[width=70pt,height=50pt]{images/airbag.jpg}}
5.37 +\subfigure{\includegraphics[width=70pt,height=50pt]{images/atc.jpg}}
5.38 \end{figure}
5.39 \end{frame}
5.40
5.41 +{
5.42 +\setbeamercolor{normal text}{bg=black, fg=white}
5.43 +\setbeamercolor{frametitle}{fg=white!30!black}
5.44 +\usebeamercolor*{normal text}
5.45 +\usebeamercolor*{frametitle}
5.46 +\begin{frame}
5.47 +\frametitle{Linear Temporal Logic}
5.48 +\framesubtitle{Motivation 1/2}
5.49 +\begin{center}
5.50 +``It is dark.''\\
5.51 +\visible<2->{``It is \emph{always} dark.''\\}
5.52 +\visible<3->{``It is \emph{currently} dark.''\\}
5.53 +\visible<4->{``It will \emph{eventually} be dark.''\\}
5.54 +\visible<5->{``It is dark \emph{until} someone puts the light on.''}
5.55 +\end{center}
5.56 +\end{frame}
5.57 +}
5.58 +
5.59 +\begin{frame}
5.60 +\frametitle{Linear Temporal Logic}
5.61 +\framesubtitle{Motivation 2/2}
5.62 +\begin{center}
5.63 +\only<1->{
5.64 +\color{white}
5.65 +\colorbox{black}{\makebox(50,10){It is dark}} \colorbox{orange}{\makebox(30,10){until}} \colorbox{black!30}{\makebox(50,10){there is light}}\\
5.66 +\visible<2->{
5.67 +\colorbox{black}{\makebox(50,10){$p_0$}} \colorbox{orange}{\makebox(30,10){$\U$}} \colorbox{black!30}{\makebox(50,10){$p_1$}}}
5.68 +}
5.69 +\end{center}
5.70 +\end{frame}
5.71 +
5.72 +\begin{frame}
5.73 +\frametitle{Linear Temporal Logic}
5.74 +\framesubtitle{Syntax}
5.75 +\begin{def:syntax}
5.76 +Let $\Prop$ be the countable set of \emph{atomic propositions}, LTL-formulae $\varphi$ are defined using following productions:
5.77 +\[\varphi ::= p \in \Prop \,|\, \neg \varphi \,|\, \varphi \lor \varphi \,|\, \X \varphi \,|\, \varphi \U \varphi\]
5.78 +\begin{itemize}
5.79 +\item $\neg, \lor$ corresponds to the Boolean \emph{negation} and \emph{disjunction}.
5.80 +\item $\X$ reads \emph{next}.
5.81 +\item $\U$ reads \emph{until}.
5.82 +\end{itemize}
5.83 +\end{def:syntax}
5.84 +\end{frame}
5.85 +
5.86 +\begin{frame}
5.87 +\frametitle{Linear Temporal Logic}
5.88 +\framesubtitle{Semantics}
5.89 +\begin{def:frames}
5.90 +An LTL-\emph{frame} is a tuple $\F = (S, R)$:
5.91 +\begin{itemize}
5.92 +\item $S = \{s_i \mid i \in \N\}$ is the set of states.
5.93 +\item $R = \{(s_i, s_{i+1}) \mid i \in \N\}$ is the accessibility relation.
5.94 +\end{itemize}
5.95 +\end{def:frames}
5.96 +
5.97 +\begin{def:models}
5.98 +An LTL-\emph{model} is a tuple $\M = (\F, V)$:
5.99 +\begin{itemize}
5.100 +\item $\F$ is a \emph{frame}.
5.101 +\item $V: S \to 2^\Prop$ is a \emph{valuation function}.
5.102 +\item Intuitively we say $p \in \Prop$ is \emph{true} at time instant $i$ iff $p \in V(i)$.
5.103 +\end{itemize}
5.104 +\end{def:models}
5.105 +\end{frame}
5.106 +
5.107 +\begin{frame}
5.108 +\frametitle{Linear Temporal Logic}
5.109 +\framesubtitle{Model Example}
5.110 +\begin{figure}
5.111 +\centering
5.112 +\begin{tikzpicture}[shorten >=1pt, node distance=2.5cm, auto, semithick, >=stealth
5.113 + ,accepting/.style={fill, gray!50!black, text=white}]
5.114 +\node[state, initial, initial text=] (s_0) {$\{p_0\}$};
5.115 +\path (s_0) [late options={label=below:$s_0$}];
5.116 +\node[state] (s_1) [right of= s_0] {$\{p_0, p_2\}$};
5.117 +\path (s_1) [late options={label=below:$s_1$}];
5.118 +\node[state] (s_2) [right of= s_1] {$\{p_1\}$};
5.119 +\path (s_2) [late options={label=below:$s_2$}];
5.120 +\node[state] (s_i) [right of= s_2] {$\{p_1\}$};
5.121 +\path (s_i) [late options={label=below:$s_i$}];
5.122 +\path[->]
5.123 +(s_0) edge node {$R$} (s_1)
5.124 +(s_1) edge node {$R$} (s_2);
5.125 +\path[dashed,->]
5.126 +(s_2) edge node {$R$} (s_i);
5.127 +\end{tikzpicture}
5.128 +\end{figure}
5.129 +\end{frame}
5.130 +
5.131 +\begin{frame}
5.132 +\frametitle{Linear Temporal Logic}
5.133 +\framesubtitle{Satisfiability}
5.134 +\begin{def:satisfiability}
5.135 +A model $\M = (\F, V)$ \emph{satisfies} a formula $\varphi$ at time instant $i$ is denoted by $\M,i \models \varphi$:
5.136 +\begin{itemize}
5.137 +\item $\M,i \models p$ for $p \in \Prop \iff p \in V(i)$
5.138 +\item $\M,i \models \neg \varphi \iff$ not $\M,i \models \varphi$
5.139 +\item $\M,i \models \varphi \lor \psi \iff \M,i \models \varphi$ or $\M,i \models \psi$
5.140 +\item $\M,i \models \X \varphi \iff \M,i+1 \models \varphi$
5.141 +\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$
5.142 +\end{itemize}
5.143 +\end{def:satisfiability}
5.144 +\end{frame}
5.145 +
5.146 \begin{frame}
5.147 \frametitle{Infinity}
5.148 \framesubtitle{Word as function}
5.149 @@ -386,125 +499,9 @@
5.150 \end{prop:general equiv}
5.151 \end{frame}
5.152
5.153 -{
5.154 -\setbeamercolor{normal text}{bg=black, fg=white}
5.155 -\setbeamercolor{frametitle}{fg=white!30!black}
5.156 -\usebeamercolor*{normal text}
5.157 -\usebeamercolor*{frametitle}
5.158 -\begin{frame}
5.159 -\frametitle{Linear Temporal Logic}
5.160 -\framesubtitle{Motivation 1/2}
5.161 -\begin{center}
5.162 -``It is dark.''\\
5.163 -\visible<2->{``It is \emph{always} dark.''\\}
5.164 -\visible<3->{``It is \emph{currently} dark.''\\}
5.165 -\visible<4->{``It will \emph{eventually} be dark.''\\}
5.166 -\visible<5->{``It is dark \emph{until} someone puts the light on.''}
5.167 -\end{center}
5.168 -\end{frame}
5.169 -}
5.170 -
5.171 -\begin{frame}
5.172 -\frametitle{Linear Temporal Logic}
5.173 -\framesubtitle{Motivation 2/2}
5.174 -\begin{center}
5.175 -\only<1->{
5.176 -\color{white}
5.177 -\colorbox{black}{\makebox(50,10){It is dark}} \colorbox{orange}{\makebox(30,10){until}} \colorbox{black!30}{\makebox(50,10){there is light}}\\
5.178 -\visible<2->{
5.179 -\colorbox{black}{\makebox(50,10){$p_0$}} \colorbox{orange}{\makebox(30,10){$\U$}} \colorbox{black!30}{\makebox(50,10){$p_1$}}}
5.180 -}
5.181 -\end{center}
5.182 -\end{frame}
5.183 -
5.184 -\begin{frame}
5.185 -\frametitle{Linear Temporal Logic}
5.186 -\framesubtitle{Syntax}
5.187 -\begin{def:syntax}
5.188 -Let $\Prop$ be the countable set of \emph{atomic propositions}, LTL-formulae $\varphi$ are defined using following productions:
5.189 -\[\varphi ::= p \in \Prop \,|\, \neg \varphi \,|\, \varphi \lor \varphi \,|\, \X \varphi \,|\, \varphi \U \varphi\]
5.190 -\begin{itemize}
5.191 -\item $\neg, \lor$ corresponds to the Boolean \emph{negation} and \emph{disjunction}.
5.192 -\item $\X$ reads \emph{next}.
5.193 -\item $\U$ reads \emph{until}.
5.194 -\end{itemize}
5.195 -\end{def:syntax}
5.196 -\end{frame}
5.197 -
5.198 -\begin{frame}
5.199 -\frametitle{Linear Temporal Logic}
5.200 -\framesubtitle{Semantics}
5.201 -\begin{def:frames}
5.202 -An LTL-\emph{frame} is a tuple $\F = (S, R)$:
5.203 -\begin{itemize}
5.204 -\item $S = \{s_i \mid i \in \N\}$ is the set of states.
5.205 -\item $R = \{(s_i, s_{i+1}) \mid i \in \N\}$ is the accessibility relation.
5.206 -\end{itemize}
5.207 -\end{def:frames}
5.208 -
5.209 -\begin{def:models}
5.210 -An LTL-\emph{model} is a tuple $\M = (\F, V)$:
5.211 -\begin{itemize}
5.212 -\item $\F$ is a \emph{frame}.
5.213 -\item $V: S \to 2^\Prop$ is a \emph{valuation function}.
5.214 -\item Intuitively we say $p \in \Prop$ is \emph{true} at time instant $i$ iff $p \in V(i)$.
5.215 -\end{itemize}
5.216 -\end{def:models}
5.217 -\end{frame}
5.218 -
5.219 -\begin{frame}
5.220 -\frametitle{Linear Temporal Logic}
5.221 -\framesubtitle{Model Example}
5.222 -\begin{figure}
5.223 -\centering
5.224 -\begin{tikzpicture}[shorten >=1pt, node distance=2.5cm, auto, semithick, >=stealth
5.225 - ,accepting/.style={fill, gray!50!black, text=white}]
5.226 -\node[state, initial, initial text=] (s_0) {$\{p_0\}$};
5.227 -\path (s_0) [late options={label=below:$s_0$}];
5.228 -\node[state] (s_1) [right of= s_0] {$\{p_0, p_2\}$};
5.229 -\path (s_1) [late options={label=below:$s_1$}];
5.230 -\node[state] (s_2) [right of= s_1] {$\{p_1\}$};
5.231 -\path (s_2) [late options={label=below:$s_2$}];
5.232 -\node[state] (s_i) [right of= s_2] {$\{p_1\}$};
5.233 -\path (s_i) [late options={label=below:$s_i$}];
5.234 -\path[->]
5.235 -(s_0) edge node {$R$} (s_1)
5.236 -(s_1) edge node {$R$} (s_2);
5.237 -\path[dashed,->]
5.238 -(s_2) edge node {$R$} (s_i);
5.239 -\end{tikzpicture}
5.240 -\end{figure}
5.241 -\end{frame}
5.242 -
5.243 -\begin{frame}
5.244 -\frametitle{Linear Temporal Logic}
5.245 -\framesubtitle{Satisfiability}
5.246 -\begin{def:satisfiability}
5.247 -A model $\M = (\F, V)$ \emph{satisfies} a formula $\varphi$ at time instant $i$ is denoted by $\M,i \models \varphi$:
5.248 -\begin{itemize}
5.249 -\item $\M,i \models p$ for $p \in \Prop \iff p \in V(i)$
5.250 -\item $\M,i \models \neg \varphi \iff$ not $\M,i \models \varphi$
5.251 -\item $\M,i \models \varphi \lor \psi \iff \M,i \models \varphi$ or $\M,i \models \psi$
5.252 -\item $\M,i \models \X \varphi \iff \M,i+1 \models \varphi$
5.253 -\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$
5.254 -\end{itemize}
5.255 -\end{def:satisfiability}
5.256 -\end{frame}
5.257 -
5.258 \begin{frame}
5.259 \frametitle{Model Checking}
5.260 -\framesubtitle{Definition 1/2}
5.261 -\begin{center}
5.262 -%\only<1>{\colorbox{black}{\makebox(35,10){\color{white} $\M \models \varphi$}}}
5.263 -\only<1>{\[\M \models \varphi\]}
5.264 -\only<2->{Given a program $P$ and specification $\varphi$:\\
5.265 -\colorbox{black}{\makebox(150,10){\color{white} does every run of $P$ satisfy $\varphi$?}}}
5.266 -\end{center}
5.267 -\end{frame}
5.268 -
5.269 -\begin{frame}
5.270 -\frametitle{Model Checking}
5.271 -\framesubtitle{Definition 2/2}
5.272 +\framesubtitle{Definition}
5.273 \begin{thm:model checking}
5.274 \label{thm:model checking}
5.275 Let $\A_P$ be the automaton for program $P$ and let $\A_\varphi$ be the automaton for formula $\varphi$.\\
