【IT】状態遷移表モデル設計だけでモデル検査技術の利用を可能にする次世代モデルベース開発
1 ：科学ニュース＋記者募集中です＠pureφ ★：
キャッツ、九州大学などと状態遷移表モデル検査技術の共同研究を実施
次世代モデルベース開発で急速に注目されている形式検証／モデル検査技術の共同研究を
キャッツ、九州大学、ＦＬＥＥＴＳで実施！
－状態遷移表モデル検査技術の研究成果をＥＳＥＣ２００５で発表！
キャッツ株式会社（社長・上島康男、横浜市港北区）、九州大学、財団法人福岡県産業・
科学技術振興財団は、次世代のモデルベース開発に画期的な効果を発揮すると期待される
状態遷移表モデル検査技術（形式手法／モデル検査技術）の共同研究を行う事を発表した。
★状態遷移表モデル検査技術とは
状態遷移表モデル検査技術とは、状態遷移表モデルで特定の性質を満たすかどうかを検
査し数理的に証明することができる技術です。この技術はシステム開発の上流工程（仕様・
設計）に潜在する論理的な矛盾やバグの原因を排除することに効果を発揮し、従来から行わ
れてきた人手／経験／膨大な試験工数による信頼性確保の問題に対しての画期的な効果を
発揮することが実証されています。また、この技術は従来の形式検証はＺやＶＤＭ、ＳＰＩＮに
代表される形式仕様言語を利用しないと数理証明（保証）が難しく適用ハードルが高いもので
したが、この技術は状態遷移表モデルを設計する事だけでモデル検査技術を利用することを
可能にした大きな研究成果です。
★状態遷移表モデル検査技術の研究成果（検査ツール）をＥＳＥＣ２００５で参考出展！
モデル検査技術（Ｍｏｄｅｌ Ｃｈｅｃｋｉｎｇ）の研究成果としての状態遷移表検査ツールとＴ－
Ｅｎｇｉｎｅをベースにした開発事例（行き先表示板）を２００５年６月２９（水）～７月１日（金）に開
催されるＥＳＥＣ２００５（第８回組込みシステム開発技術展）のキャッツ株式会社ブース及び
財団法人福岡県産業・科学技術振興財団ブースに参考出展いたします。
★状態遷移表とは
状態遷移表は組込みシステムをモレヌケ無くモデリングすることができる表記法として、組込
みシステムの開発メーカーから高い評価を得ている、キャッツの主力製品のコアとなる表記法
です。(略)
プレスリリース全文はこちらです。
日経プレスリリース 2005/06/24
http://release.nikkei.co.jp/detail.cfm?relID=103672&lindID=1
第８回組込みシステム開発技術展ＥＳＥＣ２００５ ２００５年６月２９（水）～７月１日（金）
http://www.esec.jp/
依頼 http://news18.2ch.net/test/read.cgi/scienceplus/1118578184/56
次世代モデルベース開発で急速に注目されている形式検証／モデル検査技術の共同研究を
キャッツ、九州大学、ＦＬＥＥＴＳで実施！
－状態遷移表モデル検査技術の研究成果をＥＳＥＣ２００５で発表！
キャッツ株式会社（社長・上島康男、横浜市港北区）、九州大学、財団法人福岡県産業・
科学技術振興財団は、次世代のモデルベース開発に画期的な効果を発揮すると期待される
状態遷移表モデル検査技術（形式手法／モデル検査技術）の共同研究を行う事を発表した。
★状態遷移表モデル検査技術とは
状態遷移表モデル検査技術とは、状態遷移表モデルで特定の性質を満たすかどうかを検
査し数理的に証明することができる技術です。この技術はシステム開発の上流工程（仕様・
設計）に潜在する論理的な矛盾やバグの原因を排除することに効果を発揮し、従来から行わ
れてきた人手／経験／膨大な試験工数による信頼性確保の問題に対しての画期的な効果を
発揮することが実証されています。また、この技術は従来の形式検証はＺやＶＤＭ、ＳＰＩＮに
代表される形式仕様言語を利用しないと数理証明（保証）が難しく適用ハードルが高いもので
したが、この技術は状態遷移表モデルを設計する事だけでモデル検査技術を利用することを
可能にした大きな研究成果です。
★状態遷移表モデル検査技術の研究成果（検査ツール）をＥＳＥＣ２００５で参考出展！
モデル検査技術（Ｍｏｄｅｌ Ｃｈｅｃｋｉｎｇ）の研究成果としての状態遷移表検査ツールとＴ－
Ｅｎｇｉｎｅをベースにした開発事例（行き先表示板）を２００５年６月２９（水）～７月１日（金）に開
催されるＥＳＥＣ２００５（第８回組込みシステム開発技術展）のキャッツ株式会社ブース及び
財団法人福岡県産業・科学技術振興財団ブースに参考出展いたします。
★状態遷移表とは
状態遷移表は組込みシステムをモレヌケ無くモデリングすることができる表記法として、組込
みシステムの開発メーカーから高い評価を得ている、キャッツの主力製品のコアとなる表記法
です。(略)
プレスリリース全文はこちらです。
日経プレスリリース 2005/06/24
http://release.nikkei.co.jp/detail.cfm?relID=103672&lindID=1
第８回組込みシステム開発技術展ＥＳＥＣ２００５ ２００５年６月２９（水）～７月１日（金）
http://www.esec.jp/
依頼 http://news18.2ch.net/test/read.cgi/scienceplus/1118578184/56
|
|
|
2 ：名無しのひみつ：2005/06/26(日) 21:58:01 ID:fvjIDGUl
解る？意味。
3 ：科学ニュース＋記者募集中です＠pureφ ★：2005/06/26(日) 22:01:00 ID:???
>>2
さっぱり(^_^;)
さっぱり(^_^;)
4 ：名無しのひみつ：2005/06/26(日) 22:01:38 ID:XQ/zh1IN
単にグラフを探索するだけだろ。研究成果と発表すべき新規研究ではない。
UMLはどうしちゃったんだ？
日経だからか
日経だからか
6 ：名無しのひみつ：2005/06/26(日) 22:15:19 ID:XQ/zh1IN
UMLは意思疎通伝達言語であって、このソフトウエアと直接は関係ないよ。
組み込み系で最近UMLコンパイラに食わすんじゃないの？
いまさらCASE？って感じです
いまさらCASE？って感じです
8 ：名無しのひみつ：2005/06/26(日) 23:07:12 ID:XQ/zh1IN
>>8
会った事あるかもね
会った事あるかもね
10 ：名無しのひみつ：2005/06/26(日) 23:29:46 ID:LVcIw812
誰わかりやすく解説してくり。
11 ：名無しのひみつ：2005/06/26(日) 23:59:26 ID:XQ/zh1IN
この文章自体は大した用語使ってないけど…
>>7 の言っているように単なるCASEツール（ぐぐれ）に毛が
生えた感じ。
うちのソフトウエア使えばプロジェクトのに起こりえる問題が
みんな回避できるよ！
というプロパガンダ。
いずれにしてもこの種の分野は、実力が無いのに上流行程のみ
だけやって旨みを吸おうと思っている大企業や似非コンサル会社
の連中の強迫観念を煽ってお金を引き出そうとしているだけ。
一般人や勉強し始めの人や忙しい人は無視していて良い。つうか
そのうち似たようなものがUMLに取り込まれる（ちょっとその気配
はある）ので関わるだけ無駄。
>>7 の言っているように単なるCASEツール（ぐぐれ）に毛が
生えた感じ。
うちのソフトウエア使えばプロジェクトのに起こりえる問題が
みんな回避できるよ！
というプロパガンダ。
いずれにしてもこの種の分野は、実力が無いのに上流行程のみ
だけやって旨みを吸おうと思っている大企業や似非コンサル会社
の連中の強迫観念を煽ってお金を引き出そうとしているだけ。
一般人や勉強し始めの人や忙しい人は無視していて良い。つうか
そのうち似たようなものがUMLに取り込まれる（ちょっとその気配
はある）ので関わるだけ無駄。
>>11
この研究はもっと抽象的で泥臭い話だよ
この研究はもっと抽象的で泥臭い話だよ
13 ：名無しのひみつ：2005/06/27(月) 00:07:45 ID:dHSer+RY
ぐぐってみたら、キャッツってUML→ハード（SystemC）やってんのね。
（シロアリ退治のキャッツとは違うのね）
（シロアリ退治のキャッツとは違うのね）
16 ：名無しのひみつ：2005/06/27(月) 00:30:56 ID:1i17rN/q
>>12
そうだね。従来のCASEツールよりは毛が生えた、というより
は抽象的、といった方がいいか。泥臭いかは捕らえ方による。
結局はツール使う人が泥臭い重み付けをして危険度を計らな
きゃならんわけだ。
そうだね。従来のCASEツールよりは毛が生えた、というより
は抽象的、といった方がいいか。泥臭いかは捕らえ方による。
結局はツール使う人が泥臭い重み付けをして危険度を計らな
きゃならんわけだ。
17 ：11 16：2005/06/27(月) 01:57:14 ID:1i17rN/q
>>11はちょっと勘違いだった。すまん。
どうやら本当に組込み分野のみ対応か。
そりゃ完全に泥臭い分野だったな。
遷移表から抜けパスを炙り出すのは結構
昔からあるような。色々名を変え品を変
え宣伝大変だね。
どうやら本当に組込み分野のみ対応か。
そりゃ完全に泥臭い分野だったな。
遷移表から抜けパスを炙り出すのは結構
昔からあるような。色々名を変え品を変
え宣伝大変だね。
18 ：名無しのひみつ：2005/06/27(月) 02:12:06 ID:GDMhwHO5
これってただのニュースリリースってだけの話じゃんか。
最近増えている状態遷移を知らん技術者には猫に小判で役に立たないし、
そうでない技術者にとってはこの手のトイツールは役にたたないってのがオチかと。
最近増えている状態遷移を知らん技術者には猫に小判で役に立たないし、
そうでない技術者にとってはこの手のトイツールは役にたたないってのがオチかと。
19 ：名無しのひみつ：2005/06/27(月) 05:07:00 ID:8JHK+hmf
ソフトウェア分野で状態遷移ベースといえば、シャロー/メラー手法あたりか。
要するにMDAの起源の一つだ。
ハードウェア分野で状態遷移ベースといえば・・・山のようにあるよな？
AlteraやXiLinxの製品で回路設計して、膨大な時間をかけて自動検証してるのも、
たぶんタイミングと状態遷移の検証だよな？
キャッツといえば富士通と共に、UMLでモデリングしてSpecCかSystemCのコードを生成してLSI設計する
という技術のコンソーシアムを作ってたけど、あれどうなったの？
いわゆる、活きのいいベンチャーなのだろうし、
書籍「動的モデルによる組込み開発」も入門書として面白いと思ったけど、
ちょっと何をやっているのかわからない
要するにMDAの起源の一つだ。
ハードウェア分野で状態遷移ベースといえば・・・山のようにあるよな？
AlteraやXiLinxの製品で回路設計して、膨大な時間をかけて自動検証してるのも、
たぶんタイミングと状態遷移の検証だよな？
キャッツといえば富士通と共に、UMLでモデリングしてSpecCかSystemCのコードを生成してLSI設計する
という技術のコンソーシアムを作ってたけど、あれどうなったの？
いわゆる、活きのいいベンチャーなのだろうし、
書籍「動的モデルによる組込み開発」も入門書として面白いと思ったけど、
ちょっと何をやっているのかわからない
それはそれとして。
>>11はかなり無茶苦茶なレスだな。
＞ そのうち似たようなものがUMLに取り込まれる（ちょっとその気配はある）
こりゃなんだ？状態遷移モデルならUMLに最初から入ってるよ。
UMLの状態遷移モデルに基づくコード生成も、MDAの前からあるよ。
>>11はかなり無茶苦茶なレスだな。
＞ そのうち似たようなものがUMLに取り込まれる（ちょっとその気配はある）
こりゃなんだ？状態遷移モデルならUMLに最初から入ってるよ。
UMLの状態遷移モデルに基づくコード生成も、MDAの前からあるよ。
21 ：名無しのひみつ：2005/06/27(月) 05:40:58 ID:r/MViMvp
次世代モビルスーツを開発かぁ…
22 ：名無しのひみつ：2005/06/27(月) 06:04:19 ID:EIRq1cIT
状態遷移図のチェックをしてくれるようなもんですか？
「モデル検査技術」って何？
24 ：11：2005/06/27(月) 11:33:04 ID:oCp/Tr8h
>>20
無理なレスで正解。ニュースサイトで宣伝するならともかく、
２chで宣伝するなよ、って意見で書いたからこんな文になった。
>こりゃなんだ？状態遷移モデルならUMLに最初から入ってるよ。
>UMLの状態遷移モデルに基づくコード生成も、MDAの前からあるよ。
状態遷移モデルが無いなんて言ってないけど。コード生成も
そんなのはどこぞのfreeのソフトでも実装されてるのもわかってる。
生成する方はオートマトンの延長だからそんなに難しくは無いだろ。
>>22 のようにチェック技術を取り込んだソフトもあるの？
って意味で書いたつもりだったんだけど。ちぇっくするのも
オートマトンの延長だけど、作る方は仕様の決定が大変そうだ。
ユーザーに結果表を先に作らせて、すべて辿れるかをチェックする
仕組みになるわけだ。テストファーストと一緒だな。
まあ組み込みで使うんだったら、抜け道を完璧に埋めなくては
商品回収になりかねん。
ハード屋さん・命・金が直接掛かってるやつは死ぬ気で頑張れ。
俺はパッチ出して情報流しとけばいい、中途半端な立場だから
他人事だけど。
無理なレスで正解。ニュースサイトで宣伝するならともかく、
２chで宣伝するなよ、って意見で書いたからこんな文になった。
>こりゃなんだ？状態遷移モデルならUMLに最初から入ってるよ。
>UMLの状態遷移モデルに基づくコード生成も、MDAの前からあるよ。
状態遷移モデルが無いなんて言ってないけど。コード生成も
そんなのはどこぞのfreeのソフトでも実装されてるのもわかってる。
生成する方はオートマトンの延長だからそんなに難しくは無いだろ。
>>22 のようにチェック技術を取り込んだソフトもあるの？
って意味で書いたつもりだったんだけど。ちぇっくするのも
オートマトンの延長だけど、作る方は仕様の決定が大変そうだ。
ユーザーに結果表を先に作らせて、すべて辿れるかをチェックする
仕組みになるわけだ。テストファーストと一緒だな。
まあ組み込みで使うんだったら、抜け道を完璧に埋めなくては
商品回収になりかねん。
ハード屋さん・命・金が直接掛かってるやつは死ぬ気で頑張れ。
俺はパッチ出して情報流しとけばいい、中途半端な立場だから
他人事だけど。
25 ：名無しのひみつ：2005/06/27(月) 14:45:09 ID:GDMhwHO5
ベテランほど状態遷移を意識した設計をしたりするが、
後に仕様追加などで若手がいぢってめちゃくちゃになる
というのがありがちなパターンかと。
後に仕様追加などで若手がいぢってめちゃくちゃになる
というのがありがちなパターンかと。
26 ：名無しのひみつ：2005/06/28(火) 19:15:57 ID:BaAyVwGP
27 ：24：2005/06/28(火) 23:18:07 ID:trb/wvwf
>>19 26
なるほど、簡単に膨れ上がる状態遷移を上手に押さえ込むノウハウ
があるわけですね。
中途半端にアルゴリズムとデザインパターンと知ってる程度じゃ
まだまだだとわかりました。もう少しまじめにオブジェクト指向
とMDAを勉強してみることにします(´･ω･`)ｼｮﾎﾞﾝ。
なるほど、簡単に膨れ上がる状態遷移を上手に押さえ込むノウハウ
があるわけですね。
中途半端にアルゴリズムとデザインパターンと知ってる程度じゃ
まだまだだとわかりました。もう少しまじめにオブジェクト指向
とMDAを勉強してみることにします(´･ω･`)ｼｮﾎﾞﾝ。
28 ：名無しのひみつ：2005/06/29(水) 16:17:26 ID:2ykZwsmZ
29 ：名無しのひみつ：
何がなにやらさっぽり