<?xml version='1.0' encoding='UTF-8'?><?xml-stylesheet href="http://www.blogger.com/styles/atom.css" type="text/css"?><feed xmlns='http://www.w3.org/2005/Atom' xmlns:openSearch='http://a9.com/-/spec/opensearchrss/1.0/' xmlns:blogger='http://schemas.google.com/blogger/2008' xmlns:georss='http://www.georss.org/georss' xmlns:gd="http://schemas.google.com/g/2005" xmlns:thr='http://purl.org/syndication/thread/1.0'><id>tag:blogger.com,1999:blog-8456525132033459936</id><updated>2024-11-01T19:34:14.881+09:00</updated><category term="CBMC"/><category term="テスト"/><category term="命題論理"/><category term="形式仕様記述"/><category term="ツール"/><category term="NuSMV"/><category term="ソースコード検証"/><category term="モデリング"/><category term="リアルタイム性"/><category term="信頼性"/><category term="動作モデル"/><category term="PDD"/><category term="技術マップ"/><category term="設計"/><category term="謎"/><category term="CSP"/><category term="Java"/><category term="LTSA"/><category term="レビュー"/><category term="機能安全"/><category term="目から鱗"/><title type='text'>Embedded-Note lagavulin1956</title><subtitle type='html'></subtitle><link rel='http://schemas.google.com/g/2005#feed' type='application/atom+xml' href='http://tfujikura.blogspot.com/feeds/posts/default'/><link rel='self' type='application/atom+xml' href='http://www.blogger.com/feeds/8456525132033459936/posts/default?redirect=false'/><link rel='alternate' type='text/html' href='http://tfujikura.blogspot.com/'/><link rel='hub' href='http://pubsubhubbub.appspot.com/'/><author><name>tfujikura</name><uri>http://www.blogger.com/profile/05727198324191810209</uri><email>noreply@blogger.com</email><gd:image rel='http://schemas.google.com/g/2005#thumbnail' width='32' height='29' src='//blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEgs8epYPe4xa3goLTfveQ_C5vLTl1207yOIrsIgxkIlBI5iDSFjVJFSWLsVx3BSJ1JlbVyC5e525_cMtwaUdrRMwQ6noANN_AnsnfyUeYvwIKzVLFyy4nzznFs9IyWo7FQ/s220/%E3%83%97%E3%83%AD%E3%83%95%E3%82%A3%E3%83%BC%E3%83%AB01.jpg'/></author><generator version='7.00' uri='http://www.blogger.com'>Blogger</generator><openSearch:totalResults>25</openSearch:totalResults><openSearch:startIndex>1</openSearch:startIndex><openSearch:itemsPerPage>25</openSearch:itemsPerPage><entry><id>tag:blogger.com,1999:blog-8456525132033459936.post-8071850954828965952</id><published>2011-03-27T15:09:00.001+09:00</published><updated>2011-03-27T15:10:06.622+09:00</updated><category scheme="http://www.blogger.com/atom/ns#" term="NuSMV"/><category scheme="http://www.blogger.com/atom/ns#" term="モデリング"/><category scheme="http://www.blogger.com/atom/ns#" term="形式仕様記述"/><title type='text'>NuSMVで非決定性状態マシン</title><summary type="text">非決定性の状態遷移があると実装には落とせないので、非決定性の有無は設計検証の対象になる。しかし、要求仕様の段階では非決定性のままで検証したいこともある。たとえば、ランダムな振る舞いをする外部デバイス等を環境モデルに取り込む場合などである。

ASSIGN
&amp;nbsp;&amp;nbsp;next (s) :=
&amp;nbsp;&amp;nbsp; &amp;nbsp;case
&amp;nbsp;&amp;nbsp; &amp;nbsp; &amp;nbsp; T_S1 : Sl;
&amp;nbsp;&amp;nbsp; &amp;nbsp; &amp;nbsp; T_S2 : S2;
&amp;nbsp;&amp;nbsp; &amp;nbsp; &amp;nbsp; T_S3 : S3;
&amp;nbsp;&amp;nbsp; &amp;nbsp; &amp;nbsp; !inS &amp;amp; next(inS) : S1; -- start state
&amp;nbsp;&amp;nbsp; &amp;nbsp; &amp;nbsp; TRUE : s;
&amp;</summary><link rel='replies' type='application/atom+xml' href='http://tfujikura.blogspot.com/feeds/8071850954828965952/comments/default' title='コメントの投稿'/><link rel='replies' type='text/html' href='http://tfujikura.blogspot.com/2011/03/nusmv_27.html#comment-form' title='0 件のコメント'/><link rel='edit' type='application/atom+xml' href='http://www.blogger.com/feeds/8456525132033459936/posts/default/8071850954828965952'/><link rel='self' type='application/atom+xml' href='http://www.blogger.com/feeds/8456525132033459936/posts/default/8071850954828965952'/><link rel='alternate' type='text/html' href='http://tfujikura.blogspot.com/2011/03/nusmv_27.html' title='NuSMVで非決定性状態マシン'/><author><name>tfujikura</name><uri>http://www.blogger.com/profile/05727198324191810209</uri><email>noreply@blogger.com</email><gd:image rel='http://schemas.google.com/g/2005#thumbnail' width='32' height='29' src='//blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEgs8epYPe4xa3goLTfveQ_C5vLTl1207yOIrsIgxkIlBI5iDSFjVJFSWLsVx3BSJ1JlbVyC5e525_cMtwaUdrRMwQ6noANN_AnsnfyUeYvwIKzVLFyy4nzznFs9IyWo7FQ/s220/%E3%83%97%E3%83%AD%E3%83%95%E3%82%A3%E3%83%BC%E3%83%AB01.jpg'/></author><thr:total>0</thr:total></entry><entry><id>tag:blogger.com,1999:blog-8456525132033459936.post-1057264391749348983</id><published>2011-03-23T00:11:00.001+09:00</published><updated>2011-03-23T00:20:19.868+09:00</updated><category scheme="http://www.blogger.com/atom/ns#" term="NuSMV"/><category scheme="http://www.blogger.com/atom/ns#" term="モデリング"/><category scheme="http://www.blogger.com/atom/ns#" term="動作モデル"/><title type='text'>NuSMVで階層化状態マシン</title><summary type="text">NuSMVはSPINよりもモデル化の自由度が大きくUML等で出てくる階層化状態マシンをAND状態も含めてモデル化することができる。

まず、与えられた階層化状態マシンについて二つの集合を作成する。

Τ : root stateの集合、トップ状態とAND状態の子供
Α : atomic stateの集合とAND状態

ある状態 s について v(s)は直近の親を表すとする。Tは　v(s) = s&amp;nbsp;∈&amp;nbsp;T となるような集合。

Tの要素はNuSMVの列挙型変数とする。そして、列挙型の要素 b は、

a&amp;nbsp;∈&amp;nbsp;T の時に、v(b)&amp;nbsp;∈ a　となるようなb


によって構成される。
この状態図の場合


VAR

