73 \mode<presentation>{ |
73 \mode<presentation>{ |
74 \begin{frame}[c] |
74 \begin{frame}[c] |
75 \frametitle{\large Prioirty Inheritance Protocol (PIP)} |
75 \frametitle{\large Prioirty Inheritance Protocol (PIP)} |
76 \large |
76 \large |
77 |
77 |
78 \begin{itemize} \large |
78 \begin{itemize} |
79 \item Widely used in Real-Time OSs \pause |
79 \item Widely used in Real-Time OSs \pause |
80 \item One solution of \textcolor{red}{`Priority Inversion'} problem \pause |
80 \item One solution of \textcolor{red}{`Priority Inversion'} \pause |
81 \item A flawed manual correctness proof (1990) \pause |
81 \item A flawed manual correctness proof (1990)\pause |
82 \begin{itemize} \large |
82 \begin{itemize} \large |
83 \item {Notations with no precise definition} |
83 \item {Notations with no precise definition} |
84 \item {Resorts to intuitions} |
84 \item {Resorts to intuitions} |
85 \end{itemize} \pause |
85 \end{itemize} \pause |
86 \item Formal treatments using model-checking \pause |
86 \item Formal treatments using model-checking \pause |
87 \begin{itemize} \large |
87 \begin{itemize} \large |
88 \item {Applicable to small size system models} |
88 \item {Applicable to small size system models} |
89 \item { Unhelpful for human understanding } |
89 \item { Unhelpful for human understanding } |
90 \end{itemize} \pause |
90 \end{itemize} \pause |
91 \item Verification of PCP in PVS (2000) \pause |
91 \item Verification of PCP in PVS (2000)\pause |
92 \begin{itemize} \large |
92 \begin{itemize} \large |
93 \item {A related protocol} |
93 \item {A related protocol} |
94 \item {Priority Ceiling Protocol} |
94 \item {Priority Ceiling Protocol} |
95 \end{itemize} |
95 \end{itemize} |
96 \end{itemize} |
96 \end{itemize} |
631 \frametitle{Conclusion} |
630 \frametitle{Conclusion} |
632 |
631 |
633 \begin{itemize} \large |
632 \begin{itemize} \large |
634 \item Aims fulfilled \medskip \pause |
633 \item Aims fulfilled \medskip \pause |
635 \item Alternative way \pause |
634 \item Alternative way \pause |
636 \begin{itemize} |
635 \begin{itemize} |
637 \item using Isabelle/HOL in OS code development \medskip |
636 \item using Isabelle/HOL in OS code development \medskip |
638 \item through the Inductive Approach |
637 \item through the Inductive Approach |
639 \end{itemize} \pause |
638 \end{itemize} \pause |
640 \item Future researches \pause |
639 \item Future researches \pause |
641 \begin{itemize} \large |
640 \begin{itemize} |
642 \item scheduler in RT-Linux\medskip |
641 \item scheduler in RT-Linux\medskip |
643 \item multiprocessor case\medskip |
642 \item multiprocessor case\medskip |
644 \item other ``nails'' ? (networks, \ldots) \pause |
643 \item other ``nails'' ? (networks, \ldots) \medskip \pause |
645 \item Refinement to real code and relation between implemenations |
644 \item Refinement to real code and relation between implemenations |
646 \end{itemize} |
645 \end{itemize} |
647 \end{itemize} |
646 \end{itemize} |
|
647 \end{frame}} |
|
648 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
649 *} |
|
650 |
|
651 text_raw {* |
|
652 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
653 \mode<presentation>{ |
|
654 \begin{frame}[c] |
|
655 \frametitle{Questions?} |
|
656 |
|
657 \begin{itemize} \large |
|
658 \item Thank you for listening! |
|
659 \end{itemize} |
|
660 |
648 \end{frame}} |
661 \end{frame}} |
649 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
662 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
650 *} |
663 *} |
651 |
664 |
652 |
665 |