# 4 part

下面是這堂課所規劃的四個層級：

- [Part1]Preliminary
- [Part2]Applications
- [Part3]Intelligent Technology
- [Part4]Advanced Topic

這週的課程來到了 Part 4，Advanced Topic。

# V Model

老師說 V Model 在他之前工作的車廠，豐田，是聖經；沒有遵照的話會有不安全感：)

一加公司製造產品時，絕對不可能有了計劃就直接砸錢下去做，一定會做一定的「評估」，並且評估是要隨時進行的，以確保做的對，做的好，做的成功。

這就是 V Model 誕生的原因。

## 流程

可以參考[維基百科的圖](https://zh.wikipedia.org/zh-tw/V%E6%A8%A1%E5%9E%8B)，但以垂直方向來說，就是三個順序：

:::info
Use case → Requirements → Specification
:::

同時垂直方向也代表了精細程度，以及 Design space 的大小。
>Design space 可以看作是要考慮的範圍；由於越往下範圍越窄，所以才被叫做 V Model

- Use case：最原始、寬廣的想法，例如想設計一個 Intersection Management。
- Requirements：有了想法後，就是要制定我們要達成這個想法，「要求」達到什麼
- Specification：有了要求後，就可以制定各種細部的內容，到達實作的部分

上面的三個順序，其實也對應到了 V Model 的三個水平的階層：

- Use case → Concept of Operation
- Requirements → Requirements and Architecture
- Specification → Detailed Design

> Design 不是做出來， Implementation 才是

## 分析

左邊上層的兩個，有紅色的圈圈，意思是該階段會需要「Analysis」，要有一套系統或規則可以分析你預計做的跟你想要的到底有沒有符合、以及好不好。
>例如分析安全性、穩定性、可靠性、表現等等不同的 Metric

絕對不可以 Implementation 後才做分析，那時候就為時已晚了。
>例如車子傳輸訊號的 Timing Analysis 就是一個例子，你設計好後，搭配這套方法進行分析，看看有沒有符合你的需求

當然 Implementation 之後也要有方法確保實作結果是正確的

:::info
簡單來說就是你要知道：
- 你的 design 是不是正確的，有沒有滿足你的 requirements
- 你的 Implementation 是正確的，有沒有滿足 Specification
:::

:::warning
其實 V Model 的概念不只可以用於這裡，更抽象化一點來說，只要你想做某件 Cost 很大的事情，都可以用 V Model 的流程
:::

## 分析的方法

- 數學分析：例如之前教過的 Timing Analysis
- Simulation：Implementation 前盡可能的模擬結果

上面兩個是 Implementation 前的分析；下面三個是 Implementation 前的檢驗。

- Verification：確保有沒有符合「自己內部」設置的條件、規範等等
- Validation：確保有沒有符合「外部客戶」設置的條件、規範等等
- Testing：Implementation 後來測試各種情境的成果

:::info
但是 Simulation 跟 Tesing 還是要小心，他不可能一定 Cover 所有的情況，不像 verification 跟 validation 給的是保證。
:::

:::warning
可以看到 V Model 中右到左，同個層級中會需要「Verification & Validation」，也就是 Implementation 完成後，是需要經過驗證，確保有達到目的。
:::

---

# Formal Verification

正式的 Verification。通常來說就是把問題轉成數學式子，或者是某種數學 model 例如狀態機，然後用數學的方式證明他在哪種條件下有哪些「保證的性質」。

- 常用方案一：deductive verification
- 將問題轉成一些可用現有 solver 來解的問題，例如 MILP、SAT 等等
- 常用方案二：model checking
- 這堂課的重點

## 常見的分析

下面是 Formal Verification 常見的五種分析，之後會一一介紹。

- Reachability Analysis
- Lineat Temporal Logic / LTL
- Computation Tree Logic / CTL
- Signal Temporal Logic / STL
- Contract-Based Design

## Transition System

介紹方法之前，先介紹 Transition System 的定義。

Transition System 是一個 tuple：$(X,X_{\text{init}},T)$

- $X$：狀態變數 state variable，值的範圍可以是有限或無限個
- $X_{\text{init}}$：一個函數，可以將 $X$ 映射回初始值
- $T$：「如何轉移」的描述 discription，用來更新 $X$
- 或者簡單來說就是轉移函數

要注意的是，一個狀態變數可以有很多種不同的狀態值 value，而這些值可以是有限或無限的。

具體來說就是狀態圖可以有無線種 state。

:::warning
為了方便，以下我們直接用具體的例子， Finite State Machine 來做介紹。
>但是要注意 FSM 的狀態是 Finite，不是無限的

想了解的話可以參考我之前的自動機與形式語言筆記，但是由於篇幅不多所以就當作參考就好。
:::

# Reachability Analysis

想要知道某種狀態到底「到不到的了」。

可以使用簡單的圖論演算法，例如 BFS、DFS，分離出一群一群的狀態。

如果有某個狀態是我們不想碰到的，但我們檢查後發現會碰到，那麼這個 FSM，或者說你的 Design 就要重新設計。

## 更複雜的情況

如果今天 A 狀態機，他的輸入是由另一個狀態機 B 的輸出所決定。
>B 狀態機在這裡沒有輸入，只會依照一個循環的順序 + 起始狀態，循環的輸出值給 A

此時的情況一樣可以用演算法檢查，會不會抵達某個我們不想碰到的 state。

由於 B 有個起始狀態，所以他給 A 的值的條件「比較強」。

假設今天有另一個狀態機 C，他跟 B 做一樣的事情，但是他沒有起始狀態，那麼他給 A 的值的條件「沒那麼強，比 B 弱」。

而這個「條件的強弱」可以用於邏輯的判斷，例如上面可以知道

- 如果 C 的輸出「不會」讓 A 走到我們不想走到的狀態，那麼代表 B 的輸出「也一定不會」
- 如果 B 的輸出「會」讓 A 走到我們不想走到的狀態，那麼代表 C 的輸出「也一定會」

## Safty Table

現在我們換成更 general 的情形，我們令一個 tuple $(m,k)$，意思是：「一個狀態機『連續吃到的 $k$ 個 input』中，最多會經過 $m$ 個我們不想經過的狀態」。

在這裡我們不考慮怎麼確認「該狀態機是 $(m,k)$」這件事，假設我們知道：)

