鉄道信号システムのモデル検査器SPINによる検証
スポンサーリンク
概要
- 論文の詳細を見る
The verification of safety requirements is a fundamental problem in railway signalling system design. Especially, specification of railway inter-locking systems, which control railway signals and points in a station in a safety-critical manner, becomes very complex and hard to verify. Recently in this fields, formal verification is expected to be a promising technique for verifying safety requirements. This paper describes how to verify a railway inter-locking specifications by the model checker SPIN which is a formal verification tool. In this method, a railway inter-locking system is described as a finite state machine and safety requirements are given by temporal logic formulas. Then, SPIN checks that the state machine satisfies the requirements.
著者
-
越村 三幸
九州大学大学院システム情報科学研究院
-
大神 茂之
九州大学大学院システム情報科学府知能システム学専攻
-
清水 亮
九州大学大学院システム情報科学府知能システム学専攻
-
越村 三幸
九州大学大学院システム情報科学研究院知能システム部門
関連論文
- 帰納論理プログラミングを用いたブログからのルール抽出 (「Web情報処理」および一般発表)
- モデル列挙とモデル計数(最近のSAT技術の発展)
- ODPを利用したユーザプロファイルを用いた個人化検索システム(情報検索)
- 帰納論理プログラミングを用いたWebページ評価ルールの抽出とその評価(「Webインテリジェンス」及び一般)
- 2C-6 Blogデータのクラスタリングと分析(コンテンツ推薦,一般セッション,データベースとメディア)
- 関連単語抽出アルゴリズムを用いたWeb検索クエリの生成(Web情報検索,データ工学論文)
- F-039 モデル生成法を用いた極小モデル生成(人工知能・ゲーム,一般論文)
- Wikipediaへの関連単語抽出アルゴリズムの適用とその評価(Wikipedia)
- 関連単語抽出アルゴリズムを用いたWeb検索クエリの生成(Web解析・検索クエリ)
- 1V-6 変数のアクティビティ情報を共有するマルチスレッドSATソルバ(学習・推論,学生セッション,人工知能と認知科学)
- 6S-9 ユーザーのスケジュールを用いたWebページ推薦(ユーザ指向・推薦,学生セッション,データベースとメディア)
- D-008 相関ルールに基づく文書検索システム(D分野:データベース)
- スケジュールに基づくWebページ推薦に用いる検索単語の選定(WEBサービス,特集「Web情報処理」及び一般)
- スケジュールに基づく Web ページ推薦に用いる検索単語の選定
- FPGA上のSATソルバPCMGTPへの前処理の導入
- D_024 ユーザの意思を反映したWeb検索の効率化(D分野:データベース)
- C_003 FPGAを用いたN-Queens問題の解決について(C分野:ハードウェア)
- MGTPにおけるケース分割の重複削除手法とその評価
- B_025 モデル検査器を用いたFUCEマルチスレッドプログラムの開発(B分野:ソフトウェア)
- 鉄道信号システムのモデル検査器SPINによる検証
- 抽象モデル生成による節集合の前処理(「自動推論:帰納,演繹,モデル検査/生成,学習,発見,仮説推論、論理プログラム,プランニングetc.」及び一般)
- モデル生成型定理証明手続きによるCTLのモデル検査(「自動推論:帰納,演繹,モデル検査/生成,学習,発見,仮説推論,論理プログラム,プランニングetc.」及び一般)(自動推論)
- 導出法に基づく定理証明系のJavaによる実現手法について(「自動推論:帰納,演繹,モデル検査/生成,学習,発見,仮説推論,論理プログラム,プランニングetc.」及び一般)(自動推論)
- ブール制約解消系によるモデル生成木の刈込み(自動推論 : 演繹, 帰納, モデル検査/生成, 仮説推論アブダクション, 論理プログラム, プランニング, 時相論理, etc.)
- Fuce言語HALの設計と実装
- ダイアグラムに基づく法的論争支援システム
- 抽象モデル生成による不要節の削除(人工知能,認知科学)
- Twitterにおける流行語先取り発言者の検出システムの開発
- Twitterにおける流行語先取り発言者の検出システムの開発
- ソーシャルブックマークにおける有用なユーザの発見
- Wikipediaのリンク共起とカテゴリに基づくリランキング手法
- Wikipediaのリンク共起とカテゴリに基づくリランキング手法
- Wikipediaへの関連単語抽出アルゴリズムの適用とその評価(Wikipedia)
- 関連単語抽出アルゴリズムを用いたWeb検索クエリの生成(Web解析・検索クエリ)
- ODPを利用したユーザプロファイルを用いた個人化検索システム(情報検索)
- 5S-4 Twitterの流行語発言者の抽出に基づくフォロワー推薦システムの開発(情報推薦(2),学生セッション,データベースとメディア,情報処理学会創立50周年記念)
- Twitter における流行語先取り発言者の検出システムの開発
- Wikipedia のリンク共起とカテゴリに基づくリランキング手法
- Partial Max-SATソルバーQMaxSATの評価 (特集 「AIの基本問題SATと応用技術」および一般)
- 数独パズルにおける補題の解析 : 補題の一般化に向けて
- FPGA上に実装されたPCMGTPを用いたSAT問題の解決(応用1, FRGAとその応用及び一般)
- FPGA上に実装されたPCMGTPを用いたSAT問題の解決(応用1, FRGAとその応用及び一般)
- FPGA上に実装されたPCMGTPを用いたSAT問題の解決(応用1, FRGAとその応用及び一般)
- FPGA上に実装されたPCMGTPを用いたSAT問題の解決
- F-021 基数制約を用いたMax-SATソルバーの試作(F分野:人工知能・ゲーム,一般論文)
- F-019 BOINCによるSATソルバーの並列実行(F分野:人工知能・ゲーム,一般論文)
- D-033 データ解析における並列分散処理基盤Hadoopの利用(D分野:データベース,一般論文)
- 1W-9 モデル生成によるSATソルバの並列化(最適化,学生セッション,人工知能と認知科学,情報処理学会創立50周年記念)
- 5R-2 ODPを利用した個人化検索システムの比較と効率化(Webシステム,学生セッション,データベースとメディア,情報処理学会創立50周年記念)
- 3C-2 動詞の提示による動的な検索支援システム(Web検索支援,一般セッション,データベースとメディア,情報処理学会創立50周年記念)
- 一般化補題を利用したモデル生成法
- ノンホーン・マジックセット変換節数の削減手法とその評価
- 抽象モデルを利用したSAT問題の前処理(「自動化:推論,発見,学習,データマイニング」及び一般)
- FPGA上のSATソルバPCMGTPの改良について
- Solving Open Job-Shop Scheduling Problems by SAT Encoding
- 上昇型定理証明の探索効率を高めるノンホーン・マジックセット
- 帰納論理プログラミングを用いた棋譜からのルール抽出
- Twitterのリスト機能を用いたユーザの特徴抽出
- Twitter発言の時系列解析に基づくハッシュタグの内容説明
- Wikipediaの時系列アクセス数に着目した関連度算出
- CMGTPへの事後関連性検査と畳込み機構の組込み
- 二分決定グラフによるモデル生成木の刈込み
- 二分決定グラフによるモデル生成木の刈込み
- 二分決定グラフによるモデル生成木の刈込み
- 二分決定グラフによるモデル生成木の刈込み
- 帰納論理プログラミングを用いたTwitterからのルール抽出(「コンテキストを意識した知識の利用」及び一般)
- 帰納論理プログラミングを用いた Twitter からのルール抽出