&amp;nbsp;&amp;nbsp;M: {P, Q};&amp;nbsp;&amp;nbsp;R: {UI, U2, V};&amp;nbsp;&amp;nbsp;S: {</summary><link rel='replies' type='application/atom+xml' href='http://tfujikura.blogspot.com/feeds/1057264391749348983/comments/default' title='コメントの投稿'/><link rel='replies' type='text/html' href='http://tfujikura.blogspot.com/2011/03/nusmv_23.html#comment-form' title='0 件のコメント'/><link rel='edit' type='application/atom+xml' href='http://www.blogger.com/feeds/8456525132033459936/posts/default/1057264391749348983'/><link rel='self' type='application/atom+xml' href='http://www.blogger.com/feeds/8456525132033459936/posts/default/1057264391749348983'/><link rel='alternate' type='text/html' href='http://tfujikura.blogspot.com/2011/03/nusmv_23.html' title='NuSMVで階層化状態マシン'/><author><name>tfujikura</name><uri>http://www.blogger.com/profile/05727198324191810209</uri><email>noreply@blogger.com</email><gd:image rel='http://schemas.google.com/g/2005#thumbnail' width='32' height='29' src='//blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEgs8epYPe4xa3goLTfveQ_C5vLTl1207yOIrsIgxkIlBI5iDSFjVJFSWLsVx3BSJ1JlbVyC5e525_cMtwaUdrRMwQ6noANN_AnsnfyUeYvwIKzVLFyy4nzznFs9IyWo7FQ/s220/%E3%83%97%E3%83%AD%E3%83%95%E3%82%A3%E3%83%BC%E3%83%AB01.jpg'/></author><media:thumbnail xmlns:media="http://search.yahoo.com/mrss/" url="https://blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEiYxcfSl4EpHD1nIeIZGe73JIqtGTah5EwGfuDFnM4ynt0TQh6eRWl4jtziULRSBP7Vho6jIZkhYcT3lbxsLMB9A-fyPn9u7NSd-MtMsWSZReg6gJCPomcIhseyfCyBIMmLcI8Hoq6lm2E/s72-c/%25E9%259A%258E%25E5%25B1%25A4%25E5%258C%2596%25E7%258A%25B6%25E6%2585%258B%25E5%259B%25B3.jpg" height="72" width="72"/><thr:total>0</thr:total></entry><entry><id>tag:blogger.com,1999:blog-8456525132033459936.post-3516440019871965090</id><published>2011-03-21T17:19:00.002+09:00</published><updated>2011-03-28T16:54:28.702+09:00</updated><category scheme="http://www.blogger.com/atom/ns#" term="NuSMV"/><category scheme="http://www.blogger.com/atom/ns#" term="リアルタイム性"/><title type='text'>NuSMVでタイミング解析</title><summary type="text">モデル検査ツールのNuSMVを使用してタイミング解析が可能である。従来のCPU使用率に基づく手法に比べて悲観的な結果が出ることもなく、起動オフセットも含めて網羅的な検証が可能である。さらに、最小応答時間と最大応答時間を求めることもできる。ただし、従来の手法に比べて計算時間が長くなる。
Cheddarを紹介した際の問題をNuSMVで解いてみる。

まず、基本的な定数を定義する


DEFINE
C1:=20; C2:=40; C3:=100; -- Ciは実行時間
D1:=100; D2:=150; D3:=350; -- Diはデッドライン=起動周期

次に変数
VARc1:0..C1;  -- ci: taskiの実行残り時間c2:0..C2;&amp;nbsp;c3:0..C3;&amp;nbsp;d1:0..D1; -- di: デットラインまでの時間、起動オフセットd2:0..D2;&amp;nbsp;</summary><link rel='replies' type='application/atom+xml' href='http://tfujikura.blogspot.com/feeds/3516440019871965090/comments/default' title='コメントの投稿'/><link rel='replies' type='text/html' href='http://tfujikura.blogspot.com/2011/03/nusmv.html#comment-form' title='0 件のコメント'/><link rel='edit' type='application/atom+xml' href='http://www.blogger.com/feeds/8456525132033459936/posts/default/3516440019871965090'/><link rel='self' type='application/atom+xml' href='http://www.blogger.com/feeds/8456525132033459936/posts/default/3516440019871965090'/><link rel='alternate' type='text/html' href='http://tfujikura.blogspot.com/2011/03/nusmv.html' title='NuSMVでタイミング解析'/><author><name>tfujikura</name><uri>http://www.blogger.com/profile/05727198324191810209</uri><email>noreply@blogger.com</email><gd:image rel='http://schemas.google.com/g/2005#thumbnail' width='32' height='29' src='//blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEgs8epYPe4xa3goLTfveQ_C5vLTl1207yOIrsIgxkIlBI5iDSFjVJFSWLsVx3BSJ1JlbVyC5e525_cMtwaUdrRMwQ6noANN_AnsnfyUeYvwIKzVLFyy4nzznFs9IyWo7FQ/s220/%E3%83%97%E3%83%AD%E3%83%95%E3%82%A3%E3%83%BC%E3%83%AB01.jpg'/></author><thr:total>0</thr:total></entry><entry><id>tag:blogger.com,1999:blog-8456525132033459936.post-3362275611556429715</id><published>2011-02-11T14:57:00.000+09:00</published><updated>2011-02-11T14:57:06.339+09:00</updated><category scheme="http://www.blogger.com/atom/ns#" term="テスト"/><category scheme="http://www.blogger.com/atom/ns#" term="命題論理"/><category scheme="http://www.blogger.com/atom/ns#" term="形式仕様記述"/><title type='text'>Generating Method for Combinatorial Testing Data Using Propositional Normal Form Conversion</title><summary type="text">In an embedded system which operates multiple devices, combinatorial testing of multiple events is needed to verify proper behavior of the system. However, the number of test cases becomes huge, especially for the order in which events happen in parallel, and it is difficult to carry out all cases.&amp;nbsp; So many methods to generate minimum test data set have been already proposed, but their </summary><link rel='replies' type='application/atom+xml' href='http://tfujikura.blogspot.com/feeds/3362275611556429715/comments/default' title='コメントの投稿'/><link rel='replies' type='text/html' href='http://tfujikura.blogspot.com/2011/02/generating-method-for-combinatorial.html#comment-form' title='0 件のコメント'/><link rel='edit' type='application/atom+xml' href='http://www.blogger.com/feeds/8456525132033459936/posts/default/3362275611556429715'/><link rel='self' type='application/atom+xml' href='http://www.blogger.com/feeds/8456525132033459936/posts/default/3362275611556429715'/><link rel='alternate' type='text/html' href='http://tfujikura.blogspot.com/2011/02/generating-method-for-combinatorial.html' title='Generating Method for Combinatorial Testing Data Using Propositional Normal Form Conversion'/><author><name>tfujikura</name><uri>http://www.blogger.com/profile/05727198324191810209</uri><email>noreply@blogger.com</email><gd:image rel='http://schemas.google.com/g/2005#thumbnail' width='32' height='29' src='//blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEgs8epYPe4xa3goLTfveQ_C5vLTl1207yOIrsIgxkIlBI5iDSFjVJFSWLsVx3BSJ1JlbVyC5e525_cMtwaUdrRMwQ6noANN_AnsnfyUeYvwIKzVLFyy4nzznFs9IyWo7FQ/s220/%E3%83%97%E3%83%AD%E3%83%95%E3%82%A3%E3%83%BC%E3%83%AB01.jpg'/></author><media:thumbnail xmlns:media="http://search.yahoo.com/mrss/" url="https://blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEilmlZ3eUtkI6DqwrDZuu1EoNYYv2vnZ-wS1PYm56fMTroASGsGHpbSp5FTfzRwwAsXDBhknOSgVlRf73JexruCnOSby-2DO8ZpP9svFxz5CxpZuoebRcYAcMu2gRfctISWwFMysH5PDqo/s72-c/Table1.jpg" height="72" width="72"/><thr:total>0</thr:total></entry><entry><id>tag:blogger.com,1999:blog-8456525132033459936.post-3053431901560939635</id><published>2010-12-09T11:38:00.003+09:00</published><updated>2010-12-09T16:50:09.122+09:00</updated><category scheme="http://www.blogger.com/atom/ns#" term="命題論理"/><category scheme="http://www.blogger.com/atom/ns#" term="機能安全"/><title type='text'>決定論的故障⇒決定論的原因故障</title><summary type="text">systematic failureを決定論的故障と呼ぶことにかなり違和感があった。ソフトにバグがあれば必ずおかしな動作をする。これが決定論的な動作で、そのような故障原因は安全ライフサイクルの様なシステマティックなアプローチで解決する。と言うことだと理解している。間違っていたら指摘してもらいたい。

日本語は原因の特徴について述べていて、英語は対処法について述べている。ここに違和感があったのだが、Webを見ていたら決定論的原因故障と訳している場合も多く、こちらであれば、「決定論的原因による故障」と解釈することで何とか納得できる。

決定論的原因とは原因箇所を論理的に絞り込めたり、それを証明することができるタイプの故障で、またそのことによって完全に取り除くことができる故障原因と定義してはどうだろうか。


例えばコンポーネントがA,B,Cとあってある機能Fが動かなくなってコンポーネン
トB</summary><link rel='replies' type='application/atom+xml' href='http://tfujikura.blogspot.com/feeds/3053431901560939635/comments/default' title='コメントの投稿'/><link rel='replies' type='text/html' href='http://tfujikura.blogspot.com/2010/12/blog-post.html#comment-form' title='0 件のコメント'/><link rel='edit' type='application/atom+xml' href='http://www.blogger.com/feeds/8456525132033459936/posts/default/3053431901560939635'/><link rel='self' type='application/atom+xml' href='http://www.blogger.com/feeds/8456525132033459936/posts/default/3053431901560939635'/><link rel='alternate' type='text/html' href='http://tfujikura.blogspot.com/2010/12/blog-post.html' title='決定論的故障⇒決定論的原因故障'/><author><name>tfujikura</name><uri>http://www.blogger.com/profile/05727198324191810209</uri><email>noreply@blogger.com</email><gd:image rel='http://schemas.google.com/g/2005#thumbnail' width='32' height='29' src='//blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEgs8epYPe4xa3goLTfveQ_C5vLTl1207yOIrsIgxkIlBI5iDSFjVJFSWLsVx3BSJ1JlbVyC5e525_cMtwaUdrRMwQ6noANN_AnsnfyUeYvwIKzVLFyy4nzznFs9IyWo7FQ/s220/%E3%83%97%E3%83%AD%E3%83%95%E3%82%A3%E3%83%BC%E3%83%AB01.jpg'/></author><thr:total>0</thr:total></entry><entry><id>tag:blogger.com,1999:blog-8456525132033459936.post-1526238700078268354</id><published>2010-10-09T22:15:00.000+09:00</published><updated>2010-10-09T22:15:52.480+09:00</updated><category scheme="http://www.blogger.com/atom/ns#" term="ツール"/><category scheme="http://www.blogger.com/atom/ns#" term="リアルタイム性"/><title type='text'>Cheddar: タイミング解析ツール</title><summary type="text">フリーのタイミング解析ツールCheddarを使ってみた。Windows版をダウンロードして解凍するとexeが出てくるのでそれをダブルクリックすれば立ち上がる。

一通り使えるだけの情報を提供するマニュアルもあるし、そこから関連する論文へのインデックスも付いているので時間を掛ければ色々面白いことができそうだ。
まず、プロセッサを定義する。Edit&amp;gt;Update Processorでスケジューラを指定する。RTOSの優先度ベースのスケジューリングに対応するのはHighest Priority Firstなので、これを選んでみる。この他にデッドラインモノトニックとか定番のモノが用意されている。Rate Monotonicを選べばタスク優先度を付けなくても良いので最初はこの方が良いかも知れない。独自に定義することもできる。

次にEdit&amp;gt;Update address spaceで</summary><link rel='replies' type='application/atom+xml' href='http://tfujikura.blogspot.com/feeds/1526238700078268354/comments/default' title='コメントの投稿'/><link rel='replies' type='text/html' href='http://tfujikura.blogspot.com/2010/10/cheddar.html#comment-form' title='0 件のコメント'/><link rel='edit' type='application/atom+xml' href='http://www.blogger.com/feeds/8456525132033459936/posts/default/1526238700078268354'/><link rel='self' type='application/atom+xml' href='http://www.blogger.com/feeds/8456525132033459936/posts/default/1526238700078268354'/><link rel='alternate' type='text/html' href='http://tfujikura.blogspot.com/2010/10/cheddar.html' title='Cheddar: タイミング解析ツール'/><author><name>tfujikura</name><uri>http://www.blogger.com/profile/05727198324191810209</uri><email>noreply@blogger.com</email><gd:image rel='http://schemas.google.com/g/2005#thumbnail' width='32' height='29' src='//blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEgs8epYPe4xa3goLTfveQ_C5vLTl1207yOIrsIgxkIlBI5iDSFjVJFSWLsVx3BSJ1JlbVyC5e525_cMtwaUdrRMwQ6noANN_AnsnfyUeYvwIKzVLFyy4nzznFs9IyWo7FQ/s220/%E3%83%97%E3%83%AD%E3%83%95%E3%82%A3%E3%83%BC%E3%83%AB01.jpg'/></author><media:thumbnail xmlns:media="http://search.yahoo.com/mrss/" url="https://blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEgAR-tmMOp6wa9DLXOvOMiwT1cAB2ZdxI05cDOj0nYkpdLsUp2obEHGpSJrv1E1MVaIBRXaAMvPGjTAWUBj2Pkbf9qEhLK93oRg0VgoHHv8xF3vrhr-0vn19W1-GhNG12dn4xw1_NgNUYA/s72-c/cheddar.jpg" height="72" width="72"/><thr:total>0</thr:total></entry><entry><id>tag:blogger.com,1999:blog-8456525132033459936.post-6583606106015800854</id><published>2010-07-22T10:46:00.000+09:00</published><updated>2010-07-22T10:46:00.438+09:00</updated><title type='text'>implyとequivalent及びBranch coverageとDecision coverage</title><summary type="text">Twitterで話していたがまとめて話さないと伝わらないので、まとめてみる

ここに、Branch/Decision Testingという記事があって、冒頭に

For components with one entry point 100% Branch Coverage is equivalent to 100% Decision Coverage (入り口が一つのコンポーネントに対しては100%BCは100%DCと等しい)

と書いてある。

equivalentとは?
等しいのだからBDが100%ならDCも100%になりその逆も成立する。等価性には対称律が成立する。

入り口が複数あるとは?
構造化プログラム言語を使っていると関数の入り口は一つに決まっているが、昔のFortranのentry文を使うとサブルーチンの入り口を複数作ることができる。今でもOSのディスパッチャ等はマルチ</summary><link rel='replies' type='application/atom+xml' href='http://tfujikura.blogspot.com/feeds/6583606106015800854/comments/default' title='コメントの投稿'/><link rel='replies' type='text/html' href='http://tfujikura.blogspot.com/2010/07/implyequivalentbranch-coveragedecision.html#comment-form' title='0 件のコメント'/><link rel='edit' type='application/atom+xml' href='http://www.blogger.com/feeds/8456525132033459936/posts/default/6583606106015800854'/><link rel='self' type='application/atom+xml' href='http://www.blogger.com/feeds/8456525132033459936/posts/default/6583606106015800854'/><link rel='alternate' type='text/html' href='http://tfujikura.blogspot.com/2010/07/implyequivalentbranch-coveragedecision.html' title='implyとequivalent及びBranch coverageとDecision coverage'/><author><name>tfujikura</name><uri>http://www.blogger.com/profile/05727198324191810209</uri><email>noreply@blogger.com</email><gd:image rel='http://schemas.google.com/g/2005#thumbnail' width='32' height='29' src='//blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEgs8epYPe4xa3goLTfveQ_C5vLTl1207yOIrsIgxkIlBI5iDSFjVJFSWLsVx3BSJ1JlbVyC5e525_cMtwaUdrRMwQ6noANN_AnsnfyUeYvwIKzVLFyy4nzznFs9IyWo7FQ/s220/%E3%83%97%E3%83%AD%E3%83%95%E3%82%A3%E3%83%BC%E3%83%AB01.jpg'/></author><media:thumbnail xmlns:media="http://search.yahoo.com/mrss/" url="https://blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEhXghr06b2Uore3ABRNA1xRLFPQbp1Kmw7IAZRmGeHXgz2o956hh4C85Ye_ESnm-gf8mHVQ5H7nZZJ65505qrKRmnfdH4X-oNU-fZPigpWAwrjtGJSg8aTVD1PzCFVhu0-TXcEutKUa4rY/s72-c/%E3%82%A2%E3%82%BB%E3%83%B3%E3%83%96%E3%83%A9.jpg" height="72" width="72"/><thr:total>0</thr:total></entry><entry><id>tag:blogger.com,1999:blog-8456525132033459936.post-8288788166057992641</id><published>2010-07-18T15:13:00.002+09:00</published><updated>2010-07-18T23:25:36.263+09:00</updated><category scheme="http://www.blogger.com/atom/ns#" term="CSP"/><category scheme="http://www.blogger.com/atom/ns#" term="Java"/><category scheme="http://www.blogger.com/atom/ns#" term="リアルタイム性"/><category scheme="http://www.blogger.com/atom/ns#" term="謎"/><title type='text'>Wot, no chickens?</title><summary type="text">Javaにはリアルタイム性が無いと言うと、ガベージコレクタの話題かと思うが、それだけではない。以下の二つも問題である。

Javaには待ち行列が二つある。Synchronizedによる待ち行列とwait/notifyによる待ち行列である。この二つの待ち行列のせいでライブロックが発生する。これはJava仕様の問題だろう。
それからもう一つ、待ち行列がFIFOではなくLIFOになっていることである。どこまでがJava仕様でどこからがVM実装依存なのか分からないが、現在ダウンロードできるJavaの実行環境はLIFOになっている。LIFOだと後から来たスレッドが先に処理されるので、オーバーロード時には最初に来たスレッドは永遠に待たされる。優先度付き待ち行列のポリシーはVM実装時に変更できないとどこかで読んだ気がするが、この記憶が正しければJava仕様の問題だろう。

これだけJavaが使われてい</summary><link rel='replies' type='application/atom+xml' href='http://tfujikura.blogspot.com/feeds/8288788166057992641/comments/default' title='コメントの投稿'/><link rel='replies' type='text/html' href='http://tfujikura.blogspot.com/2010/07/wot-no-chickens.html#comment-form' title='0 件のコメント'/><link rel='edit' type='application/atom+xml' href='http://www.blogger.com/feeds/8456525132033459936/posts/default/8288788166057992641'/><link rel='self' type='application/atom+xml' href='http://www.blogger.com/feeds/8456525132033459936/posts/default/8288788166057992641'/><link rel='alternate' type='text/html' href='http://tfujikura.blogspot.com/2010/07/wot-no-chickens.html' title='Wot, no chickens?'/><author><name>tfujikura</name><uri>http://www.blogger.com/profile/05727198324191810209</uri><email>noreply@blogger.com</email><gd:image rel='http://schemas.google.com/g/2005#thumbnail' width='32' height='29' src='//blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEgs8epYPe4xa3goLTfveQ_C5vLTl1207yOIrsIgxkIlBI5iDSFjVJFSWLsVx3BSJ1JlbVyC5e525_cMtwaUdrRMwQ6noANN_AnsnfyUeYvwIKzVLFyy4nzznFs9IyWo7FQ/s220/%E3%83%97%E3%83%AD%E3%83%95%E3%82%A3%E3%83%BC%E3%83%AB01.jpg'/></author><thr:total>0</thr:total></entry><entry><id>tag:blogger.com,1999:blog-8456525132033459936.post-3243288096172293798</id><published>2010-06-03T09:00:00.002+09:00</published><updated>2010-07-01T07:51:27.275+09:00</updated><category scheme="http://www.blogger.com/atom/ns#" term="CBMC"/><title type='text'>回文数式作成プログラム</title><summary type="text">プログラム検証ツールを使って回文数式を作る。
例えば

42+46=64+24


// 回文数式作成
void main()
{
&amp;nbsp;&amp;nbsp;int a1, a2, b1, b2, A1, A2, B1, B2;
&amp;nbsp;&amp;nbsp;__CPROVER_assume(a1 &amp;gt; 0 &amp;amp;&amp;amp; a1 &amp;lt;10 &amp;amp;&amp;amp; a2 &amp;gt; 0 &amp;amp;&amp;amp; a2 &amp;lt; 10 &amp;amp;&amp;amp; b1 &amp;gt; 0 &amp;amp;&amp;amp; b1 &amp;lt; 10 &amp;amp;&amp;amp; b2 &amp;gt; 0 &amp;amp;&amp;amp; b2 &amp;lt; 10);
&amp;nbsp;&amp;nbsp;A1 = 10*a1 + a2;
&amp;nbsp;&amp;nbsp;A2 = 10*a2 + a1;
&amp;nbsp;&amp;nbsp;B1 = 10*b1 + b2;
&amp;nbsp;&amp;</summary><link rel='replies' type='application/atom+xml' href='http://tfujikura.blogspot.com/feeds/3243288096172293798/comments/default' title='コメントの投稿'/><link rel='replies' type='text/html' href='http://tfujikura.blogspot.com/2010/06/blog-post.html#comment-form' title='0 件のコメント'/><link rel='edit' type='application/atom+xml' href='http://www.blogger.com/feeds/8456525132033459936/posts/default/3243288096172293798'/><link rel='self' type='application/atom+xml' href='http://www.blogger.com/feeds/8456525132033459936/posts/default/3243288096172293798'/><link rel='alternate' type='text/html' href='http://tfujikura.blogspot.com/2010/06/blog-post.html' title='回文数式作成プログラム'/><author><name>tfujikura</name><uri>http://www.blogger.com/profile/05727198324191810209</uri><email>noreply@blogger.com</email><gd:image rel='http://schemas.google.com/g/2005#thumbnail' width='32' height='29' src='//blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEgs8epYPe4xa3goLTfveQ_C5vLTl1207yOIrsIgxkIlBI5iDSFjVJFSWLsVx3BSJ1JlbVyC5e525_cMtwaUdrRMwQ6noANN_AnsnfyUeYvwIKzVLFyy4nzznFs9IyWo7FQ/s220/%E3%83%97%E3%83%AD%E3%83%95%E3%82%A3%E3%83%BC%E3%83%AB01.jpg'/></author><thr:total>0</thr:total></entry><entry><id>tag:blogger.com,1999:blog-8456525132033459936.post-8757029231699779858</id><published>2010-05-30T14:17:00.002+09:00</published><updated>2010-05-30T20:10:30.800+09:00</updated><category scheme="http://www.blogger.com/atom/ns#" term="CBMC"/><category scheme="http://www.blogger.com/atom/ns#" term="テスト"/><title type='text'>単体テストできない関数</title><summary type="text">ヨーロッパの鉄道の安全規格[1]で一番厳しいSIL4ではブランチテストの100%カバレッジが求められるらしい。if文がネストしている複雑な関数の場合、そこにたどり着く入力データを作り出すのはなかなか難しい。CBMCを使って簡単にテストデータを生成する方法としてassert(0)を埋め込む方法がある。到達したい場所にassert(0)を仕込んで置いてCBMCで検証をすればCBMCが向きになってそこまで行って転けてくれるのでたどり着く方法が明確になる。必要があればprintf文も仕込んでおく、さらにテキストファイルに書き出すようにすれば、テストツールに掛けられる形でテストケースを得ることができる。


しかし、この方法も構造化されたプログラムでないとうまく行かない。構造化されたプログラムというのは、逐次、分岐、繰り返し構造だけでできているプログラムで、前方に跳ぶgoto文とか入れ子にならない</summary><link rel='replies' type='application/atom+xml' href='http://tfujikura.blogspot.com/feeds/8757029231699779858/comments/default' title='コメントの投稿'/><link rel='replies' type='text/html' href='http://tfujikura.blogspot.com/2010/05/blog-post.html#comment-form' title='0 件のコメント'/><link rel='edit' type='application/atom+xml' href='http://www.blogger.com/feeds/8456525132033459936/posts/default/8757029231699779858'/><link rel='self' type='application/atom+xml' href='http://www.blogger.com/feeds/8456525132033459936/posts/default/8757029231699779858'/><link rel='alternate' type='text/html' href='http://tfujikura.blogspot.com/2010/05/blog-post.html' title='単体テストできない関数'/><author><name>tfujikura</name><uri>http://www.blogger.com/profile/05727198324191810209</uri><email>noreply@blogger.com</email><gd:image rel='http://schemas.google.com/g/2005#thumbnail' width='32' height='29' src='//blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEgs8epYPe4xa3goLTfveQ_C5vLTl1207yOIrsIgxkIlBI5iDSFjVJFSWLsVx3BSJ1JlbVyC5e525_cMtwaUdrRMwQ6noANN_AnsnfyUeYvwIKzVLFyy4nzznFs9IyWo7FQ/s220/%E3%83%97%E3%83%AD%E3%83%95%E3%82%A3%E3%83%BC%E3%83%AB01.jpg'/></author><media:thumbnail xmlns:media="http://search.yahoo.com/mrss/" url="https://blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEiMVLw0LgHy9EjRPLgkimNdO6YhJuH3_cn3gfT-mYkOk1fsX3x1FfqIm40yZQCjXRGF4asFJ6E2Juz8ClzFcdRP1IzqgVIEiSBP3KHZvO6INmwzjD0kC6LNfSCoGOchRri2L6SutyU4jSc/s72-c/%E3%83%86%E3%82%B9%E3%83%88%E3%83%87%E3%83%BC%E3%82%BF.jpg" height="72" width="72"/><thr:total>0</thr:total></entry><entry><id>tag:blogger.com,1999:blog-8456525132033459936.post-3447328165208664262</id><published>2010-04-25T12:56:00.003+09:00</published><updated>2010-04-25T13:16:01.781+09:00</updated><category scheme="http://www.blogger.com/atom/ns#" term="CBMC"/><category scheme="http://www.blogger.com/atom/ns#" term="PDD"/><category scheme="http://www.blogger.com/atom/ns#" term="ソースコード検証"/><category scheme="http://www.blogger.com/atom/ns#" term="形式仕様記述"/><title type='text'>PDD その2</title><summary type="text">インタフェース誌にPDDのアイディアを書いた[1]。基本的な手順は、

1.&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp; プログラムの目的を事後条件として表す。assert文で表現する。2.&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp; 入力条件を場合分けし、それを事前条件とする。assume文で表現する。3.&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp; assume文の範囲でコーディングをおこない、検証をパスさせる。4.&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp; パスさせる過程で反例を分析して、分析結果はコーディングまたは事前条件に反映させる。5.&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp; 残りの入力条件について同様に検証をパスさせる。6.&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp;&amp;nbsp; 全て</summary><link rel='replies' type='application/atom+xml' href='http://tfujikura.blogspot.com/feeds/3447328165208664262/comments/default' title='コメントの投稿'/><link rel='replies' type='text/html' href='http://tfujikura.blogspot.com/2010/04/pdd-2.html#comment-form' title='0 件のコメント'/><link rel='edit' type='application/atom+xml' href='http://www.blogger.com/feeds/8456525132033459936/posts/default/3447328165208664262'/><link rel='self' type='application/atom+xml' href='http://www.blogger.com/feeds/8456525132033459936/posts/default/3447328165208664262'/><link rel='alternate' type='text/html' href='http://tfujikura.blogspot.com/2010/04/pdd-2.html' title='PDD その2'/><author><name>tfujikura</name><uri>http://www.blogger.com/profile/05727198324191810209</uri><email>noreply@blogger.com</email><gd:image rel='http://schemas.google.com/g/2005#thumbnail' width='32' height='29' src='//blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEgs8epYPe4xa3goLTfveQ_C5vLTl1207yOIrsIgxkIlBI5iDSFjVJFSWLsVx3BSJ1JlbVyC5e525_cMtwaUdrRMwQ6noANN_AnsnfyUeYvwIKzVLFyy4nzznFs9IyWo7FQ/s220/%E3%83%97%E3%83%AD%E3%83%95%E3%82%A3%E3%83%BC%E3%83%AB01.jpg'/></author><thr:total>0</thr:total></entry><entry><id>tag:blogger.com,1999:blog-8456525132033459936.post-2380821859265737758</id><published>2010-04-18T01:56:00.003+09:00</published><updated>2010-04-18T13:17:38.756+09:00</updated><category scheme="http://www.blogger.com/atom/ns#" term="レビュー"/><category scheme="http://www.blogger.com/atom/ns#" term="信頼性"/><title type='text'>レビューの信頼性</title><summary type="text">レビューする時、間違っているのに正しいとしてしまう間違いと、正しいのに間違っているとしてしまう間違いの二通りの間違いがある。前者をtype-1、後者をtype-2の間違いとする。またそれぞれの発生確率をe1、e2とする。要するにtype-1は見落とし、type-2は濡れ衣を着せてしまうことに対応する。

一人で2回レビューする時、1回目で間違いとしたものは見直さない場合には、見落としの確率は低くなるが、濡れ衣の確率は高くなる。xをe1またはe2としてプロットすると上図のようになる。つまり、見落としの方は二回連続で見落とさない限り検出されるので、見落とし確率はe1*e1になる。0 &amp;lt; e1 &amp;lt; 1なので小さくなりレビューの信頼性は向上する。濡れ衣は一度着せられてしまうと脱げないので、着せられてしまう確率は高くなるのである。濡れ衣を着せられない確率は1-e2で二回連続で着せられ</summary><link rel='replies' type='application/atom+xml' href='http://tfujikura.blogspot.com/feeds/2380821859265737758/comments/default' title='コメントの投稿'/><link rel='replies' type='text/html' href='http://tfujikura.blogspot.com/2010/04/blog-post.html#comment-form' title='1 件のコメント'/><link rel='edit' type='application/atom+xml' href='http://www.blogger.com/feeds/8456525132033459936/posts/default/2380821859265737758'/><link rel='self' type='application/atom+xml' href='http://www.blogger.com/feeds/8456525132033459936/posts/default/2380821859265737758'/><link rel='alternate' type='text/html' href='http://tfujikura.blogspot.com/2010/04/blog-post.html' title='レビューの信頼性'/><author><name>tfujikura</name><uri>http://www.blogger.com/profile/05727198324191810209</uri><email>noreply@blogger.com</email><gd:image rel='http://schemas.google.com/g/2005#thumbnail' width='32' height='29' src='//blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEgs8epYPe4xa3goLTfveQ_C5vLTl1207yOIrsIgxkIlBI5iDSFjVJFSWLsVx3BSJ1JlbVyC5e525_cMtwaUdrRMwQ6noANN_AnsnfyUeYvwIKzVLFyy4nzznFs9IyWo7FQ/s220/%E3%83%97%E3%83%AD%E3%83%95%E3%82%A3%E3%83%BC%E3%83%AB01.jpg'/></author><media:thumbnail xmlns:media="http://search.yahoo.com/mrss/" url="https://blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEg0iwZYZy2p53xqJJOvlrBdxRpLB8zxw62SGuE6fXibr-s8_96MKvPQ0Ktj19MHSSmdLQXxdk-V4rMCyHGhMa8iLOtu2gDhoiTPQvLv466LM6DLUJjme8x2XGTEWWxq2ddxmpot2-2nie4/s72-c/%E5%9B%B31.jpg" height="72" width="72"/><thr:total>1</thr:total></entry><entry><id>tag:blogger.com,1999:blog-8456525132033459936.post-3298092146670508772</id><published>2010-03-31T01:33:00.002+09:00</published><updated>2010-10-02T08:02:36.948+09:00</updated><category scheme="http://www.blogger.com/atom/ns#" term="CBMC"/><category scheme="http://www.blogger.com/atom/ns#" term="PDD"/><category scheme="http://www.blogger.com/atom/ns#" term="ソースコード検証"/><title type='text'>TDD ⇒ PDD</title><summary type="text">ダイクストラは、テストでバグの存在は示せるがバグのないことは示せないと言っていた。一方で、TDDはテストを重ねながらプログラミングをおこない、用意したテストが全部通ったらプログラム完成と言うアプローチだ。と誤解しやすいが実は単なる開発プロセスに対する提案である(10/2)。
欲しいのはバグはあるかも知れないが取りあえず動作する綺麗なコードではなく、まずバグのないコードだ。
この点を改善するにはどうするか。実は良いアイディアが浮かんだ。自動テストツールではなく、プログラム検証ツールを使用して正しいことを証明しながらプログラミングをおこなうPDD(Proof driven development)だ。
プログラムSの証明とは、Qを事前条件、Rを事後条件として、{Q} S {P}が恒真であることを示すことだ。たとえば、二つの整数x, yを与えられてxが大きい値になるように、値を入れ替える</summary><link rel='replies' type='application/atom+xml' href='http://tfujikura.blogspot.com/feeds/3298092146670508772/comments/default' title='コメントの投稿'/><link rel='replies' type='text/html' href='http://tfujikura.blogspot.com/2010/03/tdd-pdd.html#comment-form' title='3 件のコメント'/><link rel='edit' type='application/atom+xml' href='http://www.blogger.com/feeds/8456525132033459936/posts/default/3298092146670508772'/><link rel='self' type='application/atom+xml' href='http://www.blogger.com/feeds/8456525132033459936/posts/default/3298092146670508772'/><link rel='alternate' type='text/html' href='http://tfujikura.blogspot.com/2010/03/tdd-pdd.html' title='TDD ⇒ PDD'/><author><name>tfujikura</name><uri>http://www.blogger.com/profile/05727198324191810209</uri><email>noreply@blogger.com</email><gd:image rel='http://schemas.google.com/g/2005#thumbnail' width='32' height='29' src='//blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEgs8epYPe4xa3goLTfveQ_C5vLTl1207yOIrsIgxkIlBI5iDSFjVJFSWLsVx3BSJ1JlbVyC5e525_cMtwaUdrRMwQ6noANN_AnsnfyUeYvwIKzVLFyy4nzznFs9IyWo7FQ/s220/%E3%83%97%E3%83%AD%E3%83%95%E3%82%A3%E3%83%BC%E3%83%AB01.jpg'/></author><thr:total>3</thr:total></entry><entry><id>tag:blogger.com,1999:blog-8456525132033459936.post-1634789899199515169</id><published>2010-03-04T15:33:00.061+09:00</published><updated>2010-03-11T05:06:08.158+09:00</updated><category scheme="http://www.blogger.com/atom/ns#" term="モデリング"/><category scheme="http://www.blogger.com/atom/ns#" term="技術マップ"/><title type='text'>モデル化のセンス</title><summary type="text">Use Caseモデルを作ろうとするとDFDのような数珠つなぎの絵を描いてしまう、なぜだろうか、と聞かれたのでしばらく考えていた。たまたまUML&amp;amp;FMと言う形式手法関係のIEEEのワークショップの資料を見ていたところ下図のような絵があった。

きっとMulti-viewのところの知識か何かが不足しているのでそのようなことになるのではないか。例えば、DFDの使い方には長けているので何でも本人は書けてしまうし良く理解できている。何でもExcelで書いてしまう人などこのタイプは多い。自分用のメモとしては良いかも知れないが、他の人には理解してもらえない。変てこな図を書いていても作るものは作っているのであれば、抽象化軸やアーキテクチャ軸は頭の中に存在しているのだろう。Multi-view軸のところには色々なタイやグラムが並んでいるが目的に応じて使い分けることをUMLは意図している。下の図の</summary><link rel='replies' type='application/atom+xml' href='http://tfujikura.blogspot.com/feeds/1634789899199515169/comments/default' title='コメントの投稿'/><link rel='replies' type='text/html' href='http://tfujikura.blogspot.com/2010/03/blog-post.html#comment-form' title='2 件のコメント'/><link rel='edit' type='application/atom+xml' href='http://www.blogger.com/feeds/8456525132033459936/posts/default/1634789899199515169'/><link rel='self' type='application/atom+xml' href='http://www.blogger.com/feeds/8456525132033459936/posts/default/1634789899199515169'/><link rel='alternate' type='text/html' href='http://tfujikura.blogspot.com/2010/03/blog-post.html' title='モデル化のセンス'/><author><name>tfujikura</name><uri>http://www.blogger.com/profile/05727198324191810209</uri><email>noreply@blogger.com</email><gd:image rel='http://schemas.google.com/g/2005#thumbnail' width='32' height='29' src='//blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEgs8epYPe4xa3goLTfveQ_C5vLTl1207yOIrsIgxkIlBI5iDSFjVJFSWLsVx3BSJ1JlbVyC5e525_cMtwaUdrRMwQ6noANN_AnsnfyUeYvwIKzVLFyy4nzznFs9IyWo7FQ/s220/%E3%83%97%E3%83%AD%E3%83%95%E3%82%A3%E3%83%BC%E3%83%AB01.jpg'/></author><media:thumbnail xmlns:media="http://search.yahoo.com/mrss/" url="https://blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEjEBOUDq3fLOyLQ00sjfX-E_MZHglQaKSWFlRGJzlcS85yaeG4uTZGoBZg9Tqj6QObwXWUZrQ47e9iNUdgb3Ai-QFz5imuZM0qUQCy9GNSmaa_9U3qrja0w5jX5Hfbw5sShYSjEgzQ9rZ4/s72-c/%E3%83%A2%E3%83%87%E3%83%AB%E8%BB%B8.jpg" height="72" width="72"/><thr:total>2</thr:total></entry><entry><id>tag:blogger.com,1999:blog-8456525132033459936.post-4505478526791262481</id><published>2010-02-26T23:55:00.006+09:00</published><updated>2010-03-31T01:37:59.579+09:00</updated><category scheme="http://www.blogger.com/atom/ns#" term="CBMC"/><category scheme="http://www.blogger.com/atom/ns#" term="ソースコード検証"/><category scheme="http://www.blogger.com/atom/ns#" term="ツール"/><category scheme="http://www.blogger.com/atom/ns#" term="命題論理"/><title type='text'>ソースコードの論理構造</title><summary type="text">要求を構造化した要求木と言う考え方を2010年2月号のインタフェース誌で紹介した。
要求管理ツールなどで要求のトレーサビリティを管理する例はあるが、それは単なる関係ではなくて論理的関係である。このことを利用して知識ベース化しようと言う考え方である。
今月のインタフェース誌(2010年4月号)はこの続きで、要求木の一番下のソースコードとの関係をプログラム検証ツールCBMC ( Bounded Model Checking for ANSI-C )を利用してソースコードも論理式にしてしまって要求木に組み込んで見ようと言う試みである。

上の図でCが左のソースコードの論理式表現になる。Rがアサーションでソースコードが満たすべき仕様になる。要求木の図ではReq6とかReq7にあたる。
CBMCはソースコードを論理化するのが目的ではなくPolySpaceと同じようなソースコード検証をするための</summary><link rel='replies' type='application/atom+xml' href='http://tfujikura.blogspot.com/feeds/4505478526791262481/comments/default' title='コメントの投稿'/><link rel='replies' type='text/html' href='http://tfujikura.blogspot.com/2010/02/blog-post_26.html#comment-form' title='1 件のコメント'/><link rel='edit' type='application/atom+xml' href='http://www.blogger.com/feeds/8456525132033459936/posts/default/4505478526791262481'/><link rel='self' type='application/atom+xml' href='http://www.blogger.com/feeds/8456525132033459936/posts/default/4505478526791262481'/><link rel='alternate' type='text/html' href='http://tfujikura.blogspot.com/2010/02/blog-post_26.html' title='ソースコードの論理構造'/><author><name>tfujikura</name><uri>http://www.blogger.com/profile/05727198324191810209</uri><email>noreply@blogger.com</email><gd:image rel='http://schemas.google.com/g/2005#thumbnail' width='32' height='29' src='//blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEgs8epYPe4xa3goLTfveQ_C5vLTl1207yOIrsIgxkIlBI5iDSFjVJFSWLsVx3BSJ1JlbVyC5e525_cMtwaUdrRMwQ6noANN_AnsnfyUeYvwIKzVLFyy4nzznFs9IyWo7FQ/s220/%E3%83%97%E3%83%AD%E3%83%95%E3%82%A3%E3%83%BC%E3%83%AB01.jpg'/></author><media:thumbnail xmlns:media="http://search.yahoo.com/mrss/" url="https://blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEiW0BWxx9dXs2FrhVC4F7a0lX_pYZmq46VfKsiU30AUsG77jDt_cueCC4eXOaiTfiRBm9oUiU8mHXPWvDhrTFnXMGhxFo5Rz6sogg1oP_VGWZSM0Wy-pgbIYjS1s5jz1wqn98NxLMzkjL0/s72-c/%E8%A6%81%E6%B1%82%E6%9C%A8.jpg" height="72" width="72"/><thr:total>1</thr:total></entry><entry><id>tag:blogger.com,1999:blog-8456525132033459936.post-7001602320543845715</id><published>2010-02-23T18:25:00.005+09:00</published><updated>2010-06-16T10:20:31.448+09:00</updated><category scheme="http://www.blogger.com/atom/ns#" term="ツール"/><title type='text'>Simics</title><summary type="text">エリクソンの基地局ソフトのデバッグのために開発されたシミュレーション用のツールSimicsを、ウィンドリバーのセミナーで見てきた。シミックスと読むらしい。

http://www.co-nss.co.jp/products/middleware/simics.html

バーチャテック・ジャパンと言うところが日本法人らしいがまだ日本語のホームページがない。英語のページに行くとホワイトペーパーがそろっている。ゾウムシのような虫の写真付きのホワイトペーパーがあった。スエーデンの虫だろうか?

ボードレベルのシミュレーションを行うことができる。システムLSIのシミュレーション等でサイクルアキュレートだと数ミリ秒分の実行で一晩かかったりするが、このツールはボードを仮想化してハードウェア部分のメモリとかバスのシミュレーションはやらないのでサクサクと動く。Windowsの時計のシミュレーションのデモ</summary><link rel='replies' type='application/atom+xml' href='http://tfujikura.blogspot.com/feeds/7001602320543845715/comments/default' title='コメントの投稿'/><link rel='replies' type='text/html' href='http://tfujikura.blogspot.com/2010/02/simics.html#comment-form' title='0 件のコメント'/><link rel='edit' type='application/atom+xml' href='http://www.blogger.com/feeds/8456525132033459936/posts/default/7001602320543845715'/><link rel='self' type='application/atom+xml' href='http://www.blogger.com/feeds/8456525132033459936/posts/default/7001602320543845715'/><link rel='alternate' type='text/html' href='http://tfujikura.blogspot.com/2010/02/simics.html' title='Simics'/><author><name>tfujikura</name><uri>http://www.blogger.com/profile/05727198324191810209</uri><email>noreply@blogger.com</email><gd:image rel='http://schemas.google.com/g/2005#thumbnail' width='32' height='29' src='//blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEgs8epYPe4xa3goLTfveQ_C5vLTl1207yOIrsIgxkIlBI5iDSFjVJFSWLsVx3BSJ1JlbVyC5e525_cMtwaUdrRMwQ6noANN_AnsnfyUeYvwIKzVLFyy4nzznFs9IyWo7FQ/s220/%E3%83%97%E3%83%AD%E3%83%95%E3%82%A3%E3%83%BC%E3%83%AB01.jpg'/></author><media:thumbnail xmlns:media="http://search.yahoo.com/mrss/" url="https://blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEjSPBuBp-EhdaeytTwtBXo0EdfWDeq0ERCcr-a72SVWqcNjLKQmTbNoSckvXuKCaz2eSYKUbYOmrex8yNd54wBx6rJhKzzU6LlYZjHy0yzbGyss7z3_D78g4sOn94gzt1smE5jvgBOOQW8/s72-c/%E8%99%AB.jpg" height="72" width="72"/><thr:total>0</thr:total></entry><entry><id>tag:blogger.com,1999:blog-8456525132033459936.post-4242073266760008357</id><published>2010-02-20T13:09:00.022+09:00</published><updated>2010-03-22T02:59:21.464+09:00</updated><category scheme="http://www.blogger.com/atom/ns#" term="テスト"/><category scheme="http://www.blogger.com/atom/ns#" term="命題論理"/><category scheme="http://www.blogger.com/atom/ns#" term="形式仕様記述"/><category scheme="http://www.blogger.com/atom/ns#" term="謎"/><title type='text'>原因結果グラフ-2 MASK</title><summary type="text">結果グラフで　A masks B とした場合の扱いは

1) A⇒￢B
2) Aが真ならBは未定義(三値論理の利用)
3) Aの真偽による場合分け

