UPPAAL拡張時間オートマトンの反例に基づく抽象化改良ループによるモデル抽象化手法

長岡, 武志; 岡野, 浩三; 楠本, 真二

電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス, 2007, 107(176), 77-82

Number of Access:521（2025-09-04 14:41 Counts）

Identifier to cite or link to this item: https://hdl.handle.net/11094/27441

Link to primary information 

File Format Terms of use Size Views Date.Available Description information
itr107_176_077 pdf None 745 KB 97 2014.04.11  

Item Information

Output File Export EndNote Basic Export Mendeley

Title
UPPAAL拡張時間オートマトンの反例に基づく抽象化改良ループによるモデル抽象化手法
Abstraction of Extended Timed Automata for UPPAAL Based on Counterexample-Guided Abstraction Refinement Loop
UPPAAL 　カクチョウ　ジカン　オートマトン　ノ　ハンレイ　ニ　モトヅク　チュウショウカ　カイリョウ　ループ　ニ　ヨル　モデル　チュウショウカ　シュホウ
Creator
CreatorName
長岡, 武志 ; ナガオカ, タケシ ; Nagaoka, Takeshi
NRID
1000070252632 1000070252632
CreatorName
岡野, 浩三 ; オカノ, コウゾウ ; Okano, Kozo
NRID
1000030234438 1000030234438
researchmap permalink
read0013799 read0013799
Scopus Author ID
7102741360 7102741360
CreatorName
楠本, 真二 ; クスモト, シンジ ; Kusumoto, Shinji
Subject
モデル検査
時間オートマトン
モデル抽象化
CEGAR
UPPAAL
Model Checking
Timed Automata
Model Abstraction
Abstract
近年,情報システムの高信頼設計においてモデル検査は重要な役割を果たすようになってきている.実時間システムのモデル検査では,モデルの状態数が状態変数やクロック変数に対して指数的に増加し,スケーラビリティに厳しい制限が生じる.本稿では,時間モデル検査ツールであるUPPAALで用いられる拡張時間オートマトンに対する具体的なモデル抽象化手法を提案する.モデル抽象化技法はこのスケーラビリティ改善のための主要な手法として注目を浴びている.本手法では,Clarkeらが提案した反例に基づいた抽象化改良ループCEGARを適用しており,抽象化から検査までの全ての工程を自動的に行うことが可能である.また,反例によるモデルの再抽象化においては時間オートマトンの検証で用いられるデータ構造DBMを活用する工夫を行なっている.
In the model checking of the realtime systems, the number of states of models increases exponentlly with the number of the state variables and the clock variables. Such explosion severely limits the scalability of model checking. This paper proposes a concrete model abstraction technique for extended timed automata used in UPPAAL, a famous model checking tool for realtime systems. In the proposed technique, the abstraction refinement loop based on the counterexample that Clarke et al. proposed is applied, and all the processes from the abstraction can be performed automatically. We gives concrete procedures for the abstraction loop with utilization of DBM.
Publisher
電子情報通信学会
The Institute of Electronics, Information and Communication Engineers
デンシ　ジョウホウ　ツウシン　ガッカイ
Source Title
電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス
Volume (Issue)
107(176)
Page
77-82
Date of Issued
2007-07-26
Language
Japanese
Handle URL
https://hdl.handle.net/11094/27441
PISSN
09135685
NCID
AN10013287
Access Rights
open access
CopyRight
Copyright © 2007 IEICE
本文データはCiNiiから複製したものである
oaire:version
Version of Record
Category
学術雑誌論文 Journal Article