LMNtal実行時処理系の並列モデル検査器への発展
書誌事項
- タイトル別名
-
- Evolution of the LMNtal Runtime to a Parallel Model Checker
抄録
Model checking is a verification technique based on the exhaustive search of erroneous behaviors of state transition systems, which is attracting growing interest. The LMNtal language allows us to represent state transition systems using hierarchical graph rewriting, and its runtime system, SLIM, has recently evolved into an explicit-state model checker. Hierarchical graphs are a powerful data structure that features a builtin symmetry reduction mechanism that plays a key role in state space search. However, model checking is still prone to state space explosion and has called for time- and space-efficient methods for state management. To address this problem and make our model checker more useful, we have extended the SLIM runtime further to a parallel model checker to run on shared-memory multiprocessors and developed various optimization techniques of state management. These two enhancements drastically improved the scale of problems the LMNtal model checker can handle as well as its performance.
収録刊行物
-
- コンピュータ ソフトウェア
-
コンピュータ ソフトウェア 28 (4), 137-157, 2011
日本ソフトウェア科学会
- Tweet
詳細情報 詳細情報について
-
- CRID
- 1390282679714536320
-
- NII論文ID
- 130004549234
-
- ISSN
- 02896540
-
- データソース種別
-
- JaLC
- CiNii Articles
- KAKEN
-
- 抄録ライセンスフラグ
- 使用不可