記事
設計検証を、装置エンジニアの言葉で
形式手法の最大の障壁は、難しさではなく馴染みのなさです。専門家130名への調査では、71.5% が「エンジニアの教育不足」を採用の最大の障壁に挙げました。だから私たちは、売り込みの前に説明を置きます。
順番に読めば、装置ソフトウェアの検証の空白から、それを形式手法がどう埋めるかまでが一本につながるように書いています。どこから読んでも構いません。
-
なぜ装置ソフトウェアは、V字モデルの右半分を実行できないのか
装置開発の現場が「動けば OK」で数十年やってこられたのは、手を抜いたからではありません。単体テストが物理的に成立しない構造だったからです。
-
「モデルで設計する」の次に来るもの
世界はすでに文書ではなくモデルで設計しはじめています。しかし、そのモデルが正しいかどうかは、どのツールも答えていません。その空白の話です。
-
テストと形式手法は、何が違うのか
テストは試した範囲を確かめ、形式手法は起こりうるすべての状態を確かめます。その差が効くのは、テストでは出ずに現場で出る一群のバグです。
-
反例とは何か
設計検証が問題を見つけたとき、返ってくるのは警告ではなく、違反を再現する具体的な事象列です。それを現場でどう使うかを書きます。
-
なぜ安全規格は、形式手法を求めるのか
形式手法は新しい売り込みではありません。IEC 61508 も DO-178C も、安全等級が上がった先で形式手法を挙げています。その理由を書きます。
-
誰が、実際に使っているのか
形式手法を実際に使っている組織と、その使い方を挙げます。あわせて、普及がどこまで進んでいないかも、そのまま書きます。
-
現場から実際に来る質問
「形式手法を導入したい」から始まる相談は来ません。来るのは、すでに起きた出来事についての質問です。よくいただく八つと、それぞれに何をお返しするかを書きます。
御社の設計で、確かめてみませんか。
記事は一般的な説明です。御社の装置で実際に何が出てくるかは、対象をひとつ決めれば分かります。