SysML/UMLの状態図(StateMachine)をModelicaでモデルコンパイル&シミュレーション

SysML/UMLの状態図(状態マシン)をModelicaでモデルコンパイルしました。
　
この状態図(状態マシン)をグラフ化するとこうなるのですね。

状態図(状態マシン)のシミュレーションですが、

状態図は元をただせばノードとアークによる抽象表現なので、何らかの情報を離散的に表現する場合に利用できます。

このメリットを利用して検証対象を抽象化してノードとアークの状態図で形式化できるならツールでシミュレーション可能という発想ですね。

メトリクス計測ツール『cccc』のGUIを作成

メトリクス計測ツール『cccc』は『SourceMonitor』と異なり
CUIなのでGUIで作業したくなる時があります。
　
オプションなどもGUIで手軽にON/OFFできると便利です。
　
そこでccccを呼び出すGUIを作成しました。
U氏ありがとうざいます。
　
優れたプログラム作成やテスト容易性のためにはプログラムのメトリクスやテストカバレッジが重要です。
　
数値による定量化は科学的アプローチの基本の１つです。

《振る舞い(意味)レベル》で安全な『サブシステム』と『コンポ―ネント』の再利用と機能拡張を自動計算する

一般にはあまり知られていないようですが、『サブシステム』と『コンポ―ネント』にも振る舞いレベルの型を《表明》を使って割り当てられることができます。

今回、モデリングツールで演繹推論を使い、振る舞い(意味)レベルで安全な『サブシステム』と『コンポ―ネント』の再利用と機能拡張を自動計算する方法を実装しました。
　
この機能により、単にインターフェースのシグネイチャレベルでは無く、振る舞いレベルで『サブシステム』と『コンポ―ネント』安全な再利用と機能拡張を自動計算ができます。
　
『サブシステム』と『コンポ―ネント』は、C言語とC++言語で自動コード生成させています。
　
ちなみに、クラス間の意味的な置換可能性(安全な再利用)は,
《Plug-In》
という論理式で基本は計算を自動計算を行います。
再利用や拡張に居て一定の制限を掛ければ他の式でも安全性が保障できます。
　
『サブシステム』と『コンポ―ネント』の置換可能性(安全な再利用)と機能拡張では、
《Plug-in Compatibility》
という論理式で計算を自動計算を行います。

異なる式で自動計算する理由は、再利用や機能拡張の安全性を保証する上で考慮する事が異なるからです。

Open Modelica

モデル駆動開発の”モデル”には色々なものがあり得ます。

物理系のシステムでは、Modelic仕様を使うモデリングが多くなりますが、Open Modelicaを試しています。

C++コードの『静的解析』作業

色々なコードのパターンを用意して解析作業。
ツールが解析でどこまで警告がされるかチェックしています。

分析・設計で数理的な形式手法の技法やツールを使っても、まだまだコード解析ツールによる解析は重要です。
結構地味な作業ですが効果的です。
　
『科学的モデル駆動開発』としてソフトウエア工学による科学的な手法・技法による作業を連携して自動化する方法を構築中です。
　①定理証明系の考えを使いた機能を持つツールでモデリング
　(①'クラスやコンポーネントの再利用や拡張も演繹推論的技法で意味的な整合性を保証して自動化が可能になる)
　②モデル検査(orシミュレーション)で正当性を自動検査
　③妥当性や正当性が確認されたモデルから自動コード生成
　④静的解析ツール群のよる解析
　⑤動的解析ツール群による解析

下流のビルドからテストまではJenkinsなどで統合が可能ですし、有効なのです。

今回の作業は欧米的な数理的な形式手法を効果的に取りいれた分析・設計からコード解析までの自動化です。

初秋の読書～SpinやPromelaによる『コンピュータープロトコルの設計法』

秋近しということで,時間のあるときに読もうと思う本を本棚からとってきました。

やや古い本ですが、とても役に立ちます。
　
600ページの大書ですが、論理式などの数式も登場し,内容の密度が濃く専門的なので、1000ページくらいの本を読むつもりで、ジックリ読む意識が必要かもしれません。
　
よって、かなり時間がかかります。
　
本書はSpinやPromelaが誕生したきっかけとなったプロトコルの設計と検証について書かれていまです。

しかし、SpinやPromelaの解説書そのものではなく、コンピュータープロトコルの様な複雑なシステムの設計や検証をどのように考えるのかということを詳細に述べています。
　
気長に読む必要があります。

クラスだけでなく、サブシステム、コンポーネントの処理の意味的整合性規則の自動計算と表示

定理証明系の規則である表明(クラス不変条件,メソッドの事前／事後条件)を、クラスだけでなく、サブシステム、コンポーネントにも適用できるようにしました。

論理式で記述し、自動計算させる仕様ができました。
ツールでの表示はまだですが、従来ツールで「型継承の規則」としているラベル名を「型適合規則」に変更します。
「仕様適合判定規則」というラベル名はそのままであり変更なしです。

今回は、以前から計算＆表示が可能であった、サブシステム、コンポーネントのインターフェースやポートの表明に加え、例外適合条件も自動で計算&表示できるようにすることです。
 
これにより継承関係がないクラス間同士、サブシステム間同士、コンポ―エント同士の再利用や交換の判定が適用できるようになりました。

これは、最近のOO言語では型の同型を判断するために継承関係を必要としない原理と同じです。
 
振る舞いの意味的条件(表明etc)を厳密に型情報を定義し、型の同等性を判定することで可能になります。
型の考えをサブシステム、コンポ―エントあるいはモジュールにも適用させることで可能になります。
 
非OOADで作成するサブシステム間同士、コンポ―エント同士あるいはモジュールの機能＆例外の再利用や交換の判定も同じです。
 
C言語ではC++のような例外メカニズムを実装するのはなかなか大変なので(スタックの巻き上げなど)、C言語でOOADやOOPを実装するときでも従来的な例外処理の延長線上のメカのズムを使うことが多いですが、この場合も自動計算させる仕様を定義しました。
 
なお、クラス、サブシステム、コンポーネントの再利用や交換において例外宣言や定義が一致するかどうかは、事前／事後条件ではなく、純粋な例外包含関係の十分条件が成立しているかどうかの論理式で記述し、自動計算させます。
 
これにより安全確実でクラス、サブシステム、コンポーネントの再利用や交換が可能になりました。
 
ただし、並列性があるクラス、サブシステム、コンポーネントの再利用や交換の判定条件を追加する作業があります。

Linux&EclipseでのC/C++開発

EclipseというとJavaやPHPなどIT系の開発のイメージが強かったと思います。
　
でも、私も最近はLinuxでEclipseを使いC/C++開発を行うことが多くなってきました。
　
この傾向は強まっていくと思います。
　
Eclipseのプラグインとして提供される各種機能や,LinuxにインストールするJenkins、GitおよびGoogleTestなどのプロセスの統合が簡単だからです。