--- a/Slide/prosym.md	Thu Jan 18 13:38:10 2018 +0900
+++ b/Slide/prosym.md	Thu Jan 18 15:50:01 2018 +0900
@@ -9,7 +9,6 @@
 - 現代の OS では拡張性と信頼性を両立させることが要求されている。
 <!--信頼性 信頼性を保証するには従来のテストとデバッグでは不十分-->
 <!--信頼性を保証するには証明とモデル検査を用いる方法がある-->
-
 - 信頼性をノーマルレベルの計算に対して保証し、拡張性をメタレベルの計算で実現することを目標に Gears OS を設計中である。
 - ノーマルレベルの計算とメタレベルの計算を切り離して記述するために Code Gear と Data Gear という単位を用いている。
 - Gears OS は Continuation based C(CbC) によってアプリケーションと OS そのものを記述する。
@@ -18,16 +17,17 @@
 <!--
 # OS の拡張性と信頼性の両立
 
-さまざまなコンピュータの信頼性の基本はメモリなどの資源管理を行う OS である。
-時代とともに進歩するハードウェア、サービスに対応して OS 自体が拡張される必要がある。
-その信頼性を保証するには、従来の テストとデバッグでは不十分であり、テストしきれない部分が残ってしまう。
-これに対処するため には、証明を用いる方法とプログラムの可能な実行をすべて数え上げるモデル検査を用いる方法がある。
-検証は一度ですむものではなく、アプリケーションやサービス、デバイスが新しくなることに検証をやり直す必要がある。
-このため信頼性と拡張性を両立させることが重要である。
+- さまざまなコンピュータの信頼性の基本はメモリなどの資源管理を行う OS である。
+- 時代とともに進歩するハードウェア、サービスに対応して OS 自体が拡張される必要がある。
+- その信頼性を保証するには、従来の テストとデバッグでは不十分であり、テストしきれない部分が残ってしまう。
+- これに対処するため には、証明を用いる方法とプログラムの可能な実行をすべて数え上げるモデル検査を用いる方法がある。
+- 検証は一度ですむものではなく、アプリケーションやサービス、デバイスが新しくなることに検証をやり直す必要がある。
+- このため信頼性と拡張性を両立させることが重要である。
 -->
 <!--
 # 目次？ 
 -->
+
 # メタ計算の重要性
 - プログラムを記述する際、ノーマルレベルの処理の他に、メモリ管理やスレッド管理、CPU や GPU の資源管理等、記述しなければならない処理が存在する。これらの計算をメタ計算と呼ぶ。
 - メタ計算はノーマルレベルの計算から切り離して記述したい。
@@ -66,17 +66,22 @@
 - 接続された Data Gear 以外には参照を行わない。
 
 # Gears でのメタ計算
+- Gears OS ではメタ計算を Meta Code Gear、Meta Data Gear で表現する。
+- Meta Code Gear はノーマルレベルの Code Gear の直後に遷移され、メタ計算を実行する。
+- Meta Code Gear で OS の機能であるメモリ管理やスレッド管理を行う。
 
-- またGears OS ではメタ計算を Meta Code Gear、Meta Data Gear で表現する。
-- Meta Code Gear はノーマルの Code Gear の直後に遷移され、メタ計算を実行する。
-- Meta Code Gear で OS の機能であるメモリ管理やスレッド管理を行う。
+<div style="text-align: center;">
+　<img src="./fig/metaCS.pdf" alt="metaCS" width="600">
+</div>
 
 # Gears OS の構成
 
+<!--
 # CbC による Gears OS 記述の問題点
 - Gears OS を CbC で実装する上でメタ計算の記述が煩雑であることがわかった。
 - 本研究ではこれらのメタ計算を自動生成することにより Gears OS を記述する上においてより良い構文をユーザーに提供することにした。
 - そのためのプロトタイプとして perl スクリプトを作成した。
+-->
 
 # Context
 - Gears OS には Context と呼ばれる接続可能な Code Gear、Data Gear のリスト、Temporal Data Gear のためのメモリ空間等を持っている Meta Data Gear がある。