の三通りが考えられる。

1)の場合REQ制約の否定として表現できる。CEGTestの場合は、問い合わせ中だが、REQの否定を柔軟に利用できればMASKは要らなくなってしまう。&amp;nbsp;赤い四角で囲った部分を表現することが出来るので1)の意味でのMASKは特に必要ない。
青丸で囲んだところはちょっと怪しい。と言うか括弧で括るような、否定を取る優先順位を決めなければならない。そう言うことを考えなくても良いようにREQとMASKが定義してあると言うのは合理的かも知れない。ただし、最近FXの秋山氏の指摘で新たな謎が生まれた。MASKは結果側に付ける[1]と言うものである。もしそうなら原因結果グラフは結構簡単で使いやすいものになる気がする。この謎</summary><link rel='replies' type='application/atom+xml' href='http://tfujikura.blogspot.com/feeds/4242073266760008357/comments/default' title='コメントの投稿'/><link rel='replies' type='text/html' href='http://tfujikura.blogspot.com/2010/02/2-mask.html#comment-form' title='0 件のコメント'/><link rel='edit' type='application/atom+xml' href='http://www.blogger.com/feeds/8456525132033459936/posts/default/4242073266760008357'/><link rel='self' type='application/atom+xml' href='http://www.blogger.com/feeds/8456525132033459936/posts/default/4242073266760008357'/><link rel='alternate' type='text/html' href='http://tfujikura.blogspot.com/2010/02/2-mask.html' title='原因結果グラフ-2 MASK'/><author><name>tfujikura</name><uri>http://www.blogger.com/profile/05727198324191810209</uri><email>noreply@blogger.com</email><gd:image rel='http://schemas.google.com/g/2005#thumbnail' width='32' height='29' src='//blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEgs8epYPe4xa3goLTfveQ_C5vLTl1207yOIrsIgxkIlBI5iDSFjVJFSWLsVx3BSJ1JlbVyC5e525_cMtwaUdrRMwQ6noANN_AnsnfyUeYvwIKzVLFyy4nzznFs9IyWo7FQ/s220/%E3%83%97%E3%83%AD%E3%83%95%E3%82%A3%E3%83%BC%E3%83%AB01.jpg'/></author><media:thumbnail xmlns:media="http://search.yahoo.com/mrss/" url="https://blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEid4eYnl8B6FizhWHSyumOlAtbiRNe4pc7QYbevsnBkQV3jYZ1Rjr5uFaqQvCSfkei5VJHcue-5cuz4mvCbH0LWcuFCvFZtJngKm49_EIKiQZOrxxWgbzrWnNMCjmjyWYdAYlj5UtAKuKs/s72-c/%E6%88%BB%E3%82%8B(%E5%B0%8F).jpg" height="72" width="72"/><thr:total>0</thr:total></entry><entry><id>tag:blogger.com,1999:blog-8456525132033459936.post-3026499981334108528</id><published>2010-02-16T10:01:00.021+09:00</published><updated>2011-07-14T01:35:46.955+09:00</updated><category scheme="http://www.blogger.com/atom/ns#" term="テスト"/><category scheme="http://www.blogger.com/atom/ns#" term="命題論理"/><category scheme="http://www.blogger.com/atom/ns#" term="形式仕様記述"/><title type='text'>原因結果グラフを利用した形式仕様記述</title><summary type="text">形式仕様記述というと述語論理から始まるが、命題論理でもやれることは多い。その一つが原因結果グラフである。これについては以前インタフェース誌[1]に書いたことがある。しかし、最近ニフィのK氏がCEGTestをリリースされたのだがどうも仕様が違う様なので悩んでいる。また、FXのA氏のツール(X-CEG)とも違う様だ。特にMASKの扱いが違う。それで本当はどうなのか少し整理しておきたい。インタフェース誌[1]に掲載した変換規則を以下に示す。元ネタは[2]である。EとOは要素数が3ヶ以上の時は論理式の形が変わる。それは[1]を参照。


