おめぇら、形式的仕様記述について知ってる事を書け

だれかJMLって使ったことあります?

Java + Eiffelのassertion + VDM

みたいなもんらしいですが.

おまいら、セキュリティ仕様やデータ安全性の検証って、どうやってますか？
SSLプロトコルやらLinuxやら、はたまたEJBのセキュリティや仕様自体の曖昧さを、
形式仕様記述言語使って、実験的に検証した、とか聞くけど、どーなのよ？

VDMとかRAISE使うと出来るの？
ZやVDMじゃだめなんだろうね？

おまいらの情報、とっとと早く書けっ！！ほれほれっ

さもなきゃ形式仕様記述なんて、実用で使ってくれる所、滅多にないんだからさぁ

>>22
CafeOBJといえば学会でよくJAISTの人が発表してた。
なつかしいな。

LOTOSあげ

じっさいVDM++とか使えるん？

> ## 見たなぁ。
> ## 今あなたは、このファイルをエディタなりで見ていますね。
> ## そういう方には、ヘルプファイルの形式をお教えします。
> ## 頑張れば、自分専用のヘルプ情報にできます。
> ## コントロールキーの割当ての部分を変えるとか、Ｃの関数の仕様を
> ## ヘルプファイルに入れてしまうとか、そういうことをやって下さい。
> ## 大変だとは思いますが、頑張って作って下さい。
> ##
> ## 【ヘルプファイルの形式】
> ## 形式は、通常のMS-DOS標準テキストファイルである。
> ## 内容は、改頁コード(0CH)で区切られたページの集まりである。ひとつの
> ## ページは、ページ名、見出し行、本文、制御行からなり、見出し行、本文、
> ## 制御行はなくてもよい。
> ##
> ## <ヘルプファイル> ::＝ {<ページ>}
> ## <ページ> ::＝ <ページ名>{<見出し行>}{<本文>}{制御行}<改頁>
> ## <改頁> ::＝ 0CH
> ## <ページ名> ::＝ <検索対象ページ名>|<非検索対象ページ名>
> ## <検索対象ページ名> ::＝ <頁区切文字1><30文字以内の文字列><頁区切文字2>
... 以下略

以上, 新松のヘルプファイル先頭より。
後になってこの説明が BNF またはその variant だと知った。
ヘルプファイル自體は(簡易?)ハイパーテキスト形式であった
(さう言や K3 は當時簡易 SGML フォーマッタも作ってゐたとか)。
尚, このヘルプファイルの先頭部分は後の松からは削除された。
「巫山戯た事を書いて怪しからん」と苦情を言った(或は苦言を
呈したのか?)顧客が居たからだと何處かで讀んだ氣がする。
眞僞の程は知らない。
通りすがりにスレ汚しスマソ。沈んで來ます。

>>282 executable notation, executable documentation ってやつですね。

投稿台の冒険吸湿に最近入り浸ってたんだけど、
やつら未だに仕様奇術＝実装が可能だと信じ込んでるぞ。
実務的にはRational MDAの出現でFAなのに、チョト可哀想。

代数学を誰もが理解できるわけではないというこの現実から始めよう

助けてください。SOS
オカルト板で、バサバサ削除する削除人が
登場しています。こわいです。おそろしいです。SOS
http://qb2.2ch.net/test/read.cgi/sakud/1021962883/l50

>実務的にはRational MDAの出現でFAなのに、
この認識は実務レベルでもドキュソだと思うけど

>>298
どーでもいいけど。
じゃ、なんか提案してみて。

>>298
>>295は、「多少は実用的な MDAですら 『仕様＋スクリプト』で実装コード生成してる
のに、今更『仕様奇術＝実装』はねぇだろ」っつう意図で書いたんだが。

