作成した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言語などの高級言語で主に開発しました。