ディジタルATCデータベースの証明による検証
スポンサーリンク
概要
- 論文の詳細を見る
ディジタルATC線区データベース仕様を, コンピュータ上で行なわれる自動証明によって検証した.最初にデータベースの構造および最低限の操作に関する仕様を形式的仕様記述言語によって記述した.この仕様には軌道回路を始めとするデータベースの各構成要素間で常に満たさなければならない不変条件が記述されている.次にこの構造に矛盾のないこと, また操作によって不変条件が破壊されないことを保証するための証明責務を生成し, これを仕様とともに証明エンジンに投入した.一部の証明責務は自動で証明され, 残りの証明責務も証明エンジンを対話的に操作することにより証明された.すなわち仕様が矛盾のないことを完全に機械で証明することができた.
- 社団法人電子情報通信学会の論文
- 2001-12-07
著者
関連論文
- Bメソッドによる単線自動閉そく装置の検証 (ディペンダブルコンピューティング)
- 交流通電によるレール・車輪間接触抵抗低減について
- Bメソッドによる単線自動閉そく装置の検証(安全性及び一般)
- 1108 レール-車輪間の通電試験結果(第3報)(SS8-2 インターフェイス問題,SS8 境界領域研究,J-Rail 2006)
- レール/車輪試験片間の通電試験結果について
- 2409 (模擬)車輪-レール間の通電試験結果(第 1 報)
- 要求分析と統合的ライフサイクルコスト評価に基づいた鉄道信号システム構築手法の検討
- 鉄道信号システムの自然災害時における影響評価の考察 : 実際の障害データを用いた定量的分析(安全性・一般)
- 信号設備事故データの分析と評価
- 山岳トンネルの電磁遮蔽効果に対する解析手法の高度化
- 鉄道高架橋の電磁遮蔽効果解析手法の高度化
- 簡易な符号伝送による低周波軌道回路の耐ノイズ性能向上 (特集 信号通信技術)
- 長大軌道回路の耐ノイズ性能向上策
- A-18-6 ペトリネットを用いた超分散連動システムに対する一検討(A-18.安全性,一般講演)
- デジタルATC
- 段階的詳細化に基づく鉄道信号へのフォーマルメソッド適用法 (特集 信号通信技術)
- 車上速度照査式ATSの基本仕様検討
- 新幹線用無絶縁ATC軌道回路の開発
- 要求分析とアベイラビリティ評価に基づく鉄道信号システム構築の検討(安全性及び一般)
- 新幹線高架橋での電磁誘導測定試験と解析
- 高架橋の電磁遮蔽効果を考慮した誘導予測計算法の提案(2)
- 高架橋の電磁遮蔽効果を考慮した誘導予測計算法の提案
- 鉄道信号システムへのフォーマルメソッドの適用
- 段階的詳細化に基づく鉄道信号へのフォーマルメソッド適用
- 枠型スラブ軌道板の鉄筋が軌道回路へ与える影響の実測と数値計算解析
- 山岳トンネルの電磁遮蔽効果に対する解析手法の高度化
- 段階的詳細化によるシステムの高信頼化手法(安全性及び一般)
- 軌道短絡
- 1107 レール表面状態の違いによるレール-車輪間の接触抵抗の考察(SS8-2 インターフェイス問題,SS8 境界領域研究,J-Rail 2006)
- 現行システムと併用可能な車上速度照査式ATSの開発 (特集 信号通信技術)
- 現行ATSと併用可能な車上速度照査式ATS
- 6-2 鉄道におけるレールと車輪間の接触抵抗測定実験の効率化に対する検討(セッション6 安全性,理論)(日本信頼性学会第17回秋季信頼性シンポジウム報告)
- 軌道回路残留電圧波形分析による列車検知手法の開発 (特集:信号通信技術)
- 6-2 鉄道におけるレールと車輪間の接触抵抗測定実験の効率化に対する検討(セッション6 安全性、理論,第17回秋季信頼性シンポジウム)
- 超分散連動システムのアルゴリズムに関する検討
- [4-2] 鉄道信号用の超分散型連動装置の実現可能性の検討(セッション4 安全性,日本信頼性学会 第14回春季信頼性シンポジウム 報告)
- 4-2 鉄道信号用の超分散型連動装置の実現可能性の検討(安全性,セッション4)
- 軌道回路に適用する巡回符号の検定方法の検討
- 無絶縁軌道回路に対応した新幹線用デジタルATCの開発 (特集 信号通信技術)
- 軌道回路の短絡不良要因と改善手法 (特集 信号通信技術)
- フレキシブル信号システムの要件 : フレキシブル信号システムに関する協同研究委員会中間報告
- 鉄道信号システムへのフォーマルメソッドの適用 (特集 信号通信技術)
- 軌道回路の列車検知性能向上に関する研究 (特集 信号通信技術)
- ディジタルATCデータベースの証明による検証
- 新幹線用無絶縁ATC軌道回路の開発(試験報告)
- ディジタルATCの性能評価
- 耐ノイズ性を向上した中間軌道回路の開発 (特集 信号通信技術)
- 閑散線区に適した拠点無線式列車制御システム (特集 信号通信技術)
- アベイラビリティ評価指標による鉄道信号システム開発手法 (特集 信号通信技術)
- 軌道回路の列車検知性能向上に関する研究
- ペトリネットによる連動仕様の検証 (信号通信技術)
- 〔第3章 信号編〕 12. 雑音(誘導)
- モデル検査法による単線自動閉そく装置の検証(安全性及び一般)
- 軌道回路における短絡現象
- 遺伝的アルゴリズム
- 暗号キー
- 鉄道分野での高信頼性データベースの設計に関する一考察
- 高安全性システムのための要求分析技術 (特集:情報システム)
- 北陸新幹線(長野・金沢間)異周波境界におけるATC妨害電流予測計算
- 新幹線用無絶縁ATC軌道回路の開発 : 総合試験報告
- 車上受電器を用いた軌道回路の状態監視手法に関する研究
- IMESの鉄道分野への応用に関する基礎的検討
- シンポジウム論文優秀賞 閑散線区向けの拠点無線式列車制御システムの開発
- 北陸新幹線50/60Hzき電両用区間対応DS-ATCの開発 (特集 信号通信技術)
- レールと車輪間の電気的接触抵抗が有する半導体特性のモデル化 (レーザ・量子エレクトロニクス)
- レールと車輪間の電気的接触抵抗が有する半導体特性のモデル化 (光エレクトロニクス)
- レールと車輪間の電気的接触抵抗が有する半導体特性のモデル化 (電子部品・材料)
- レールと車輪間の電気的接触抵抗が有する半導体特性のモデル化 (機構デバイス)
- レールと車輪間の電気的接触抵抗が有する半導体特性のモデル化 (信頼性)
- レールと車輪の電気的接触抵抗に関する研究(機構デバイスの信頼性,信頼性一般)
- レールと車輪の電気的接触抵抗に関する研究(機構デバイスの信頼性,信頼性一般)
- 北陸新幹線(高崎・金沢間)60Hzき電区間対応DS-ATCの開発
- 軌道スラブ板鉄筋の等価導体モデル化手法
- VDMの紹介と鉄道信号への適用例(情報システムの信頼性・安全性)
- 北陸新幹線(長野・金沢間)50/60Hz対応DS-ATCの開発
- 無絶縁DS-ATCの開発と実用化
- 高架橋鉄筋の等価導体モデル化手法
- 車輪通過の繰り返しや通電によるレールと車輪間の接触抵抗への影響
- レールと車輪の電気的接触抵抗に関する研究
- 車輪通過の繰り返しや通電によるレールと車輪間の接触抵抗への影響
- レールと車輪間の電気的接触抵抗が有する半導体特性のモデル化(光部品・電子デバイス実装技術・信頼性,及び一般)
- レールと車輪間の電気的接触抵抗が有する半導体特性のモデル化(光部品・電子デバイス実装技術・信頼性,及び一般)
- レールと車輪間の電気的接触抵抗が有する半導体特性のモデル化(光部品・電子デバイス実装技術・信頼性,及び一般)
- レールと車輪間の電気的接触抵抗が有する半導体特性のモデル化(光部品・電子デバイス実装技術・信頼性,及び一般)
- レールと車輪間の電気的接触抵抗が有する半導体特性のモデル化(光部品・電子デバイス実装技術・信頼性,及び一般)