@techreport{oai:ipsj.ixsq.nii.ac.jp:00226853,
 author = {青木, 善貴 and 小形, 真平 and 中川, 博之 and 小林, 一樹 and Yoshitaka, Aoki and Shinpei, Ogata and Hiroyuki, Nakagawa and Kazuki, Kobayashi},
 issue = {27},
 month = {Jul},
 note = {モデル検査は，複雑な相互作用をもつシステムの性質を検証に有効である．NuSMV や SPIN などのモデル検査器はそういった複雑なモデルの振る舞いの検証には適しているが，時間的な考慮が必要な検証をすることはできない．本稿では，モデル検査器の NuSMV と時間を扱えるモデル検査器 PRISM を併用することにより，複雑な相互作用をもつモデルに，時間的な考慮を入れた検証ができる手法を提案する．, 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.},
 title = {二種類のモデル検査器を用いたシステムの振る舞いの検証の試み},
 year = {2023}
}