| Item type |
SIG Technical Reports(1) |
| 公開日 |
2023-07-13 |
| タイトル |
|
|
タイトル |
二種類のモデル検査器を用いたシステムの振る舞いの検証の試み |
| タイトル |
|
|
言語 |
en |
|
タイトル |
Verification of System Behavior using two types of model checking |
| 言語 |
|
|
言語 |
jpn |
| 資源タイプ |
|
|
資源タイプ識別子 |
http://purl.org/coar/resource_type/c_18gh |
|
資源タイプ |
technical report |
| 著者所属 |
|
|
|
BIPROGY株式会社 |
| 著者所属 |
|
|
|
信州大学 |
| 著者所属 |
|
|
|
大阪大学 |
| 著者所属 |
|
|
|
信州大学 |
| 著者所属(英) |
|
|
|
en |
|
|
BIPROGY Inc. |
| 著者所属(英) |
|
|
|
en |
|
|
Shinshu University |
| 著者所属(英) |
|
|
|
en |
|
|
Osaka University |
| 著者所属(英) |
|
|
|
en |
|
|
Shinshu University |
| 著者名 |
青木, 善貴
小形, 真平
中川, 博之
小林, 一樹
|
| 著者名(英) |
Yoshitaka, Aoki
Shinpei, Ogata
Hiroyuki, Nakagawa
Kazuki, Kobayashi
|
| 論文抄録 |
|
|
内容記述タイプ |
Other |
|
内容記述 |
モデル検査は，複雑な相互作用をもつシステムの性質を検証に有効である．NuSMV や SPIN などのモデル検査器はそういった複雑なモデルの振る舞いの検証には適しているが，時間的な考慮が必要な検証をすることはできない．本稿では，モデル検査器の NuSMV と時間を扱えるモデル検査器 PRISM を併用することにより，複雑な相互作用をもつモデルに，時間的な考慮を入れた検証ができる手法を提案する． |
| 論文抄録(英) |
|
|
内容記述タイプ |
Other |
|
内容記述 |
In recent years, with the development of interfaces, the number of systems that interact closely with humans has increased. With the development of networks, multimodal user interfaces have been developed. Conflicts in the operation of multiple interfaces can lead system behavior that is contrary to human expectation, and the behavior may cause serious accidents. Model checking is effective in verifying properties of systems with complex interactions. Model checkers such as NuSMV and SPIN are suitable for verifying the behavior of such complex models, but they cannot perform time-sensitive verifications. In this paper, we propose a verification method that considers time for models with complex interactions by using both NuSMV, a model checker, and PRISM, a model checker that can handle time. |
| 書誌レコードID |
|
|
収録物識別子タイプ |
NCID |
|
収録物識別子 |
AN10112981 |
| 書誌情報 |
研究報告ソフトウェア工学（SE）
巻 2023-SE-214,
号 27,
p. 1-6,
発行日 2023-07-13
|
| ISSN |
|
|
収録物識別子タイプ |
ISSN |
|
収録物識別子 |
2188-8825 |
| Notice |
|
|
|
SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc. |
| 出版者 |
|
|
言語 |
ja |
|
出版者 |
情報処理学会 |
IPSJ-SE23214027.pdf (1.3 MB)
