\begin{frame}
  \frametitle{Where is Modal Logic Applied?}
  
  \begin{goal}{}
    Modal logic is applied in industry for 
    \begin{itemize}
      \item \emph{program verification},
      \item \emph{protocol validation}.
    \end{itemize}
  \end{goal}
  That is, to guarantee that a program / protocol is correct!
  \pause
  
  \tikzstyle{sensor}=[draw, fill=blue!20, text width=5em, 
      text centered, minimum height=2.5em,drop shadow]
  \tikzstyle{sensor2}=[sensor, text width=8.5em]
  \tikzstyle{ann} = [above, text width=5em, text centered]
  \tikzstyle{wa} = [sensor, text width=10em, fill=red!20, 
      minimum height=6em, rounded corners, drop shadow]
  \tikzstyle{sc} = [sensor, text width=13em, fill=red!20, 
      minimum height=10em, rounded corners, drop shadow]
  
  \begin{center}
  \scalebox{0.75}{{\small
  \begin{tikzpicture}[>=stealth]
  
      \node (wa) [wa]  {${\it Program}\vDash {\it Reqs}$};
      \draw[dashed, rounded corners=2mm] (wa.west)+(-4.5,-2.5) rectangle +(-1.9,2.2);
      \node at($(wa.west)+(-3.2,-2.2)$) {Modal Logic};
      \draw[dashed, rounded corners=2mm] (wa.west)+(-0.3,-2) rectangle +(4.1,1.3);
      \node at($(wa.south)+(0,-0.5)$) {Verifier / Model Checker};
      \path (wa.west)+(-3.2,1.5) node (asr1) [sensor] {${\it Req}_1$};
      \path (wa.west)+(-3.2,0.5) node (asr2)[sensor] {${\it Req}_2$};
      \path (wa.west)+(-3.2,-0.6) node (dots)[ann] {$\vdots$}; 
      \path (wa.west)+(-3.2,-1.0) node (asr3)[sensor] {${\it Req}_n$};
      \path (wa.east)+(3.0,0) node (vote) [sensor2] {Program / Protocol}; 
      \draw[dashed, rounded corners=2mm] (vote.west)+(-0.3,-0.7) rectangle +(3.5,0.7);
      \node at($(vote.south)+(0.0,-0.6)$) {};
  
      \begin{scope}[shorten <= 1mm, shorten >= 1mm]
      \path [draw, ->] (asr1.east) -- node [above] {} 
          (wa.160) ;
      \path [draw, ->] (asr2.east) -- node [above] {} 
          (wa.180);
      \path [draw, ->] (asr3.east) -- node [above] {} 
          (wa.200);
      \path [draw, <-] (wa.east) -- node [above] {} 
          (vote.west);
  
      \path (wa.south) +(0,3) node (asrs) {Verification process};
      \end{scope}
      
      \begin{pgfonlayer}{background}
          \path (asr1.west |- asr1.north)+(-0.7,0.6) node (a) {};
          \path (wa.south -| wa.east)+(+0.5,-0.3) node (b) {};
          \path (vote.east |- asrs.east)+(+0.5,-4.7) node (c) {};
            
          \path[fill=yellow!10,rounded corners, draw=black!50, dashed]
              (a) rectangle (c);           
          \path (asr1.north west)+(-0.2,0.2) node (a) {};  
      \end{pgfonlayer}
  \end{tikzpicture}
  }}\vspace{-2ex}
  \end{center}
  
  \begin{goal}{}
  The requirements are formulated in a variant of modal logic.
  \end{goal}
\end{frame}