異なる形式手法を用いて検査されたサービスの合成結果の検証

• Item type: SIG Technical Reports(1)
• 公開日: 2014-07-21
• タイトル: 異なる形式手法を用いて検査されたサービスの合成結果の検証
• タイトル / 言語: en
• タイトル: Formal verification for service composition of formaly verified services using different mechanisms
• 言語: jpn
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_18gh
• 資源タイプ: technical report
• 著者所属: 日本電気株式会社情報・ナレッジ研究所
• 著者所属: 日本電気株式会社情報・ナレッジ研究所
• 著者所属(英): en
• 著者所属(英): NEC Corporation
• 著者所属(英): en
• 著者所属(英): NEC Corporation
• 著者名: 船越, 和大; 細野, 繁
• 著者名(英): Kaz, Funakoshi; Shigeru, Hosono
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 複数の形式手法を用いてそれぞれ検査されたサービスのモデルとその制約を示す論理式を入力とし，定理証明支援系である Coq 上のモデルと証明したい論理式に変換する方法と，合成サービスの検査方法について述べる．形式手法に基づくサービスやビジネスプロセスの検証事例が増えており，その検査手法もそれぞれ異なる．しかし，異なる手法による検証は，各サービスの検証結果に対する再利用を妨げる要因となっている．そこで，異なる手法により検証されたサービスから構成される，合成サービスを検査するための技術が重要となる．本発表では具体例を用いて Event－B および SPIN で検査されたサービスを合成し，その性質の検査方法を示す．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: This presentation describes a case study to generate models on proof assistant Coq with input of multiple Web services' models which are verified in different methodologies. In recent days, formally verified services or business processes are highlighted. However, they are verified in different ways which prevent generating formally verified composite Web services rather than composite verified Web services. It is crucial that the verification of service composition of existing verified services in different approaches. In this case study, presenter reports a small example to verify a service composition of services verified in Event-B and SPIN/Promela.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11838947
• 書誌情報: 研究報告ユビキタスコンピューティングシステム（UBI）; 巻 2014-UBI-43, 号 9, p. 1-6, 発行日 2014-07-21
• Notice: SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc.
• 出版者 / 言語: ja
• 出版者: 情報処理学会