6つのテーマを同時並行作業

現在6つのテーマを同時並行で作業しています。

いずれのテーマもある程度作業の目途がつき成果もでてきました。

6つのテーマは全く違いますが、共通していることは「数学的・科学的アプローチ」と「自動処理」です。

今後ブログで作業進捗や内容を紹介していくたいと考えています。

すっかりご無沙汰してしましました

このブログもすっかり更新をさぼってしまいました。

最近はSNSはあまりやらずにいました。

とわ言え、これからは実世界ではなく、サイバー空間が生活やビジネスの中心的な場になることは間違いないので、コミュニケーションの場としてSNSのようなものは確実に深く浸透するでしょうね。

AIやＩｏTの時代は、勉強や仕事および人間の生活を大きく変えることは、日本人でも誰でも理解しているのに、「働き方改革」などの議論をみると現状の仕事の考え方に引きづられていますね。

CCCC(C AND C++CODE COUNTER)GUIランチャーの公開

"CCCC - C and C++ Code Counter" version 3.1.1（オープンソース）のフロントエンドとして機能するGUIランチャーを公開しました。

このランチャーの紹介とダウンロードは下記です。

http://hsc-i.com/HSCI_Tooldownload.html#CCCC(C AND C++CODE COUNTER)GUIランチャー

作成したYicesのGUIからオプションを変えSMTを行う

『Yices』でSMTを行う際にオプションが幾つかあるが,それを変更してSMTをしました。
 
スクリプトを組むだけでなく,モデルから検証対象内容を変換させてSMTにかけることもできますので,次回実施する予定です。

『Yices』によるSMTソルバ

YicesによるSMTソルバを使った作業の効率化のためにGUIインタフェースを作成中ですが,ドラフト版1号が出来上がってきました。

『安全性工学』『レジリエンス・エンジニアリング』と『数学的直観主義・構成主義』

昨日東京大学においてErik HOLLNAGEL教授の『レジリエンス・エンジニアリング』の講義を聞きいてる最中にふと,『数学的直観主義・構成主義』が頭をよぎりました

Erik氏によると従来の安全性解析の考え方は『Safty-I』と呼ばれ,つまり『事故が起き無い==安全が保たれる』という考え方が根底にあると強調しています。

大げさに言えば,過去の事故である有限の事象を解析し(安全な事象は直接には注目しない),まだ発生していない無限の事象の安全性を担保したいという考えです。

一方、『レジリエンス・エンジニアリング』は『Safty-Ⅱ』のアプローチであり,安全が保たれている大多数の事象に直接注目し,安全とは何か？どういうことであるのか？と安全な事象を直接解析するアプローチです(事故の解析も行う)。

従来の品質保証活動や信頼性・安全性解析技の殆んどは,『Safty-I』のアプローチに該当します。

ここで『数学的直観主義』あるいは『数学的構成主義』ですが,無限集合を考える時に背理法の規則を用いて非存在が成立しないことを利用した推論技法により,存在を示すこを禁じています。

別の言い方をすると,排中律に対して厳しい態度をとる主義です。

確かに無限を扱う時に,その直接の対象を扱わず非存在を証明することで,存在を成立させることは違和感があります(素数の存在証明など)。

素数の存在自体を直接証明していなので,素数の存在を構成的に説明することができていません。

素数の存在証明には,それ自体「素数がどの様に存在しているのか」という直接の問いが含まれている感じがします。

しかし,背理法はこの点に何も答えてくれません。これで素数の存在証明になるのかということは誰でも思います。

『Safty-I』のアプローチが過去の事故である有限の事象からまだ行い無限の事象の安全性を担保するというには,「￢事故=安全」で背理法的な印象を与えます。

『レジリエンス・エンジニアリング』の『Safty-Ⅱ』のアプローチが『数学的直観主義』あるいは『数学的構成主義』と何となぁ～く類似点を感じました。

今日の東京大学でのセミナーの整理と考察

今日の理論と事例の中で、とても良いヒントや応用面のイメージが湧いたものがありました。

また一度に聞いたDeeplearningの隠れ層のニューロンにマルコフ連鎖を適用し変換することで、formalVerificationを行う話しも検討する事を忘れていた話題もありました。
先月聞いたばかりでしたが、年末年始で忙殺され、すっかり失念していました。

それから別の技術問題には過去にやったAIの経路問題が使えそう。

また、非線形の変化には遺伝アルゴリズムがいけるかもしれないのは、制御系の分野も同じだと思うので、かなり遺伝アルゴリズムから遠ざかっているので思いだしながらまだできるかな。

ペトリネットツールでシミュレーション実行と安全性判定の概念

久しぶりに以前使ったペトリネットツールでシミュレーション実行したいと思い,適当に作成してみました。
　
操作性や速度の確認などの確認です。
　
思った以上に操作性は良く,シミュレーションもサクサク動きました。
　
シミュレーションモードのアニメでは、発火後の遷移とトークンの変化が良く観察できます。
　
ペトリネット自体は単純なものなのですが,色々な数理的意味づけが行えるために,発火や遷移の安全性判定の概念を盛り込むことができます。
　
行列式への変換は機械的に行えるので,ツールで自動変換できればかなり作業がはかどりそうです。

東京大学に来ています

今日は午後一杯は東京大学です。

晴れているのでさほど寒く感じません。

ロケット発射＆制御システムの例題とミサイル制御システムのプログラム開発

正月明けそうそうオフィスの整理です。
　
まずは書籍や資料の整理をしています。
整理のなかで出てきたのが、学校を出て最初に社内教育で使ったテキストです。
　
社内教育ですから教師は先輩や上司ですが、宇宙・防衛分野の皆エキスパートです。
　
私が学校を出て鎌倉製作所で開発をし出した頃は、レーダー制御や目標の優先度判定処理、追尾目標の外挿計算処理を開発する仕事が主でした。　
　
そのうち4面フェーズドアレイの様な追尾目標の外挿計算処理が不要な追尾レーダー&射撃レーダーを兼ねた新型レーダーも登場してきたし。。。
　
テキストの内容よりも業務の実践の方が、はるかに高度で極めて複雑でしたので、いつも分からないことだらけでした。
　
先輩や上司はロケットやミサイル発射＆制御システムはアセンブラでプログラムしていました。
　
私は先輩や上司が過去に開発したプログラムに、機能追加でアセンブラでパッチを当てる作業もありましたが、インストラクション表を使い、ハンドアセンブルなどしながらやはり面倒だったですね。

その後、私はAda言語やC言語などの高級言語で主に開発しました。

CMMI & Agile

本日、CMMI  Instituteからメールで連絡がありました。

資料は結構ボリュームがあります。

どのように取り組むのかが、プロセス領域毎に解説されています。

有界モデル検査ツールのGUI２

作成中の有界モデル検査ツールのGUIで対応するオプションが増えました。

このツールはCUIなのでオプションの入力が面倒でしたが、また効率的に行えるようになりました。
　
まだ色々作り込む予定ですが、機能性＆利便性が向上しました。

変動を扱う分析手法

周波数、確率変動、共鳴およびノイズなど従来の分析手法では使わない要素を用いて安全を解析するアプローチを使用するために準備です。
　
従来の根本原因分析アプローチでは効果が弱い、意味がない解析対象に対して幾つかの解析技法を用いる際の1つとして使います。

MITの先生による講義@九州大学

今日の大半はMITの先生によるモデリングの講義でした。
有益な情報が入手出来ました。

有界モデル検査『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でもある程度代用することが可能です。