Protocol Verification by using LOTOS and Tools (part 1)

<セキュリティ社会システム特論(IT受講不可)>※2012年度不開講

■part 1 目次

0. 概要

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

2. プロセスと木

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

4. Basic LOTOS

5. 設計例

6. Full LOTOS

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

付録A. CADP toolboxのインストール

参考資料・リンク集


■必須提出課題

CADPセットアップ(課題0)

演習課題1

演習課題2

演習課題3

演習課題4


■レポート提出システム

■CAI進捗状況表示


■参考資料・リンク集

■質問・相談用掲示板(XOOPSフォーラム)

2012年2月21日 10:06 更新

 

items

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

担当: 和崎 克己
CAI進捗状況

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

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

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

※ライセンス申請・取得済み(情報工学科・情報工学専攻)
 →ダウンロード&セットアップ方法(VMWare仮想アプライアンス含む)はここから参照

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

what's new?


2012.2.21
平成24年度は不開講です

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


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

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


2008. 9. 29
セットアップ手順書をCADP ver.2006-a向けに更新しました

CADP toolbox ver.2006-a (stable) 向けに、セットアップ手順書を更新しました。また、caesar.adtがver5.2へ更新されたことに伴い、ADT抽象データ型のNATURALの制限値の設定方法(*.tファイルで指定)が変わりました。この変更に伴って、第6章と第7章の内容を更新しました。


2006. 5. 23
Fedra Core 5 (FC5) ではインストーラが正常に動きません

CADP toolbox をセットアップする際に使用するインストーラは、Fedra Core 5 上では正常に動作しない不具合があります。お手数ですが、RedHat, CentOS, FC4, Turbolinux, VineLinuxなどのパッケージをご利用ください。


2004. 1. 1
サイトがグランドオープンしました

Protocol Verification by using LOTOS and Tools (part 1) (情報工学専攻・セキュリティ社会システム特論(リアル学生の場合))のためのwebサイトがグランドオープンしました。概要、第1章から第7章、参考文献・リンク集、演習課題0から4(全5題)ならびにCADP toolboxのインストール・ライセンスファイル取得方法について説明してあります。内容は逐次更新・変更される可能性があります。


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