@techreport{oai:ipsj.ixsq.nii.ac.jp:00211806,
 author = {井, 浩也 and 大戸, 柾之介 and 桐生, 仁司 and 小形, 真平 and 岡野, 浩三 and Hiroya, Ii and Masanosuke, Ohto and Hitoshi, Kiryu and Shinpei, Ogata and Kozo, Okano},
 issue = {6},
 month = {Jul},
 note = {ソフトウェア開発において，ソフトウェアの要求を厳密に記述した要求仕様書を用いて開発が進められることがある．要求仕様書の記述には，自然言語のようなテキスト表現が用いられることが通常であるが，自然言語には曖昧さを含んでいる可能性がある．また，ソフトウェア開発では，要求通りのシステムを作成できているか確認することができるのはテスト工程であり，テスト工程で問題が発生すると開発工程まで手戻りする必要がある．この手戻りが要するコストは大きく，できる限りこの手戻りを少なくするための様々なソフトウェアの開発手法が提案されている．この手戻りを防ぐためには，自然言語で記述された要求仕様書から曖昧性や矛盾を開発工程で発見し，取り除く必要がある．解決案の一つとして，開発するシステムが要求を満たしているかを検証する手法としてモデル検査 がある．モデル検査を行うためには，状態変数，変数値などの情報が記述された遷移モデルを必要とする．しかし，遷移モデルを作成し，モデル検査を行うには専門的な知識が必要であるため，一般の技術者には難しいとされている．そのため，仕様記述からモデルを自動生成する技術はソフトウェア開発において有効な技術であると考えられる．本報告では，遷移モデルの自動導出を考慮した要求仕様書の記述方法とそこからの状態遷移モデルの導出方法を提案する．要求仕様書から本提案記述法に何らかの形で変換できればあとは遷移モデルを自動生成できることを想定している．本報告では提案方法を実際に話題沸騰ポットの仕様記述に対して適用した結果についても報告する．, In software development, a requirements specification, which is a strict description of software requirements, is sometimes used for development. Although textual expressions such as natural languages are usually used to describe the requirements, natural languages may contain ambiguities. In addition, in software development, The testing process is to make sure that the system is built according to the requirements. If a problem occurs in the testing process, it is necessary to go back to the development process. The cost of this rework is significant, therefore various software development methods have been proposed to minimize this rework as much as possible. In order to prevent such rework, it is necessary to find and remove ambiguities and inconsistencies from the requirements specification written in a natural language during the development process. One of the solutions is model checking, which is a method to verify whether the system to be developed according to the requirements. In order to perform model checking, a transition model that describes information such as state variables and variable values is required. However, it is considered difficult for general engineers to create transition models and perform model checking because it requires specialized knowledge. Therefore, a technology to automatically generate models from specification descriptions is considered to be an effective method in software development. In this report, we propose a method of describing requirement specifications and a method of deriving state transition models from them, taking into account the automatic derivation of transition models. It is assumed that the transition model can be generated automatically if the requirements specification can be converted to the proposed method in some way. We also report the results of applying the proposed method to the specification description of an electrical hot pot provided by Sessame.},
 title = {遷移モデル自動導出を考慮した要求仕様書と導出方法の提案},
 year = {2021}
}