我們這裡要介紹的是，哪些狀態機是「特別情形」，以及上面提到的條件強弱可以用於建這個表。
>請參見講義的圖表

- optimal strategy for system designers
- 可以看到綠的色安全範疇，代表該狀態機滿足 $(m,k)$
- 而位於角角的情形就是最佳的情形，因為他們「容錯率」最高
- 也就是連續 $k$ 個 input 中，可以承受的「經過的不好狀態」比例最高
- optimal strategy for attackers
- 可以發現一樣是位於角角的情形
- 因為他們只要經過最少比例的「不好的狀態」，比較容易達成

## 建表方法

假設我們定義求出 $(m,k)$ 的時間是 1，那麼 naive 的方法就需要 $O(k^2)$。
>$0\le m \le k$

但其實我們可以知道：

- 如果 $(m,k)$ 是安全的，那麼 $(m^*,k),\ m^* \le m$ 都會是安全的
- 如果 $(m,k)$ 是不安全的，那麼 $(m^*,k),\ m^* \ge m$ 都會是不安全的
- 如果 $(m,k)$ 是安全的，那麼 $(m,k^*),\ k^* \ge k$ 都會是安全的

依照這個邏輯，我們只需要從 $(1,1)$ 出發，然後就可以根據規則，走出一個沿著邊界的 Z 字型步伐，算出全部 table 的值。

這樣時間就可以壓到 $O(K)$。

## Composition of FSM

上面有說 A 是以 B 的輸出作為輸入，其中 B 沒有輸入，就是單純輸出值給 A。

但是其實可以有不同的情形：

- 例如可能 A 跟 B 是其實兩者的狀態要共同考慮，基於組合的狀態「Parallel Composition」來做評估
- 這時又要考慮兩者的 transition 時間是不是一樣
- 可以分成 「Synchronous」跟 「Asynchronous」
- 又或者其實兩者是互相影響的，一樣是基於兩者組合的狀態「Parallel Composition」來做評估

