文献

J-GLOBAL ID：201002239911464131   整理番号：10A0979439

LMNtal実行時処理系の並列モデル検査器への展開

著者 (3件)： 後町将人 (早稲田大 大学院基幹理工学研究科) ,  堀泰祐 (早稲田大 大学院基幹理工学研究科) ,  上田和紀 (早稲田大 理工学術院)
資料名： 日本ソフトウェア科学会大会講演論文集(CD-ROM)  (日本ソフトウエア科学会大会講演論文集(CD-ROM))
巻： 27th  ページ： ROMBUNNO.3B-1  発行年： 2010年 
JST資料番号： X0080B  ISSN： 1348-0901  資料種別： 会議録 (C)
記事区分： 短報  発行国： 日本 (JPN)  言語： 日本語 (JA)

抄録/ポイント： システム検証技術であるモデル検査は,状態遷移系として表現したシステムの振舞いから不具合の探索を網羅的に行う技術として注目を集めている。階層グラフ書換えに基づく状態遷移系記述言語LMNtalは,実行時処理系SLIMを拡張する形でモデル検査器へと発展してきた。階層グラフ構造は,状態空間探索において重要となる対称性吸収メカニズムを備えた強力なデータ構造であるが,それでもなおモデル検査は状態空間爆発によるメモリ使用量と検証時間の爆発的な増加を招きやすく,時間と空間の両面で効率的な状態管理方式を必要としていた。この問題に対処して検証機能としての有用性を高めるべく,我々は共有メモリ環境を対象にした並列モデル検査器への拡張と新たな状態管理手法の開発に取り組み,LMNtalをモデル記述言語としたモデル検査の検証規模拡大と高速化を実現した。(著者抄録)

シソーラス用語： *モデル検査 ,  *並列処理 ,  状態遷移図 ,  項書換え系 ,  *システム記述言語 ,  共有メモリ ,  管理 ,  状態 ,  規模 ,  高速化
準シソーラス用語： グラフ書換え ,  状態管理 ,  *並列モデル検査器

分類 (3件)： 計算理論  (JB02000A) ,  ディジタル計算機方式一般  (JC02010O) ,  応用プログラミング言語  (JD03052Y)

タイトルに関連する用語 (2件)： モデル検査 ,  展開