まさか・・・「MDAで仕様奇術＝実装が可能になった」とか「MDA実用的でｻｲｺｳ」とか
読み違えてるわけねぇよな(ﾜﾗ

いずれにせよ、より良き提案があれば、あなたの意見を受け付けます。
提案ができねぇようなら、さっさと氏ね

↑ちなみに、「氏ね」は「この場からサッサと立ち去れ」という意味の
　２ちゃん固有の煽り文句。生命を終了させろ、という意味とは違う

ましてや、実際のその言葉を口にした事は、これまで一度もない事は言うまでもない

ましてや、実際その言葉を口にした事は、これまで一度もない事は言うまでもない

実用レベルでつかっているとこあんの？

>>300
>>295のFAってどういう意味？
あと、>>299と>>300の「替わりになんか提案しろ」の論理が
よくわからんのですが…

>>304
ITU

形式的記述とはちょっと違うけど
プログラムの解析だか正当性の検査にデータフローを追うみたいなやり方ありませんでしたっけ。
まえどっかでチラッとそんな内容の本を見た記憶があるんだけど題名が思い出せないんです｡
Amazonでそれらしき単語入れてもヒットしないし。

>>305
ふりーえーじぇんと。

ま、ファイナルアンサーだと思うのだがな。
で、やつらは銀の弾丸を求めてるだけだからほっとけ。

あぼーん

↑頭の病気の人、とうとうこのスレにも進出してきたか。
　

>>308thx

キャッツの社長さんが書いたＵＭＬ動的モデルで組み込みモデリングの本、
なかなか面白そうですね。
システムＬＳＩ〜形式的手法の話まで触れていて、なかなか興味深いんで、早速買いました。。。
って、この本、１年前に発売されてたのね。。。
ウルシステムやオージスの本は知ってたけど、
キャッツの本、マジでこれまでずーっと目に止まりませんでした。
この本読んでおきゃ、去年一年無駄にせずに済んだものを。。。

あと、面白そうなのは、セマンティックWebで会社作って、星雲社からシリーズ本出してる人の本。
ここ数年、漏れが目標としながらなかなか形として実らなかったものが、着々と形になってきているんだな〜と強く感じた、春の夜。

よく分らんが、UMLみたいなモデリングに関するものって
形式的仕様記述と呼べる物なのか？おれは代数学を
使わないとそうは呼べないものだと思っていたが。論理で
ゴリゴリやるのもそう読んでいいかもしれんけど。

>>313
別にどう解釈してもえぇ〜んじゃねぇ〜？

仮にUMLが代数学と比べてショボい・低級なツールに見えるとして、
そのショボいツールで、LSI製造メーカがLSI設計しようとしているとしたら、
その意味はどこにあるのか、考えてみてはいかがでしょうねぇ。

今、国内で、それなりの規模と質の仕事で、形式的仕様記述を扱おうとしている所って、
どれくらいあるんでしょうね？

・旧鉄道総研系？
・証券のWebフロントエンドやってるあそこ
・SystemC＋UMLでツール作ってる↑あそこ
・組込系でExecutableUMLやってる所
・MDA周りは、形式的仕様記述ってのとは違うのかな？(大メーカ、大SIerもまだ模様眺めみたいですが。。。)

>>315
いやだからおれの言いたいのは、UMLはスレ違いなんじゃ
ないだろうかってこと。まあ過疎スレだから何書こうが
おれはどうでもいいけど。

>>313
Syntropy方法論でVDM使って形式仕様記述(つかHoare論理の記述なのかな？)したのが、
UML 1.1 Object Constraint Language 標準化の発端だとすれば、
OCL込みのUML、OCLと等価の仕様記述を持ったUMLも、形式仕様記述の一種と見ていいのではないかと。
後、Executable UML〜MDAの流れも。

あと、形式的仕様記述っつうと堅苦しく見えるけど、
Formal Method って言えば、いろいろバリエーションがある事は想像がつくでそ。
例えば、>>５６ のメモ参照。

どう思われますか。

>>317
あんたのレスは筋違い。
わかったふうなレスで、スレを荒らすな。
厨房はもう寝れ。

>>315
「人海戦術で厨房プログラマー集めて、雑多なシステムLSIを大量に設計させるのが目的。
　それが可能になったら、高学歴高収入のLSI設計者はリストラしたい」、とかなんとかだったら、
日本の将来は暗いねぇ〜ｗ

>>316
ttp://unit.aist.go.jp/informatics/ も入れよう.

>320
そもそも ITって、そんなもんでは?
「素人でも熟練者なみの○○ができる！」っていうか.

`>321

ぁ、AISTのシステム検証センターね。関西だっけ？
ちょっと前まで、ポス毒とテクニシャンの募集してたっけ。
たしか、テクニシャンの任期が最長2年、なんでちょっと(ry


で、IT云々の件、
メーカや総研やSIerで なんちゃってSE/コンサルやるなら、
その程度の認識でも結構でしょうけどｗ
俺は、そんな程度の奴とはお付き合いしたくないなぁ〜

理学者が、概念整理して体系を作って、
工学者が、それを素人でも扱える対象に焼きなおして、
そうやって食い散らかされた挙句の
「一見うまくいきそうだが、実は落とし穴だらけ」な「単純作業の荒野」
で、素人労働者の皆さんに、いかにいきいきとクリエイティブな仕事をして頂くか？
という観点も重要なんぢゃないか、と。

>>322
高学歴高収入なエンジニアは（おそらく）クリエイティブな設計をする為の訓練を受けてない,
落とし穴をひとつひとつ潰していく（ある種のデバッグ）事が高学歴高収入なエンジニアの仕事　⇒　自分の首を絞め...

ホントに工学部でスポイルされちまった、自称高学歴の職人さんより、
まっとうな学問的訓練の経験すら怪しい厨房プログラマ〜の方が、
ナンとやらも煽れば木に登る〜って感じで、オモロイ反応してくれるかもｗ

俺は厨房とは顔合わせるのもやだけどｗ

>>323
クリエイティブなLSI設計って、一体なんなんでしょう？

東芝-Sony-IBMのセル計画みたいなの？
それとも、いち早くMP3エンコーダ・チップや、MP4ビデオ・プレーヤや、新しい携帯電話付加機能を企画するような人の事？
はたまた、ヲズニアックみたく、シンプルで高機能な回路を設計する人の事？

よくわかんないっす。

マイクロ・プロセッサの開発：IntelとNEC (1970頃)
LSI設計のコンピュータ支援：(1970年代アメリカ)
DSPの開発：　　　　　　　　　　NEC (1980年代？)
PLDとかFPGAの開発：　　　　(多分海外っすね、これは)
とか見ると、日系企業では NECのクリエイティビティが結構高そうかなｗ

物性物理の新規分野開拓、てな意味では、日立とかNECとか、強いよね〜多分。

う〜ん、難しい問題ですな。
ただ、昔と今とでは状況が違う。
昔は、開発に携わる事ができる人がほんの一握りであって、
そんな仕事に就くには（信用が必要なので）高学歴であったけど、
今では、開発が非常に多くなって高学歴職人が揃えられなくなった,,,
厨房でも設計できるツールが必要≒高学歴高収入は不要

クリエイティブは、個人の感性とか経験が大事なので、学歴はあまり関係ない，
芸術に近いものだと思う。
学歴が感性を磨いたり経験を積んだりするのに役立たない教育過程の指標な訳だし。

なんか、スレ違いなので、この辺で...

頭いい人なら、自分で記述方法を考案してそれを使うよね。
他人の作ったものをありがたがるんじゃなくて。俺仕様の
害悪とはまた別の話になるけど。

>>322
AISTはDQ法化してから商売に走ってるからなあ。
でもまだ武家の商法ってところはあるね。

鉄道信号の場合は国際規格との絡みもあるからな。
ヨーロッパのメーカは差別化のために形式仕様を
宣伝してるから日本がこれに追従できないとこれから
海外で商売する場合に困るのは確かだね。

で、モデルチェッキングくらいなら素人でもすぐ使えるよ。
SPINとかSMVとか只で使えるツールもダウンロードできるし。
AISTはSMVつかってるね。あれはCTLで仕様を書くのかな。
SPINはLTLだね。どっちがいいかは一長一短あるけど。
使ってみると面白いからやってみたら？

形式仕様はクリエイティビティを阻害しないと思うよ。
それに、形式仕様って実はそんなに難しくないって。
今時は文系でも形式論理学教えてたりするからね。

一応修士修了の漏れがいうのもなんだけど
”高学歴”って確かに意味ないね。
クリエイティビティは学問の世界でも大事なはずだけど
実際には大学の教育はそういうこととは無縁なのは確か。
まあ、教育でどうこうできるのか？って疑問はあるけどね。

＞UMLみたいなモデリングに関するものって
＞形式的仕様記述と呼べる物なのか？
＞おれは代数学を使わないとそうは呼べないものだと思っていたが。

ま、代数を使うかどうかは別として、UMLの場合
モデルが満たすべき性質を陽に記述できないんで
その意味では形式仕様の記述っていう感じではない。
（OCLとかいう言語で性質を記述するとかいう話もあるが
　よく知らないので割愛。）

代数っていうのは例えばCafeObjみたいな
代数的仕様記述のこといってるのかな？
実は漏れ、あれのどこが代数なのか
よく分からないんだけど（笑）

>>329
論理学って、数理論理学以外は文系に分類されちまうらしいね。

それから、大学が、クリエイティビティを促進するか、阻害するか、は一概には決められないと思うよ。
そーゆーこと言う人って、いったいどこの学部/学科出身なんだろうね？情報系〜工学系？ｗ

>>330
UMLは、UML1.1以降のOCL込みで、形式仕様記述であろうとした、って感じだと。

>>331
いや、最近は文系でも数理論理学を教えてたりするよ。

大学がクリエイティビティを阻害するとは思わないけど
積極的に促進するって感じでもないでしょ。
もちろん、例外はいくらもあると思うよ。
そういうところにはがんばってほしいよね。
ちなみに漏れは理工系学部の情報系学科出身。
やってきたのは理論臭いことばっか。
だから漏れの見方も偏見に満ちてる。ｗ

>>331
そして、ExecutableUML〜MDA〜UML2.0で、ツールが自動コード生成するための、
グラフィカル・モデリング言語になったとさｗ

めでたしめでたし

昼弁当23時の問題

昼飯用に調理された弁当を、23時に食べても安全であるか否かという
前世紀初等に提出された有名な未解決問題。

IPA
セキュリティエンジニアリング
ソフトウェア開発者向けのページ

2. セキュアプロトコルと相互運用可能性確保
http://www.ipa.go.jp/security/awareness/vendor/software.html#2

IPAか。
あそこは結構腐ったネタを、文献調査してあとはせいぜいデモ・システム作って
研究と称してる感じがあるから、パスしときたいな。

いまどき、○×総研程度の連中ですら、
「検索エンジン使って情報集めるようなのは研究とは呼べない」だってさ。
連中がWebCrawlの研究開発に貢献した、という噂は一切聞いた事ないんだけどｗ

あんまり身のある議論も出なさそうだけど、とりあえずあげ