prio/Slides/Slides1.thy
changeset 364 21428f38e506
parent 363 c89f82fb95f8
--- a/prio/Slides/Slides1.thy	Mon Aug 13 10:37:37 2012 +0000
+++ b/prio/Slides/Slides1.thy	Mon Aug 13 12:08:52 2012 +0000
@@ -110,13 +110,13 @@
   \begin{itemize}
   \item Undergraduate OS course in our university \pause
         \begin{itemize}
-           \item {\large Experiments using intrutional OSs }
-           \item {\large PINTOS (Stanford) is choosen }
+           \item {\large Experiments using instrutional OSs }
+           \item {\large PINTOS (Stanford) is chosen }
            \item {\large Core project: Implementing PIP in it}
         \end{itemize} \pause
-  \item Understanding is crucial to implemention \pause
-  \item Little help was found in the literature \pause
-  \item Some mentioning the complication
+  \item Understanding is crucial for the implemention \pause
+  \item Existing literature of little help \pause
+  \item Some mention the complication
   \end{itemize}
 
   \end{frame}}
@@ -189,7 +189,7 @@
   \large
 
   \begin{itemize}
-  \item Purpose: gurantee the most urgent task be processed in time
+  \item Purpose: gurantee the most urgent task to be processed in time
   \item Processes have priorities\\
   \item Resources can be locked and unlocked
   \end{itemize}
@@ -342,7 +342,7 @@
   \frametitle{Event Abstraction}
 
   \begin{itemize}\large
-     \item Use Inductive Approch of L. Paulson \pause
+     \item Use Inductive Approach of L. Paulson \pause
      \item System is event-driven \pause
      \item A \alert{state} is a list of events 
   \end{itemize}
@@ -537,7 +537,7 @@
   
   \begin{itemize}
   \item @{text "RAG s' = RAG s"}
-  \item No precedence needs to recalculate
+  \item No precedence needs to be recomputed
   \end{itemize}
 
   \end{frame}}
@@ -557,7 +557,7 @@
   
   \begin{itemize}
   \item @{text "RAG s' = RAG s"}
-  \item No precedence needs to recalculate
+  \item No precedence needs to be recomputed
   \end{itemize}
 
   \end{frame}}
@@ -636,12 +636,12 @@
            \item using Isabelle/HOL in OS code development \medskip
            \item through the Inductive Approach
        \end{itemize} \pause
-  \item Future researches \pause
+  \item Future research \pause
        \begin{itemize}
            \item scheduler in RT-Linux\medskip
            \item multiprocessor case\medskip
            \item other ``nails'' ? (networks, \ldots) \medskip \pause
-           \item Refinement to real code and relation between implemenations
+           \item Refinement to real code and relation between implementations
         \end{itemize}
   \end{itemize}
   \end{frame}}