387 Views
September 15, 23
スライド概要
大学連携セッション「計算機科学に基づくソフトウェア工学」
伊藤 宗平 氏(長崎大学 情報データ科学部 准教授 )
2023年9月15日(金)に出島メッセ長崎にて「7th長崎QDG」を開催しました。
ご講演者より許可を頂いた資料につきましてNaITEにて公開いたします。(公開版資料は当日版資料と内容が異なっていることがあります)
★7th長崎QDG
https://nagasaki-it-engineers.connpass.com/event/263690/
★NaITE(長崎IT技術者会)
https://naite.swquality.jp/
NaITE(長崎IT技術者会)です。 イベントや勉強会の資料を公開していきます! ★NaITE(長崎IT技術者会) https://naite.swquality.jp/
計算機科学に基づく ソフトウェア⼯学 ⻑崎⼤学 情報データ科学部 伊藤 宗平 7th ⻑崎QDG
計算機科学(Computer Science)とは? Edgar Dijkstraの説明 Computer Science Is Not About Computers, Any More Than Astronomy Is About Telescopes (天⽂学が望遠鏡に関する学問でないのと同様に、計算機科学はコンピュータに関する学問ではない) • 本来の意味での「計算機科学」は、「計算」という概念を数学 的に探究する学問 • 現代では「理論計算機科学」と呼ぶ⽅が適切
計算機科学に基づくソフトウェア⼯学 • 計算の数学的扱いに基づいたソフトウェア⼯学のこと • 形式⼿法 (Formal methods) と呼ばれる。
なぜ「計算」という概念を数学で考える ようになったのか? • 数学といえば… • • • • ⽅程式の解を求めよ 〜な点の座標を求めよ 図形〜の⾯積を求めよ etc. • このように、19世紀ごろまでは何かを計算で求めるのが数学 だった。
が有理数となる無理数 は存在するか? 存在する。 証明. 2 は有理数か無理数であるかのどちらかである。 有理数であれば𝑥 2, 𝑦 無理数であれば𝑥 2 ,𝑦 2がその証拠である。 2がその証拠である。(Q.E.D.) しかし、具体的な𝑥, 𝑦は求められていない。
数学の論法 • 排中律(𝐴または 𝐴のどちらかは真) • 背理法( 𝐴と仮定すると⽭盾するので𝐴は正しい) のような論法を⽤いると、解が存在することは証明できても、具 体的な解を求める⽅法は与えられない。 19世紀末、解を求める⼿順は存在するか?ということが数学者 の関⼼を引くようになった。 => すなわち、アルゴリズムの存在性
ヒルベルトの第10問題 • 整係数多変数⾼次不定⽅程式が整数解を持つかどうかを決定す る⼀般的な解法を求めよ。 • 1900年、国際数学者会議にて • 以降、あいまいだった「アルゴリズム」という概念について数 学者たちが考えるようになった。
計算についての数学的定義 • クリーネらは「帰納的関数」を計算の数学的モデルとして提案 • チューリングらは「チューリング機械」を計算の数学的モデル として提案 • 両者は奇跡的に(?)⼀致することが判明 • 他にも様々な計算のモデルが提案されたがすべて⼀致 • じゃあこれをもって「計算可能」ということにしよう! • チャーチ・チューリングの提唱
チューリング機械 • テープと有限制御部からなる … (i) テープは読み書きできる (ii) ヘッドは左右に動くことができる • 1ステップ動作は以下の通り 有限制御部 (a) テープのヘッドの下の記号を読み、 (b) 状態を変え、 (c) ヘッドの下の記号を書き換え、 (d) ヘッドを1コマ右または左に動かす。 • 状態変化、書き換える記号、ヘッドの移動⽅向は(a)で読んだ記 号と現在の状態で定まる。
チューリング機械の停⽌性 • チューリング機械が必ず停⽌することが望ましい。 • 無限ループに陥らない 定理. チューリング機械𝑀に⼊⼒𝑤を与えた時に停⽌するかどうかを判 定するアルゴリズムは存在しない。 • ある問題を解くアルゴリズムが存在しない場合、その問題は決 定不能であるという。
チューリング機械の等価性 定理. チューリング機械𝑀 と𝑀 が同じ⼊⼒に対し必ず同じ出⼒を返す かどうかを判定するアルゴリズムは存在しない。 • その他、様々なチューリング機械の解析問題は、決定不能 • チューリング機械=プログラム • すなわち、プログラムの正しさの判定をプログラムで⾏うこと はできない。 もっと単純な計算モデルが望ましい!
もっと単純な計算モデル • 有限オートマトン • ωオートマトン • 時間オートマトン • ハイブリッドオートマトン
有限オートマトン • 投⼊⾦額がちょうど200円かどうか判定するオートマトン 受理 状態 100円 0円 50円 50円 200円 100円 50円 50円 100円 100円 50円 50円,50円,100円 -> 受理 50円,100円 -> 不受理 150円 • このように、有限列がある条件を満たしているかどうかの判定 を⾏うことができる。
無限列の性質 • 𝑎𝑏𝑎𝑏𝑎𝑏𝑎𝑏 …や𝑎𝑏𝑎𝑏𝑏𝑎𝑏𝑎𝑏𝑎𝑎𝑎𝑎𝑎𝑎 …など、無限⻑の列の性質も 判定したい場合がある。 • 無限列𝑤は𝑎と𝑏を交互に繰り返すか? • 無限列𝑤は途中から𝑎だけになるか? 出⼒ ⼊⼒ Reactive System • 停⽌しない計算のモデル化に使える • リアクティブシステム • 環境からの⼊⼒に適切に応答し続け、基本的に停⽌しない • 例)OS, エレベータ、原⼦⼒発電所の制御システム、⾃動運転 環境
ωオートマトン • Büchiオートマトン • 受理状態を無限にしばしば通る列を受理する b a a s0 s1 b aが出現したら必ずbが出現する無限列を受理するBüchiオートマトン • 受理条件の設定により様々なωオートマトンがある • Mullerオートマトン • Rabinオートマトン, etc.
時間オートマトン • 有限オートマトンにクロックを追加したもの • アクション遷移(ロケーションの遷移) • ディレイ遷移(同じロケーションに留まるが時刻だけ経過) • の2通りがある。 2つのプロセスの 並⾏合成
時間オートマトンの動作 (off, y=0) (off, y=10) ディレイ遷移 10秒滞在 (low, y=0)→(low, y=3) アクション遷移 press ディレイ遷移 3秒滞在 (bright, y=3)… アクション遷移 press
ハイブリッドオートマトン • 有限オートマトンの状態(ロケーション)の内部で連続的に変 数の値が変わっていくシステム • 時間オートマトンでいうところのディレイ遷移のさなかに、時間とと もに変化していく変数がある。 • アクション遷移(離散遷移)も可能。 • ロケーション遷移 • 離散ダイナミクスと連続ダイナミクスの両⽅を持つので、ハイ ブリッドオートマトン
例)部屋の暖房システム 𝑈 𝐿 温度センサ 制御器 ON/OFF 制御器はヒーターの電源を制御する。 部屋の室温を𝐿と𝑈の間に保つのが⽬的
暖房システムの制御器 𝑙 𝑥 𝑈 𝑥 𝑦 𝐿 𝑥 𝑘𝑥 0 𝑥 ON 𝑥 𝑙 𝐿→𝑦≔0 𝑈∨𝑦 𝑥 500 𝑥 𝑘 ℎ 𝑥 𝑦 1 𝑈 ∧ 𝑦 500 OFF ヒーターオフ 𝐿 10, 𝑈 30 の場合の𝑥の変化 ヒーターオン
形式⼿法: 計算機科学に基づく⼿法 • ソフトウェアの振る舞いを形式的(数学的)にモデル化 • 数学的に厳密な⼿法で検証を⾏う • モデル=オートマトンなど • 要求される性質=論理式、理想的な振る舞いのオートマトンな ど • 仕様書や設計の段階のバグを検出できる! • 機械的・数学的に安全性が保証される
形式⼿法(Formal methods) • ソフトウェアの正しさを保証するための技術の総称。 • 厳密な(formal)⾔語で対象を記述し、その性質を数学的に証 明する。 従来の開発プロセス 要求仕様 設計仕様 ソース コード 実⾏コード 形式化 モデリング 検証性質 (時相論理式等) 設計モデル (状態遷移系等) 設計検証 ⾃動/マニュアル コード⽣成 形式⼿法適⽤プロセス(設計検証の場合)
形式⼿法の適⽤事例 • 鉄道 • パリ、北京、サンパウロ、ニューヨーク地下鉄 • シャルルドゴール空港内シャトル • ICチップ・ICカード • Felica • クラウド • Amazon AWS • など
研究紹介 • リアクティブシステムの仕様検証効率化 • ロボットカーの速度制御装置検証
リアクティブシステムの仕様 検証効率化
リアクティブシステム • 環境と相互作⽤を⾏い、⼊⼒に対 し適切に応答し続けるシステム •例 • • • • エレベータ クルーズコントロールシステム 原発の制御システム 航空管制システム ⾼い安全性が求められる セーフティクリティカルシステム 安全性を厳密に保証することが望ましい 環境 応答 ⼊⼒ リアクティブ システム
リアクティブシステムの仕様検証 • 仕様を厳密な(形式的な)⾔語で記述 • 数学的⼿法で仕様に問題がないか検証 • 良く⽤いられるのは… エレベータシステムの仕様のLTL記述例 • 線形時相論理(LTL) → 𝐅𝑑𝑜𝑜𝑟 ∧ 𝐆 𝑝𝑢𝑠ℎ → 𝑑𝑜𝑜𝑟 𝐆 𝑝𝑢𝑠ℎ • 仕様をBüchiオートマトンに変換して受理⾔語の性質を調べる • 充⾜可能性 • 実現可能性 [Pnueli, 89] [Abadi, 89] • 実現可能な仕様からはプログラムが⾃動合成可能
問題点 • LTL仕様をBüchiオートマトンに変換する⼯程 • LTL式の⻑さを𝑛とすると、変換したオートマトンのサイズは 𝑂 2 となる。 規模の大きな仕様を検証するのは困難!
本研究の⽬的 LTL式をBüchiオートマトンに変換する⼯程を効率化する。 提案⼿法 • LTLによる仕様を、より効率の良いBüchi変換アルゴリズムの知られ ているサブ⾔語に変換(近似) • 具体的には Flat LTL (FLTL) [Kanso, 2019] • 式の⻑さ𝑛に対し、サイズ𝑂 𝑛 のBüchiオートマトンに変換可能 • 任意の論理式に対する正しい近似式を与えるのは不可能なので、良 く⽤いられるDwyerの仕様パターンに対する近似式を考案
押しボタン式信号機の仕様に対する結果 • 得られたオートマトンの状態数・遷移数の⽐較 • 状態数並びに遷移数を削減することに成功している。
ロボットカーの速度制御装置 検証
ロボットカー • FPTʼ21FPGAデザインコンテストにおいて実際に使⽤された⾃ 動運転ロボット • ⾃動運転ロボットは左右の⼆輪からなり,それぞれの⾞輪に 別々のPID制御装置をもつ 𝑉 𝐾 𝑒 • ゲインの設定は適切か? 𝐾 𝑒 𝜏 𝑑𝜏 𝐾 𝑒
制御の流れ • それぞれの⾞輪について,制御の流れは右 図の通り • ⽬標値及びフィードバックとして返ってく る回転量は,⾞輪が0.5s間にどれだけ回転 するかを度数法で表したもの • PID制御装置はPWMモジュールに渡す制 御量を計算する
検証する性質 • モータにかける電圧は最⼤値の95%を超えると挙動が不安定に なる恐れがある • すなわち,制御量uが最⼤値の95%を超えないことを確かめる • オーバーシュートについても,⽬標値を⼤きく超えてしまうと 安全であると⾔えない • ⽬標値の105%を超えないことを確かめる
アプローチ • PID制御装置をハイブリッドオートマトンでモデル化 • 「危険域」に到達することがないことを検証(到達可能性検 証)
PID制御装置のモデル化
モータのモデル化
フィードバック系全体のモデル
検証結果1 Forbidden states: loc(PIDcopy_1)==unsafe
検証結果2 Forbidden states: omegaout >3.66519|| (loc(accel_1)==turn2 &&omegaout < 2.652)
まとめ • 計算機科学=「計算」という概念を数学的に探究する学問 • 形式⼿法=計算の数学的扱いに基づいたソフトウェア⼯学 • 「計算」のモデルを⽤いてソフトウェアをモデル化 • 様々なオートマトンなどを⽤いる • モデルが正しいことを数学的に検証する