原因結果グラフの本来の使い方はテストケースを絞り込むことであり、仕様を記述することではない。仕様記述としてはMC/DC等の手法を使って絞り込む前の論理式表現に興味がある。同じ文章から原因結果グラフを作っても人によって違うグラフが出来ることが多い。それは元の文章の</summary><link rel='replies' type='application/atom+xml' href='http://tfujikura.blogspot.com/feeds/3026499981334108528/comments/default' title='コメントの投稿'/><link rel='replies' type='text/html' href='http://tfujikura.blogspot.com/2010/02/blog-post_16.html#comment-form' title='0 件のコメント'/><link rel='edit' type='application/atom+xml' href='http://www.blogger.com/feeds/8456525132033459936/posts/default/3026499981334108528'/><link rel='self' type='application/atom+xml' href='http://www.blogger.com/feeds/8456525132033459936/posts/default/3026499981334108528'/><link rel='alternate' type='text/html' href='http://tfujikura.blogspot.com/2010/02/blog-post_16.html' title='原因結果グラフを利用した形式仕様記述'/><author><name>tfujikura</name><uri>http://www.blogger.com/profile/05727198324191810209</uri><email>noreply@blogger.com</email><gd:image rel='http://schemas.google.com/g/2005#thumbnail' width='32' height='29' src='//blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEgs8epYPe4xa3goLTfveQ_C5vLTl1207yOIrsIgxkIlBI5iDSFjVJFSWLsVx3BSJ1JlbVyC5e525_cMtwaUdrRMwQ6noANN_AnsnfyUeYvwIKzVLFyy4nzznFs9IyWo7FQ/s220/%E3%83%97%E3%83%AD%E3%83%95%E3%82%A3%E3%83%BC%E3%83%AB01.jpg'/></author><media:thumbnail xmlns:media="http://search.yahoo.com/mrss/" url="https://blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEhvMdxMSruJhiy1tavIkutJ1az4WgGYjUxMDXEth-T4ctsOmEMt3xVZpBJYb4QSSCnAUS1YuReeWyA4OdwQ77jgG6Zcby6fRhWB6R0C-UA6PLKZYaKiIZfTzF5pVCVO94IT2sINBR2wdXk/s72-c/%E5%8E%9F%E5%9B%A0%E7%B5%90%E6%9E%9C%E3%82%B0%E3%83%A9%E3%83%95.jpg" height="72" width="72"/><thr:total>0</thr:total></entry><entry><id>tag:blogger.com,1999:blog-8456525132033459936.post-2170996929664475015</id><published>2010-02-13T01:23:00.005+09:00</published><updated>2010-02-13T11:47:44.482+09:00</updated><category scheme="http://www.blogger.com/atom/ns#" term="LTSA"/><category scheme="http://www.blogger.com/atom/ns#" term="動作モデル"/><category scheme="http://www.blogger.com/atom/ns#" term="設計"/><title type='text'>Watchdogの設計-2 リセットのモデル</title><summary type="text">WDTの動作モデルを作ってみる。基本的な動作を並列合成することで目的の状態マシンを生成することが出来れば、要求仕様を組み合わせてそれを満たす状態マシンを作ることが出来る。そのサンプルとしてマルチタスク下のWDTの挙動を利用する。

