文献

J-GLOBAL ID：201102221356406385   整理番号：11A0128920

統合開発環境によるLMNtalモデル検査

LMNtal Model Checking using an Integrated Development Environment

著者 (5件)： 綾野貴之 (早稲田大学大学院基幹理工学研究科情報理工学専攻) ,  堀泰祐 (早稲田大学大学院基幹理工学研究科情報理工学専攻) ,  岩澤宏希 (早稲田大学大学院基幹理工学研究科情報理工学専攻) ,  小川誠司 (早稲田大学大学院基幹理工学研究科情報理工学専攻) ,  上田和紀 (早稲田大学理工学術院情報理工学科)
資料名： コンピュータソフトウェア  (Computer Software)
巻： 27  号： 4  ページ： 4.197-4.214 (J-STAGE)  発行年： 2010年 
JST資料番号： Y0628A  ISSN： 0289-6540  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： 日本 (JPN)  言語： 日本語 (JA)

抄録/ポイント： LMNtalは階層グラフ書換えに基づく統合計算モデルとして設計され発展してきたが,我々は新たにLMNtalの検証および探索分野への応用を目指して,LMNtalをモデリング言語とするモデル検査器を構築し,モデリングと検証の経験を蓄積している.本論文では,状態空間探索や検証の可視化機能を備えた統合開発環境LMNtalEditorとそれを利用したモデル記述例,動作例,可視化例を紹介する.新たに構築したLMNtalEditorは,全状態空間や反例の可視化とブラウジング機能や,特定の条件を満たす状態の検索機能などを備えている.並行計算やAI探索問題を含む多様な例題をLMNtalEditor上で実行することで,本統合環境がモデルや反例の理解に重要な役割を果たし,検証作業の効率を大幅に高めることが確認できた.またPromela, MSR, Coloured Petri Netなどのモデリング言語による記述のLMNtalへの変換実験を通じて,LMNtalの表現力がカバーする範囲を検証分野に拡大することができた.(著者抄録)

シソーラス用語： *モデル検査 ,  項書換え系 ,  *プログラミング環境 ,  応用向き言語 ,  可視化 ,  ブラウジング ,  探索問題 ,  並列演算 ,  人工知能 ,  階層構造 ,  構文分析 ,  状態遷移図 ,  *仕様記述言語
準シソーラス用語： 統合開発環境 ,  グラフ書換え ,  モデリング言語

分類 (1件)： 計算機システム開発  (JD02010R)

タイトルに関連する用語 (2件)： 統合開発環境 ,  モデル検査