1.1 --- a/paper/src/paper.tex Tue Jul 12 02:49:15 2011 +0200
1.2 +++ b/paper/src/paper.tex Tue Jul 12 13:43:09 2011 +0200
1.3 @@ -88,19 +88,25 @@
1.4 %\normalfont
1.5 \newpage
1.6 \section{Introduction}
1.7 -The rapid digital evolution of semi-conductor design has changed the way of development in the industry. Exponential growth in processing frequencies has massive implications on the complexity of chip-design. When a considerable portion of the development cycles is dedicated to design validation, an increasingly high effort is invested in the realisation of efficient verification methods.
1.8 +The rapid digital evolution of semi-conductor design has changed the way of development in the industry. Exponential growth in processing frequencies has massive implications on the complexity of chip-design. When a considerable portion of the development cycle is dedicated to design validation, an increasingly high effort is invested in the realisation of efficient verification methods.
1.9
1.10 -The computer hardware industry has adapted to the rise of complexity by the application of automated design verification. Another natural consequence was the preference of standard non-specialised hardware solutions accompanied by software realisation of the required functionality. Software systems have penetrated all industries, and increasingly so in high-demand and safety-critical application areas. Software programs provide high-demand server infrastructures for the internet, control our air traffic and protect our lifes in car accidents. When handling such critical systems, it becomes inevitable to verify the correctness of such software solutions.
1.11 +The computer hardware industry has adapted to the rise of complexity by the application of automated design verification. Another natural consequence was the preference of standard, non-specialised hardware solutions accompanied by software realisations of the required functionality. Software systems have penetrated all industries, and increasingly so in high-demand and safety-critical application areas. Software programs e.g. provide high-demand server infrastructures for the internet, control our air traffic and protect our lifes in car accidents. When handling such critical systems, it becomes inevitable to verify the correctness of such software solutions.
1.12
1.13 -Compared to hardware design, the highly dynamic properties of software components confront us with another state space explosion. Concurrent system designs increase the complexity of verification by some orders of magnitude; and concurrent applications have begun to dominate recent software solutions, because we are closing the physical limits for single-core processor frequencies.
1.14 +Compared to hardware design, the highly dynamic properties of software components confront us with another state space explosion. Concurrent system designs increase the complexity of verification by some orders of magnitude; and concurrent applications have started to dominate recent software solutions, because we are closing the physical limits for single-core processor frequencies.
1.15
1.16 -Again, the industry is facing a \emph{validation crisis} \cite{ref:automated verification} and formal verification methods are in demand. Deductive, manual and computer-supported verification techniques are an interesting digression, but may not be applicable in the validation of software programs of high complexity. Theories for algorithmic verification have existed for decades and recent successful applications have demonstrated their practical value.
1.17 +Again, the industry is facing a \emph{validation crisis} \cite{ref:automated verification} and formal verification methods are in high demand. Deductive, computer-supported verification techniques are an interesting digression, but may not be applicable in the validation of software programs of high complexity. Theories for algorithmic verification have existed for decades and recent successful applications have demonstrated their practical value.
1.18
1.19 -In this text, we provide an introduction to formal verification by means of algorithmic methods. Such an algorithmic approach is the base for automated verification procedures.
1.20 +In this text, we provide an introduction to formal verification by means of algorithmic methods. Such an algorithmic approach is the base for automated verification procedures. We will concentrate on the validation of reactive programs, without any loss of the general applicability of the presented methods. Reactive systems are, in contrast to terminating programs, continuous processes. Once initiated, a reactive system persists in an active state, where it reacts to concurrent inputs with appropriate actions. Examples of reactive systems are monitoring processes, schedulers and even whole operating systems.
1.21
1.22 -The first three sections will define the preliminaries for the automata-theoretic constructions. At first, we provide the notion of reasoning about infinite computational paths within formal language theory. Then we tackle those infinite structures with the help of automata theory, which shall build the framework of the formal verification theory. Next we introduce the reader to modal logics, in particular to linear temporal logic. Linear temporal logic is the language we use to talk about program properties, i.e., the propgram specification language. The fifth section interweaves automata theory and modal logics for the formalisation of program and specification automata construction. Based on this construction we apply the methods presented in the model checking section. The last section is a short excursion into the practical considerations of automated verification.
1.23 +The first three sections define the preliminaries for the automata-theoretic constructions. At first, we provide the notion of reasoning about infinite computational paths within formal language theory. Then we tackle those infinite structures with the help of automata theory, which shall build the framework of the formal verification theory. Next we introduce the reader to modal logics, in particular to linear temporal logic. Linear temporal logic is the language we use to talk about program properties, i.e., the propgram specification language.
1.24 +
1.25 +The fifth section interweaves automata theory and modal logics for the formalisation of the automata constructions, i.e., we construct automata depicting the program design and the specified properties. Based on this constructions, we apply the methods presented in the model checking section. The last section is a short excursion into the practical considerations of automated verification. For a successful application of automated verification, we consider ways of reducing the complexity of the automata-theoretic approach.
1.26 +
1.27 +The formal frame of this text is mostly based on Madhavan Mukund's \cite{ref:ltl&büchi} and Moshe Y. Vardi's \cite{ref:handbook} works. We will conclude this paper with a discussion of \cite{ref:ltl&büchi}.
1.28
1.29 \section{$\omega$-regular languages}
1.30 +For the formalisation of non-terminating, reactive systems, we need to get familiar with the concept of infinity. When a system is persistently active, the conceptual model of its input becomes an infinite structure, and likewise the description of its computational path. We want to settle this infinite structures within a formal corset.
1.31 +
1.32 \begin{def:finite words}
1.33 Let $\Sigma$ be a non-empty set of symbols, called the alphabet. $\Sigma^*$ is the set of all \emph{finite} words over $\Sigma$. A \emph{finite} word $w \in \Sigma^*$ is a \emph{finite} sequence $(v_0,...,v_{n-1})$ of symbols from alphabet $\Sigma$ with length $n = |w|$. $\varepsilon$ denotes the empty word with length $|\varepsilon| = 0$.
1.34 \end{def:finite words}
1.35 @@ -146,6 +152,8 @@
1.36 \end{def:omega regular languages closure}
1.37
1.38 \section{B\"uchi automata}
1.39 +Automata theory is the foundation of state-based modelling of computation. Non-deterministic automata provide an elegant way of describing interleaving systems. B\"uchi automata extend the idea of such automata to comfort the need for computational models on infinite inputs.
1.40 +
1.41 \begin{def:buechi automata}
1.42 A non-deterministic B\"uchi automaton is a tuple $\A = (\Sigma, S, S_0, \Delta, F)$, where $\Sigma$ is a finite non-empty \emph{alphabet}, $S$ is a finite non-empty set of \emph{states}, $S_0 \subseteq S$ is the set of \emph{initial states}, $F \subseteq S$ is the set of \emph{accepting states} and $\Delta: S \times \Sigma \times S$ is a \emph{transition relation}. When suitable we will use the arrow notation for the transitions, where $s \xrightarrow{a} s'$ iff $(s, a, s') \in \Delta$.
1.43
1.44 @@ -154,6 +162,8 @@
1.45 Within this text \emph{automaton} will refer to the non-deterministic B\"uchi automaton, unless otherwise noted.
1.46 \end{def:buechi automata}
1.47
1.48 +With infinite inputs comes a new definition of acceptance. Automata on finite inputs define acceptance by the termination of the computation in an accepting state. This notion needs adjustments, when modelling non-terminating systems. First, we need to define the legal sequence of state transitions of an automaton when reading an infinite input word.
1.49 +
1.50 \begin{def:automata runs}
1.51 Let $\A = (\Sigma, S, S_0, \Delta, F)$ be an automaton, a run $\rho$ of $\A$ on an infinite word $w = (a_0,a_1,...)$ over alphabet $\Sigma$ is a sequence $\rho = (s_0,s_1,...)$, where $s_0 \in S_0$ and $(s_i, a_i, s_{i+1}) \in \Delta$, for all $i \geq 0$. Again we may view the run sequence as a function $\rho : \N \to S$, where $\rho(i) = s_i$ denotes the state at the $i^{th}$ sequence position.
1.52 \end{def:automata runs}
1.53 @@ -166,9 +176,11 @@
1.54 The language $L_\omega(\A)$ recognised by automaton $\A$ is the set of all infinite words accepted by $\A$. A language $L$ is \emph{B\"uchi-recognisable} iff there is an automaton $\A$ with $L = L_\omega(\A)$.
1.55 \end{def:automata acceptance}
1.56
1.57 +Given all legal computations of an automaton, we have defined the acceptance condition. A computation is accepting, if it passes through an accepting state infinitely times. Since the set of states $S$ is finite, there must be a state $s \in S$, which occurs infinitely often within an infinite run; but it is not necessary, that $s$ is an accepting state, $F$ can be even an empty set.
1.58 +
1.59 \subsection{Generalised B\"uchi automata}
1.60 \begin{def:general automata}
1.61 -A \emph{generalised B\"uchi automaton} is a tuple $\A = (\Sigma, S, S_0, \Delta, \{F_i\}_{i < k})$ for $i, k \in \N$, where the \emph{acceppting states} $F_i$ are composed within a finite set with $F_i \subseteq S$.
1.62 +A \emph{generalised B\"uchi automaton} is a tuple $\A = (\Sigma, S, S_0, \Delta, \{F_i\})$ for $i \in \N$, where the \emph{acceppting states} $F_i$ are composed within a finite set with $F_i \subseteq S$.
1.63 \end{def:general automata}
1.64
1.65 \begin{def:general acceptance}
1.66 @@ -492,6 +504,11 @@
1.67 {\em Alternating Automata and Program Verification}.
1.68 Computer Science Today, Volume 1000 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 1995.
1.69
1.70 +\bibitem{ref:automated verification}
1.71 +\uppercase{M{\footnotesize oshe} Y. V{\footnotesize ardi}.}
1.72 +{\em Automated Verification: Graphs, Logic and Automata}.
1.73 +Proceeding of the International Joint Conference on Artificial Intelligence, Acapulco, 2003.
1.74 +
1.75 \bibitem{ref:on-the-fly verification}
1.76 \uppercase{R{\footnotesize ob} G{\footnotesize erth,} D{\footnotesize oron} P{\footnotesize eled,} M{\footnotesize oshe} Y. V{\footnotesize ardi and} P{\footnotesize ierre} W{\footnotesize olper}.}
1.77 {\em Simple On-the-fly Automatic Verification of Linear Temporal Logic}.
1.78 @@ -507,12 +524,12 @@
1.79 M{\footnotesize oshe} Y. V{\footnotesize ardi and}
1.80 A. P{\footnotesize rasad} S{\footnotesize istla}.}
1.81 {\em Reasoning about Infinite Computation Paths}.
1.82 -In Proceedings of the 24th IEEE FOCS, 1983.
1.83 +Proceedings of the 24th IEEE FOCS, 1983.
1.84
1.85 \bibitem{ref:handbook}
1.86 \uppercase{P{\footnotesize atrick} B{\footnotesize lackburn},
1.87 F{\footnotesize rank} W{\footnotesize olter and} J{\footnotesize ohan van} B{\footnotesize enthem}.}
1.88 {\em Handbook of Modal Logic (Studies in Logic and Practical Reasoning)}.
1.89 -3rd Edition, Elsevier, Amsterdam, 2007.
1.90 +3rd Edition, Elsevier, Amsterdam, P. 975-989, 2007.
1.91 \end{thebibliography}
1.92 \end{document}