動作の合成
定周期タスクの動作は左図で表される。これをLTSAモデルにすると

CTask = (body-&amp;gt;alive-&amp;gt;CTask).

となる。WDTはCTaskがbody部分で無限ループになるかデッドロックになってフラグにaliveを書き込まないとシステムリセットを掛ける。リセット動作は

ResetProcess = (Allaction-&amp;gt;ResetProcess|reset-&amp;gt;shutdown-&amp;gt;END).

と書くことが出来る。ここでAllactionは、
set Allaction = {body, alive}</summary><link rel='replies' type='application/atom+xml' href='http://tfujikura.blogspot.com/feeds/2170996929664475015/comments/default' title='コメントの投稿'/><link rel='replies' type='text/html' href='http://tfujikura.blogspot.com/2010/02/watchdog-2-ltsa.html#comment-form' title='0 件のコメント'/><link rel='edit' type='application/atom+xml' href='http://www.blogger.com/feeds/8456525132033459936/posts/default/2170996929664475015'/><link rel='self' type='application/atom+xml' href='http://www.blogger.com/feeds/8456525132033459936/posts/default/2170996929664475015'/><link rel='alternate' type='text/html' href='http://tfujikura.blogspot.com/2010/02/watchdog-2-ltsa.html' title='Watchdogの設計-2 リセットのモデル'/><author><name>tfujikura</name><uri>http://www.blogger.com/profile/05727198324191810209</uri><email>noreply@blogger.com</email><gd:image rel='http://schemas.google.com/g/2005#thumbnail' width='32' height='29' src='//blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEgs8epYPe4xa3goLTfveQ_C5vLTl1207yOIrsIgxkIlBI5iDSFjVJFSWLsVx3BSJ1JlbVyC5e525_cMtwaUdrRMwQ6noANN_AnsnfyUeYvwIKzVLFyy4nzznFs9IyWo7FQ/s220/%E3%83%97%E3%83%AD%E3%83%95%E3%82%A3%E3%83%BC%E3%83%AB01.jpg'/></author><media:thumbnail xmlns:media="http://search.yahoo.com/mrss/" url="https://blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEid4eYnl8B6FizhWHSyumOlAtbiRNe4pc7QYbevsnBkQV3jYZ1Rjr5uFaqQvCSfkei5VJHcue-5cuz4mvCbH0LWcuFCvFZtJngKm49_EIKiQZOrxxWgbzrWnNMCjmjyWYdAYlj5UtAKuKs/s72-c/%E6%88%BB%E3%82%8B(%E5%B0%8F).jpg" height="72" width="72"/><thr:total>0</thr:total></entry><entry><id>tag:blogger.com,1999:blog-8456525132033459936.post-6386773469277071281</id><published>2010-02-12T01:01:00.001+09:00</published><updated>2010-02-12T01:16:20.817+09:00</updated><category scheme="http://www.blogger.com/atom/ns#" term="技術マップ"/><title type='text'>形式手法あれこれ</title><summary type="text">形式手法(Formal Method)と言われる分野にはおおざっぱに分けて形式仕様記述とモデル検査がある。それから、形式的開発手法というか開発プロセス的にまとめたものがある。