# Logic

接下來介紹上面提到的三種 Logic 分析。

- Linear Temporal Logic / LTL
- Computation Tree Logic / CTL
- Signal Temporal Logic / STL

他們叫做 Logic 不是沒有原因的，因為他就是用一套語言，來描述特定的邏輯，某種程度上來說就是一種形式邏輯。

這三個的關係如下：

- LTL 是描述離散時間軸的單一可能性(path)
- CTL 是描述離散時間軸的多種可能性(path)
- 可能某個論述 $p$，他在某些 paths 的情況，跟其他 paths 不一樣
- STL 是描述連續時間軸的多種可能性(path)

## Operator

在離散的情況下，路上的每個狀態的時間是逐步進行的，例如時間從 0 開始，一直到 ...。

- $G p$：代表「所有的時間」，$p$ 都是對的
- $Fp$：代表從初始時間開始，存在一個時間點 $p$ 是對的
- $Xp$：代表從初始時間開始，下一個時間，$p$ 是對的
- $q U p$：代表 $q$ 在某個時間點以前，某個時間點是對的，直到該時間點時，p 是對的

以上是 LTL 的範疇； CTL 考慮了多條路，所以新增了兩個 operator：

- $A p$ 對所有路徑
- $E p$ 存在一條路徑

如果是連續的情況下，或者說 STL，那麼就沒有所謂的時間點，但是會改成在 operator 下標標註時間範圍：

- 例如 $G_{[0,2]}p$

而上述的 operator，是可以結合一起使用的，例如：

- $AG p$
- $EF p$

並且同時可以搭配基本的邏輯符號，例如：

- 代表 OR 的 $\vee$
- 代表 AND 的 $\wedge$
- 代表 If then 的 $\rightarrow$

而 STL 要注意，p 的論述也要是連續的時間。

:::info
其實還可以根據各種不同應用場景，有不同的語言，他們有各自的性質，例如時間是不是連續的，或者是不是 Decidable：)
:::

## 例子

老師說他在豐田的一個同事，評估了兩種系統的整合可不可行：

- Cooperative Pile-up Mitigation System (CPMS)
- 簡單來說就是車子發現剎不住，就會緊急告訴其他車子，尤其是前車，快逃
- 此時 CPMS 在判斷可以往前後加速駛離後，就會讓車子踩油門快逃
- False-Start Prevention System (FPS)
- 防止車子誤踩油門

然後老師的同事就將兩種系統，用 STL 語言描述一個 assumption 後，使用現有的工具 Breach，來看看是 True 還是 False。

結果是會是 False；直覺上來說就是有時候 CPMS 提供的訊號，會被誤判成是誤踩油門，而導致逃離失敗。

# Contract-Based Design

簡單來說就是要設計一種 contract，然後我們一定就要符合 contract 的內容。
>某種意義上來說就是限制

contract 通常可以分出四種 level：

- basic contract
- 說好變數要是怎樣的形態、如何使用等等
- behavior contract
- 定義好函數的行為
- synchronous contract
- 時間有沒有要同步
- QoS contract
- 提供的服務要有多好

## Assume-Guarantee Contract

這種 Contract 長得像一個 tuple $(A,G)$ 意思是只要滿足給定的 assumption $A$，那麼保證的 guarantee $G$ 就一定要發生。

所以就可以根據這個 contract 對設計的結果做檢查：

- design error：不符合 assumption
- Implementation error：guarantee 沒有滿足

---

# Testing and Simulation

大致上面都講完了，這裡介紹一些有趣的內容。

## Testing

老師說台灣自駕車的測試場可以去彰化，有個專門的測試場地；不過近年法規有放寬。

Waymo 自駕車做 Testing 時，會先在電腦模擬環境做 Testing。
>或許這應該叫做 Simulation

接著就可以在測試場地測試，最後就是實際世界的測試。

## Simulation

可以拿來模擬的軟體：

- AirSim
- Carla
- Unity 3D
- SUMO
- 比較偏向紅綠燈控制的模擬