設計を、正しさを問える形にする
装置ソフトウェアの基準は設計です。しかしその設計は、多くの場合、自然言語と熟練者の頭のなかにあり、正しいかどうかを問える形になっていません。問える形にするところから始めます。
DatumProof について
DatumProof は、自動化装置の設計を実機ができる前に検証する会社です。このページには、なぜこの問題なのか、どういう原則で仕事をするのか、そして 何をしないのかを書いています。
出発点の問い
制御している物理システムがそれほど複雑でないなら、なぜ制御ソフトウェアは、これほど理解しにくく、直しにくく、検証しにくくなるのか。
答えは、装置が複雑だからではありません。要求・システムの挙動・異常処理・検証条件・過去の設計判断が、明確で実行可能な形で表現されていないからです。表現されていないものは、確かめられない。確かめられないものは、実機が動くまで分からない —— それが、装置ソフトウェアの検証が最後まで先送りされる理由です。
この構造については、なぜ装置ソフトウェアは、V字モデルの右半分を実行できないのかで詳しく書いています。
仕事の原則
装置ソフトウェアの基準は設計です。しかしその設計は、多くの場合、自然言語と熟練者の頭のなかにあり、正しいかどうかを問える形になっていません。問える形にするところから始めます。
「ツールがそう言っています」は、装置の現場では通用しません。指摘は、設計レビューにそのまま持ち込めるイベント列として返します。人が読んで判断できないものは、成果物として不十分だと考えます。
設計検証は万能ではありません。検証するのは設計であって、組み上がった実機ではない。モデルは抽象であり、抽象の選び方には限界がある。できることより先に、できないことを説明します。
しないこと
新しい手法の話でいちばん警戒されるのは、「では、いまのやり方を全部変えるのか」という点です。答えは、いいえです。
既存の PLC 開発や制御ソフトの作り方には手を入れません。検証は、いまの開発の横に並べて始められます。
配線、組み立て、実際のモータの応答 —— 実機でしか確かめられないものは、テストの仕事のままです。検証とテストは別の問いに答えます。
私たちが返すのは検証の結果であって、コードではありません。設計が正しいかどうかを、低い負担で確かめられることに絞っています。
立ち位置
世界はすでに「モデルで設計する」方向へ動いています。そのうえで、モデルをつくることと、そのモデルが正しいと証明することは、別の仕事のまま残されています。
DatumProof はモデルをつくる道具と競合しません。その上に載る検証の層です。装置業界にこの層がまだ無いこと —— それが、この会社が存在する理由です。
原則
装置ソフトウェアは、明示的なモデルと文書化された設計意図から、理解でき、検証でき、修正できるものであるべきだ。
現在の状況
DatumProof は設立準備中です。会社の登記情報は、手続きの完了後にこのページへ掲載します。
お問い合わせやご相談は、いまの段階でもお受けしています。
御社の装置で、いま何がいちばん痛いか。そこから始めます。