形式仕様記述ではVDM, Z等が有名である。モデル検査ではSPIN, NuSMV等が有名である。形式的開発手法にはB-method,RAISE等がありどれが有名と言うことはない。

VDMはツールの名前でもあるし言語の名前、あるいは記述スタイルを指して使われるが、Zは言語あるいは記法であり適当な専用ツールが無い。Zは好きだけど動かないからVDMを使う人は多い。それじゃZは使えないかと言うと事例はある。日本では使うの使わねぇのと言う段階から使えるのか使えないのかと言う議論が始まるまでに10年掛かったが、海外には成功事例も失敗事例もちゃんとある。

Zは集合論とλ計算など数学とコンピュータサイエンスの合わせ技で構成さ</summary><link rel='replies' type='application/atom+xml' href='http://tfujikura.blogspot.com/feeds/6386773469277071281/comments/default' title='コメントの投稿'/><link rel='replies' type='text/html' href='http://tfujikura.blogspot.com/2010/02/blog-post_12.html#comment-form' title='0 件のコメント'/><link rel='edit' type='application/atom+xml' href='http://www.blogger.com/feeds/8456525132033459936/posts/default/6386773469277071281'/><link rel='self' type='application/atom+xml' href='http://www.blogger.com/feeds/8456525132033459936/posts/default/6386773469277071281'/><link rel='alternate' type='text/html' href='http://tfujikura.blogspot.com/2010/02/blog-post_12.html' title='形式手法あれこれ'/><author><name>tfujikura</name><uri>http://www.blogger.com/profile/05727198324191810209</uri><email>noreply@blogger.com</email><gd:image rel='http://schemas.google.com/g/2005#thumbnail' width='32' height='29' src='//blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEgs8epYPe4xa3goLTfveQ_C5vLTl1207yOIrsIgxkIlBI5iDSFjVJFSWLsVx3BSJ1JlbVyC5e525_cMtwaUdrRMwQ6noANN_AnsnfyUeYvwIKzVLFyy4nzznFs9IyWo7FQ/s220/%E3%83%97%E3%83%AD%E3%83%95%E3%82%A3%E3%83%BC%E3%83%AB01.jpg'/></author><thr:total>0</thr:total></entry><entry><id>tag:blogger.com,1999:blog-8456525132033459936.post-9081792309693921315</id><published>2010-02-11T12:23:00.006+09:00</published><updated>2010-02-11T13:03:14.597+09:00</updated><category scheme="http://www.blogger.com/atom/ns#" term="目から鱗"/><title type='text'>USP友の会</title><summary type="text">業務系の話題だけれど、おもしろい人たちの存在を昨日知ってしまった。かなりの実績もあるという。RDBを使わずにシェルスクリプトだけで業務システムを構築する。開発費も運営費もIBMとか富士通がやる場合の1/10になるという。しかもパフォーマンスも良い。宇宙を飛ぶ怪しいムササビも良い。
データを書き足すだけで更新しない、検索しやすいようなファイルパスを設定する、書き込むデータ毎に別ファイルにする、ベースデータ以外は毎朝一から作り直すのでいつも新鮮(データの整合性が保たれる)、等々常識を覆すアイディア満載のシステム。既存のSIerは真っ青かも。

