有界モデル検査『CBMC』のGUI

有界モデル検査のツールであるCBMCは,コードを解析する際にとても有用です。

しかし,オリジナルのCBMCはCUIベースであり,かつ,オプションスイッチが多いためにやや利便性に難があります。

そのため,CBMCをGUIを通じて;

• 「解析対象のコードの設定」
• 「オプション設定」
• 「解析結果の保存」
• 「解析結果の表示」
• 「解析作業に必要な各種設定」
• など

GUIを通じてできるようにします。

PSPの『ProcessDashboard』を更新した

正規にはβ版となっているが最新の『ProcessDashboard』に更新しました。

Carnegie Mellon Universityで開発・管理された『ProcessDashboard』は,『科学的システム開発』には重要なツールですが,今回の更新に伴いプロセス定義とサンプリングデーターの見直し行います。
　
データー解析はツールが自動的に行うが,解析結果をフィードバックする上で事前のゴール設定と評価基準の定義が大切です。

『特許証』が特許庁から届いた

『特許証』が特許庁から届きました。

『Event-B Day』のworkshop

国立情報学研究所(NII)@学術総合センターに来てます。

形式手法であるEvent-Bの『Event-B Day』のworkshopが開催されています。
　
参加者のほとんどが外国人で世界中から研究者がきていますが,UKとFranceの方が多いです。
　
アジェンダ(スケジュール)は下記です。
http://research.nii.ac.jp/eventb2016/

Eclipseでのモデリングを環境を確立

JVMを一新してEclipseでのモデリングを環境を確立しました。
 
これまで問題があって使えなかったProfileや自動処理機能を利用できるようにセットアップしました。
　
UMLやSysMLは最新のノーテーションであることは勿論、DSLも幾つか利用出来ようにしました。

IoT&M2M時代のSysMLによる『ハザード分析』&『安全性解析』 のモデリングの重要性

今日は鉄道の制御のIEEE1474国際標準と CBTC(Communications-Based Train Control)について調査し,SysMLによる『ハザード分析』&『安全性解析』のモデリングの予備調査を行いました。
　

今日の焦点は『コントロール・ストラクチャ』と『コントロール・アクション』のモデリングです。
　

世界の事例の資料を参照し,ミッションクリティカルなシステムの『ハザード分析』&『安全性解析』 のモデリングのノウハウを参考にしました。
　

IoT&M2M時代は,『ハザード分析』&『安全性解析』 のモデリングの重要性は増しています。
　
従来であればミミションクリティカルな分野でしか見かけない『ハザード分析』&『安全性解析』 のモデリングの話題でしたが,エンタープライズ系にも適用の傾向が表れ始めています。

日本ではモデルベースの開発やアーキテクチャ分析・設計に議論が多くなりがちが,ISO,IEEE,IECなどの国際規約をまず満たす事を保証しないと話になりません(満たさないと門前払いのケースが多くなってきいています)。

そのため、制御系の『モデル駆動開発』では,要件定義,安全性解析,アーキテクチャ設計,検証など作業についてモデルの成果物を作成を開発当初から意識して行っていきます。

『ハザード分析』『安全性解析』のモデリングや作業は,かなり大変ですが,さらに最近は『アシュアランスケース』についても要求が厳しくなってきていますが,このモデリング作業も大変な作業です。

『ハザード分析』 &『安全性解析』 のモデリングかなり専門的な作業かつドメインの経験・知識が求められる上に,作業にかなり時間がかかります。
　

FTA,FMEA,HAZOP,STAMP/STPAなどなどは独自のノーテーションを定義していますが,SysMLでもある程度代用することが可能です。

『安全性解析』のモデリング作業～『アシュアランスケース』や『安全性解析』が大切

制御系のシステム加発では必至となりつつある『安全性解析』のモデリングの作業と調査をしています。
まだまだ作業途中です。

開発において要求定義も従来の方法だけでは不足で,『アシュアランスケース』や『安全性解析』の観点から,システムに求められる(逆に発生しては困る事項や避けなければならない事項)ことを定義していくことが必要です。

SysMLによるアーキテクチャ分析・設計とアーキテクチャの性能検証作業

コンポ―ネントの振る舞い性能やタスク／スレッドのスケジューリング性能解析です。

astah*SysMLとastah*UMLのプラグインを設定しました

SysMLとUMLによるモデル駆動開発のモデル開発のために,astah*SysMLとastah*UMLのプラグインを設定や更新をしました。

astah*SysMLとastah*UMLは操作性のフィーリングがとても良いです。
　
海外製のモデリングツールにありがちなLook&Feelのストレスが無いためにモデリング作業の負担が少ないです。

『SysML／UMLモデル』の正当性～ シミュレーションとモデル検査

SysMLで作成したモデルを普段使っているGUIを割けてCUIで作業しました。

色々なタイプのモデルを検査しますが,まずは最も単純なパターンからです。この後は色々な性質を条件として付加して作業です。

CUIならどのような環境でもモデルシミュレーションとモデル検査が可能なので作業場所や作業環境に影響を受け無いからですが,それでもバージョンや付けたオプションの違いを意識する必要があります。

ちなみにモデルのシミュレーションとモデル検査は異なります。

モデル検査をする場合は、モデル検査用の言語をC言語に変換し,gccでコンパイルして実行しますので,異なるコンパイラやそのバージョンおよびオプションの違いも気を付けます。