7th長崎QDG　大学連携セッション 「計算機科学に基づくソフトウェア工学」

計算機科学に基づく ソフトウェア⼯学 ⻑崎⼤学 情報データ科学部 伊藤 宗平 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) ヘッドを１コマ右または左に動かす。 • 状態変化、書き換える記号、ヘッドの移動⽅向は(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通りがある。 ２つのプロセスの 並⾏合成

時間オートマトンの動作 (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制御装置のモデル化

モータのモデル化

フィードバック系全体のモデル

検証結果１ Forbidden states: loc(PIDcopy_1)==unsafe

検証結果２ Forbidden states: omegaout >3.66519|| (loc(accel_1)==turn2 &&omegaout < 2.652)

まとめ • 計算機科学＝「計算」という概念を数学的に探究する学問 • 形式⼿法＝計算の数学的扱いに基づいたソフトウェア⼯学 • 「計算」のモデルを⽤いてソフトウェアをモデル化 • 様々なオートマトンなどを⽤いる • モデルが正しいことを数学的に検証する