『科学的モデリング』による『科学的MDA』アプローチ~モデルの「充足性(Satisfiability)」「適用可能性(Applicability)」「正当性(Correctness)」「妥当性(Feasibility/Validity)」
『科学的モデリング』による『科学的MDA』アプローチ ~モデルの「充足性(Satisfiability)」「適用可能性(Applicability)」「正当性(Correctness)」「妥当性(Feasibility/Validity)」
人工知能やSATソルバエンジンなどの進歩で、モデルの「充足性(Satisfiability)」「適用可能性(Applicability)」「正当性(Correctness)」などを持つ自動検証とコード生成が可能になってきた。
『科学的モデリング』では、その必然的帰結として『科学的MDA』アプローチになる。
お絵かきモデルから脱却するには、モデルの作成はもちろんMDA(モデルドリブン開発)でも「充足性(Satisfiability)」「適用可能性(Applicability)」「正当性(Correctness)」「妥当性(Feasibility/Validity)」について真正面から向き合わないといけない。
実際に、国際規約で「充足性(Satisfiability)」「充足性(Satisfiability)」「適用可能性(Applicability)」「正当性(Correctness)」「妥当性(Feasibility/Validity)」」で重要視されている。
そうしないとエンジニアリングではない。分析や設計すべき重要事項が完全に欠落していまう。
『科学的MDA』アプローチは、「充足性(Satisfiability)」「適用可能性(Applicability)」「正当性(Correctness)」「妥当性(Feasibility/Validity)」が全く考慮されていない単なる「お絵かきモデル」から自動コード生成をするMDAとは異なり、リファイメント(Refinement)の考えを自動あるいは半自動で実現するアプローチとなる。
リファイメントは、下向き模倣(Down Simulation)と前向き模倣(Forward Down Simulation)あるいはその併用やいくつかの課題があるが、「抽象化関数(Abstruction Function )が求めることで、上位フェーズのモデルと下位フェーズのモデルの対応関係が数学的に行える。
まぁ、理想的にはいかない部分もあるが、このようなリファイメント(Refinement)の考え方や自動検証の知識は不可欠と思う。
分析、設計および実装の開発速度と品質が大きく異なるからである。
| 固定リンク
「パソコン・インターネット」カテゴリの記事
- 6つのテーマを同時並行作業(2019.07.05)
- すっかりご無沙汰してしましました(2018.05.27)
- CCCC(C AND C++CODE COUNTER)GUIランチャーの公開(2017.04.13)
- 作成したYicesのGUIからオプションを変えSMTを行う(2017.01.19)
- 『Yices』によるSMTソルバ(2017.01.18)
最近のコメント