リアクティブシステムの仕様記述、検証、および実装に関する研究
| Project/Area Number |
12780206
|
|---|
| Research Category |
Grant-in-Aid for Encouragement of Young Scientists (A)
|
| Allocation Type | Single-year Grants |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
緒方 和博 北陸先端科学技術大学院大学, 情報科学研究科, 助手 (30272991)
|
|---|
| Project Period (FY) |
2000 – 2001
|
| Project Status |
Completed (Fiscal Year 2001)
|
| Budget Amount *help |
¥600,000 (Direct Cost: ¥600,000)
Fiscal Year 2001: ¥600,000 (Direct Cost: ¥600,000)
|
|---|
| Keywords | リアクティブシステム / モデル化 / 検証 / 状態遷移機械 / CafeOBJ / 実時間 / 相互排除アルゴリズム / 鉄道信号システム / 仕様記述 / 安全性 / UNITY |
|---|
| Research Abstract |
本年度は、以下のことを行った。
・リアクティブシステムのモデル化および検証方法の整理:代数仕様言語CafeOBJおよびその実装であるCafeOBJシステムに基づくリアクティブシステムのモデル化および検証方法を整理、提案した。モデル化は、UNITY等で用いられている状態遷移機械を使って行い、作成したモデルをCafeOBJで記述し、モデルが望ましい性質を有する事をCafeOBJシステム支援のもとで行う。この方法に則り、以下のような事例研究を行った。
・分散相互排除アルゴリズムの検証:リアクティブシステムの代表例である分散相互排除アルゴリズムを例に提案方法の有効性を示した。解析したアルゴリズムは、Ricart, AgrawalaアルゴリズムとSuzuki, Kasamiアルゴリズムである。
・時間システムの分散実検証:実時間システムを扱えるように、提案方法を拡張した。有効性を示すため、鉄道の踏切り制御システム等の検証を行った。
・鉄道信号システムの検証:提案方法の有効性を示すため、2種類の鉄道信号システムを検証した。
|
Report
(2 results)
Research Products
(8 results)
