Protocol Verification by using LOTOS and Tools (part 1)

<セキュリティ社会システム特論>※隔年開講

■part 1 目次

0. 概要

1. 並行プロセスのモデル化

2. プロセスと木

3. プロセスの並列化構成

4. Basic LOTOS

5. 設計例

6. Full LOTOS

7. プロトコル検証の例(ABP)

(参考)CADP toolboxの新規ライセンス取得

参考資料・リンク集


■必須提出課題

演習課題1

演習課題2

演習課題3

演習課題4

 

 

items

先修推奨コンピュータネットワーク学部)、グラフ理論状態機械論の先修が望まれます。演習に必要なツールキットの使用には、Linux入門UNIX操作の基礎 程度のスキルが必要となります。

担当: 和崎 克己

演習時に必要なツールキット

ホームページへジャンプ!

CADP (Caesar/Aldebaran Development Package)
A Software Engineering Toolbox for Protocols and Distributed Systems : INRIA/VASY Project, FRANCE
ホームページ

※ライセンス申請・取得済み(情報工学科・情報工学専攻)

※ツールキットのダウンロードとセットアップを行うためのLinuxOS環境(CentOS、Ubuntu など)ならびにインターネット接続環境が必要です。VirtualBox仮想マシン上で演習する場合には,VirtualBoxが動作するintelベースPCが必要です.

what's new?


2017.4.4
平成27年度以降はeALPSコースウェアで展開します.

セキュリティ社会システム特論について,平成27年度以降はレポート提出など全てeALPS上で展開します.従前の「ReportSystem」は利用しないで下さい.


2016.4.1
平成28年度は不開講です

セキュリティ社会システム特論の授業実施について、平成28年度は不開講です(隔年開講).


2012.2.21
IT受講不可措置について

ITコース開講科目「システム検証」としては,平成24年度以降,IT受講不可となりました.



wasaki _AT_ cs.shinshu-u.ac.jp
Copyright(c) Katsumi Wasaki. All rights reserved.