ログイン 新規登録
言語:

WEKO3

  • トップ
  • ランキング
To
lat lon distance
To

Field does not validate



インデックスリンク

インデックスツリー

メールアドレスを入力してください。

WEKO

One fine body…

WEKO

One fine body…

アイテム

  1. 論文誌(ジャーナル)
  2. Vol.44
  3. No.6

振舞い近似手法を用いたステートチャートに対する不変性の検証

https://ipsj.ixsq.nii.ac.jp/records/11200
https://ipsj.ixsq.nii.ac.jp/records/11200
8164683b-1737-430f-b2ed-b30e9301b0ff
名前 / ファイル ライセンス アクション
IPSJ-JNL4406003.pdf IPSJ-JNL4406003.pdf (237.2 kB)
Copyright (c) 2003 by the Information Processing Society of Japan
オープンアクセス
Item type Journal(1)
公開日 2003-06-15
タイトル
タイトル 振舞い近似手法を用いたステートチャートに対する不変性の検証
タイトル
言語 en
タイトル Behavior Approximation Method for Verifying Invariant on Statecharts
言語
言語 jpn
キーワード
主題Scheme Other
主題 特集:オブジェクト指向技術
資源タイプ
資源タイプ識別子 http://purl.org/coar/resource_type/c_6501
資源タイプ journal article
その他タイトル
その他のタイトル 形式的仕様
著者所属
日本IBM東京基礎研究所
著者所属
北陸先端科学技術大学院大学/科学技術振興事業団さきがけ研究21
著者所属
北陸先端科学技術大学院大学
著者所属(英)
en
IBM Tokyo Research Laboratory
著者所属(英)
en
Japan Advanced Institute of Science and Technology/PRESTO, Japan Science and Technology Corporation
著者所属(英)
en
Japan Advanced Institute of Science and Technology
著者名 立石, 孝彰 青木, 利晃 片山, 卓也

× 立石, 孝彰 青木, 利晃 片山, 卓也

立石, 孝彰
青木, 利晃
片山, 卓也

Search repository
著者名(英) Takaaki, Tateishi Toshiaki, Aoki Takuya, Katayama

× Takaaki, Tateishi Toshiaki, Aoki Takuya, Katayama

en Takaaki, Tateishi
Toshiaki, Aoki
Takuya, Katayama

Search repository
論文抄録
内容記述タイプ Other
内容記述 本稿では,互いに依存する複数のステートチャートを合成することなく不変性 の検証を行う手法を示す. 単一のステートチャートの検証では,まず最初に与えられたステートチャート をステートチャートに対する正規表現に変換する.そして,本稿で提案する形 式的体系を用いて,Hoareのプログラム検証手法と同じ方法を用いて不変性に関する検証を行う. 振舞いが互いに依存する複数のステートチャートの検証においては,通常は合 成と呼ばれる手法が用いられる.しかし,状態爆発などの問題を起こすため, 本稿では合成後に得られるステートチャートの振舞いに徐々に近づける手法を 提案する.この方法は,目的とする検証が行えるようになるまで何度でも適用 できる. また,ステートチャートどうしの通信方法には様々ある.ステートチャートが どのように協調動作するのかに応じて,ステートチャート間の通信方法を決め る必要がある. そこで,提案する手法では,通信方法に応じて柔軟に対応できるようにしてい る.
論文抄録(英)
内容記述タイプ Other
内容記述 In this paper, we propose a method for verifying invariant properties of statecharts without making the composition. We first convert a statechart to a regular expression to verify the given single statechart. We then verify it with the similar method to Hoare's program verification method. When verifying multiple statecharts which depend on the other, we make them to approximate composite behavior by repeating to apply a method we describe in this paper. The method can repeat to be applied until a target verification is completed. On the other hand, there are various communication mechanism between statecharts and we apply one of them considering how statecharts communicate with each other. Our method can be flexibly adapted to an applied communication mechanism.
書誌レコードID
収録物識別子タイプ NCID
収録物識別子 AN00116647
書誌情報 情報処理学会論文誌

巻 44, 号 6, p. 1448-1460, 発行日 2003-06-15
ISSN
収録物識別子タイプ ISSN
収録物識別子 1882-7764
戻る
0
views
See details
Views

Versions

Ver.1 2025-01-23 02:21:33.747876
Show All versions

Share

Mendeley Twitter Facebook Print Addthis

Cite as

エクスポート

OAI-PMH
  • OAI-PMH JPCOAR
  • OAI-PMH DublinCore
  • OAI-PMH DDI
Other Formats
  • JSON
  • BIBTEX

Confirm


Powered by WEKO3


Powered by WEKO3