サブルーチン何か作らない。巨大なメインがあれば良い、その方が、早いから。
再利用なんかしない、似たプログラムを見つけてコピーして直して使う。クローンの何が悪いのさ
オブジェクト指向なんて要らない、インスタンスがあればいい。仕事をするのはインスタンスだ。</summary><link rel='replies' type='application/atom+xml' href='http://tfujikura.blogspot.com/feeds/9081792309693921315/comments/default' title='コメントの投稿'/><link rel='replies' type='text/html' href='http://tfujikura.blogspot.com/2010/02/usp.html#comment-form' title='2 件のコメント'/><link rel='edit' type='application/atom+xml' href='http://www.blogger.com/feeds/8456525132033459936/posts/default/9081792309693921315'/><link rel='self' type='application/atom+xml' href='http://www.blogger.com/feeds/8456525132033459936/posts/default/9081792309693921315'/><link rel='alternate' type='text/html' href='http://tfujikura.blogspot.com/2010/02/usp.html' title='USP友の会'/><author><name>tfujikura</name><uri>http://www.blogger.com/profile/05727198324191810209</uri><email>noreply@blogger.com</email><gd:image rel='http://schemas.google.com/g/2005#thumbnail' width='32' height='29' src='//blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEgs8epYPe4xa3goLTfveQ_C5vLTl1207yOIrsIgxkIlBI5iDSFjVJFSWLsVx3BSJ1JlbVyC5e525_cMtwaUdrRMwQ6noANN_AnsnfyUeYvwIKzVLFyy4nzznFs9IyWo7FQ/s220/%E3%83%97%E3%83%AD%E3%83%95%E3%82%A3%E3%83%BC%E3%83%AB01.jpg'/></author><media:thumbnail xmlns:media="http://search.yahoo.com/mrss/" url="https://blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEhPmkq7i2_FbWPUuqh_XlLBirw1ghfj130ApvKrMD0C1qWVL0yA0MC4SqmNu4ygnvOf4-gsDdXzWTPLsHg-zA3wZeR6_8S8g4yoWRABP9NB6EFb7QYZiA9LLZHO8Uz4WYgOjvY3epfriqg/s72-c/%E3%82%80%E3%81%95%E3%81%95%E3%81%B3.jpg" height="72" width="72"/><thr:total>2</thr:total></entry><entry><id>tag:blogger.com,1999:blog-8456525132033459936.post-7780302715774096980</id><published>2010-02-06T03:46:00.012+09:00</published><updated>2010-02-08T09:26:00.469+09:00</updated><category scheme="http://www.blogger.com/atom/ns#" term="テスト"/><category scheme="http://www.blogger.com/atom/ns#" term="信頼性"/><category scheme="http://www.blogger.com/atom/ns#" term="動作モデル"/><title type='text'>信頼性について-2: MTTFによるテスト</title><summary type="text">クリーンルーム手法では品質保証を目的としたテストの指標としてMTTF(Mean Time To Failure)を利用する。そして、バグ密度のような指標は品質にとっては意味がないと言っている。クリーンルーム手法はホーア理論に基づいた形式手法の一種である。

また一方、ソースコード検証ツールであるPolySpaceのWebセミナーは

プログラム検証によって発見されたソースコードのバグを100%取る必要は無い。95%ぐらいでよい。
機能テストとプログラム検証は違う。
プログラム検証をやっても機能テストは必要だ。5%の取り残しバグがあっても機能テストをパスすれば良い。

と言っている。

クリーンルームの方は、機能テストをすればプログラム検証は必要ないという言い方になっていて一見すると別のようだが、障害の有無が重要でありfaultの数は重要でないと言う点では一致している気がする。バグは欠陥(</summary><link rel='replies' type='application/atom+xml' href='http://tfujikura.blogspot.com/feeds/7780302715774096980/comments/default' title='コメントの投稿'/><link rel='replies' type='text/html' href='http://tfujikura.blogspot.com/2010/02/2-mttf.html#comment-form' title='0 件のコメント'/><link rel='edit' type='application/atom+xml' href='http://www.blogger.com/feeds/8456525132033459936/posts/default/7780302715774096980'/><link rel='self' type='application/atom+xml' href='http://www.blogger.com/feeds/8456525132033459936/posts/default/7780302715774096980'/><link rel='alternate' type='text/html' href='http://tfujikura.blogspot.com/2010/02/2-mttf.html' title='信頼性について-2: MTTFによるテスト'/><author><name>tfujikura</name><uri>http://www.blogger.com/profile/05727198324191810209</uri><email>noreply@blogger.com</email><gd:image rel='http://schemas.google.com/g/2005#thumbnail' width='32' height='29' src='//blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEgs8epYPe4xa3goLTfveQ_C5vLTl1207yOIrsIgxkIlBI5iDSFjVJFSWLsVx3BSJ1JlbVyC5e525_cMtwaUdrRMwQ6noANN_AnsnfyUeYvwIKzVLFyy4nzznFs9IyWo7FQ/s220/%E3%83%97%E3%83%AD%E3%83%95%E3%82%A3%E3%83%BC%E3%83%AB01.jpg'/></author><media:thumbnail xmlns:media="http://search.yahoo.com/mrss/" url="https://blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEid4eYnl8B6FizhWHSyumOlAtbiRNe4pc7QYbevsnBkQV3jYZ1Rjr5uFaqQvCSfkei5VJHcue-5cuz4mvCbH0LWcuFCvFZtJngKm49_EIKiQZOrxxWgbzrWnNMCjmjyWYdAYlj5UtAKuKs/s72-c/%E6%88%BB%E3%82%8B(%E5%B0%8F).jpg" height="72" width="72"/><thr:total>0</thr:total></entry><entry><id>tag:blogger.com,1999:blog-8456525132033459936.post-4942238973992073056</id><published>2010-02-04T23:40:00.017+09:00</published><updated>2010-02-08T00:39:31.281+09:00</updated><category scheme="http://www.blogger.com/atom/ns#" term="信頼性"/><title type='text'>信頼性について</title><summary type="text">品質と同じようにわかり辛いのが信頼性だ。ソフトにバグが有ると品質も信頼性も低くなることは依存はないと思うが、バグが無ければ高品質で高信頼性かというとそうでもない。仮にそうだとしてもバグの無いソフトはない、あるいはバグの無いことを証明することはできないとも言われるので、ソフトについて高品質とか高信頼性とか言うと嘘つきになって、話が終わってしまう。そんな訳だからあまり人と議論してもまともな議論にならないことが多い。もっと定量的な定義が必要である。
品質属性の一つとして信頼性があるというのが一般的なので、信頼性から考えてみたい。障害が起きるかどうかは確率的事象と考えることが妥当である。f(t)を障害が起きる確率密度関数とすると。ある時刻tまでに障害が起きる確率分布関数F(t)は以下のようになる。
障害を広辞苑で引くと「2. 身体器官に何らかのさわりがあって機能を果さないこと」と出ている。この何</summary><link rel='replies' type='application/atom+xml' href='http://tfujikura.blogspot.com/feeds/4942238973992073056/comments/default' title='コメントの投稿'/><link rel='replies' type='text/html' href='http://tfujikura.blogspot.com/2010/02/blog-post.html#comment-form' title='0 件のコメント'/><link rel='edit' type='application/atom+xml' href='http://www.blogger.com/feeds/8456525132033459936/posts/default/4942238973992073056'/><link rel='self' type='application/atom+xml' href='http://www.blogger.com/feeds/8456525132033459936/posts/default/4942238973992073056'/><link rel='alternate' type='text/html' href='http://tfujikura.blogspot.com/2010/02/blog-post.html' title='信頼性について'/><author><name>tfujikura</name><uri>http://www.blogger.com/profile/05727198324191810209</uri><email>noreply@blogger.com</email><gd:image rel='http://schemas.google.com/g/2005#thumbnail' width='32' height='29' src='//blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEgs8epYPe4xa3goLTfveQ_C5vLTl1207yOIrsIgxkIlBI5iDSFjVJFSWLsVx3BSJ1JlbVyC5e525_cMtwaUdrRMwQ6noANN_AnsnfyUeYvwIKzVLFyy4nzznFs9IyWo7FQ/s220/%E3%83%97%E3%83%AD%E3%83%95%E3%82%A3%E3%83%BC%E3%83%AB01.jpg'/></author><media:thumbnail xmlns:media="http://search.yahoo.com/mrss/" url="https://blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEjfuxCQIw52R-wB-mS24KmEqLjW1jparjBSP9c7euOFm1w-LkxvMUUbZrziASrGtktwVQAJKrXS04Il754NzxHEgBtmZZbEXo4avrrpnHuBqzPWXKQvDooJcplZYgf6TXZRW3AE20nlkzo/s72-c/1.jpg" height="72" width="72"/><thr:total>0</thr:total></entry><entry><id>tag:blogger.com,1999:blog-8456525132033459936.post-9215893815477231403</id><published>2010-02-04T22:07:00.002+09:00</published><updated>2010-08-29T14:16:45.413+09:00</updated><category scheme="http://www.blogger.com/atom/ns#" term="ツール"/><title type='text'>Prism</title><summary type="text">テクマトリクスでのPrismの説明会に参加した。Prismは、プログラムの動的解析をするツールである。
入力としては、デバッグ情報付きのオブジェクトコード、実際に実行して得たトレース情報、ソースコードである。
　マルチタスクやマルチコア環境でのチューニングやシングルコアからマルチコアに移行する際の設計支援に利用することが出来る。ソースコードを入力として利用するのでソースコードを解析するのかと思っていたら、解析対象は実行トレースであった。別々のスレッドが同じアドレスにアクセスしていたらソースコードを参照してアラートを上げてくれる仕組みである。従って、実行した部分のみが解析対象になる。排他制御が必要なのに排他制御されてないと、タイミング上実際に不具合が無くても不具合の可能性として検出する。また、アドレスを見ているので、ポインターのポインターのそのまたポインターによる参照でも検出することが</summary><link rel='replies' type='application/atom+xml' href='http://tfujikura.blogspot.com/feeds/9215893815477231403/comments/default' title='コメントの投稿'/><link rel='replies' type='text/html' href='http://tfujikura.blogspot.com/2010/02/prism.html#comment-form' title='0 件のコメント'/><link rel='edit' type='application/atom+xml' href='http://www.blogger.com/feeds/8456525132033459936/posts/default/9215893815477231403'/><link rel='self' type='application/atom+xml' href='http://www.blogger.com/feeds/8456525132033459936/posts/default/9215893815477231403'/><link rel='alternate' type='text/html' href='http://tfujikura.blogspot.com/2010/02/prism.html' title='Prism'/><author><name>tfujikura</name><uri>http://www.blogger.com/profile/05727198324191810209</uri><email>noreply@blogger.com</email><gd:image rel='http://schemas.google.com/g/2005#thumbnail' width='32' height='29' src='//blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEgs8epYPe4xa3goLTfveQ_C5vLTl1207yOIrsIgxkIlBI5iDSFjVJFSWLsVx3BSJ1JlbVyC5e525_cMtwaUdrRMwQ6noANN_AnsnfyUeYvwIKzVLFyy4nzznFs9IyWo7FQ/s220/%E3%83%97%E3%83%AD%E3%83%95%E3%82%A3%E3%83%BC%E3%83%AB01.jpg'/></author><thr:total>0</thr:total></entry><entry><id>tag:blogger.com,1999:blog-8456525132033459936.post-402684096274977459</id><published>2010-01-31T20:26:00.008+09:00</published><updated>2010-02-13T01:25:41.169+09:00</updated><category scheme="http://www.blogger.com/atom/ns#" term="設計"/><title type='text'>マルチタスク環境におけるWatchdogの設計</title><summary type="text">Watchdogタイマーは基本的にはカウンターでzeroになった時かオーバーフローした時にシステムにリセットを掛けてシステムを再スタートさせるハードウェア部品だ。組込屋さんは、PCプログラマのことをバグがあってもリセットすれば良いと思ってる見たいに偉そうに言うが、実はWatchdogはそれを自動化したものだ。やばい時にはリセットするのは変わりない。
ここでは、どんな使い方をするのかまとめてみる。組込では、RTOSを使う場合と使わない場合があるが面白いのはRTOSを使った場合である。以降はWatchdogタイマーをWDTで表す。

要件(やりたいこと)
OSやタスクの無限ループ、デッドロックの検出をする
低優先度のタスクが動けることのチェックをする
単に動くだけではなく、アプリケーションに応じて健全性チェックをする
設計(つくりかた)
WDTをkickするタスクをモニタータスク(MTask</summary><link rel='replies' type='application/atom+xml' href='http://tfujikura.blogspot.com/feeds/402684096274977459/comments/default' title='コメントの投稿'/><link rel='replies' type='text/html' href='http://tfujikura.blogspot.com/2010/01/watchdog.html#comment-form' title='0 件のコメント'/><link rel='edit' type='application/atom+xml' href='http://www.blogger.com/feeds/8456525132033459936/posts/default/402684096274977459'/><link rel='self' type='application/atom+xml' href='http://www.blogger.com/feeds/8456525132033459936/posts/default/402684096274977459'/><link rel='alternate' type='text/html' href='http://tfujikura.blogspot.com/2010/01/watchdog.html' title='マルチタスク環境におけるWatchdogの設計'/><author><name>tfujikura</name><uri>http://www.blogger.com/profile/05727198324191810209</uri><email>noreply@blogger.com</email><gd:image rel='http://schemas.google.com/g/2005#thumbnail' width='32' height='29' src='//blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEgs8epYPe4xa3goLTfveQ_C5vLTl1207yOIrsIgxkIlBI5iDSFjVJFSWLsVx3BSJ1JlbVyC5e525_cMtwaUdrRMwQ6noANN_AnsnfyUeYvwIKzVLFyy4nzznFs9IyWo7FQ/s220/%E3%83%97%E3%83%AD%E3%83%95%E3%82%A3%E3%83%BC%E3%83%AB01.jpg'/></author><media:thumbnail xmlns:media="http://search.yahoo.com/mrss/" url="https://blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEhm9dZ7GtGf0eNr0ekwm2smSII34GXhuc-vurSBa0ZFVd_Uc1zkROJFb40se1evJa5sW0ufZgwhcmPWoiwn5MgMw8wQiV_V37xZIL6zeUoLRglPVpX0MU4QwktoO_LdqpPOafi75gqmDYo/s72-c/%E7%B6%99%E7%B6%9A(%E5%B0%8F).jpg" height="72" width="72"/><thr:total>0</thr:total></entry></feed>