跳轉到內容

從 A 到 Z 的建模/廢物管理系統建模

Add links
來自華夏公益教科書，為開放世界提供開放書籍
< 從 A 到 Z 的建模
此頁面可能需要審查其質量。

下一代核電站及廢物管理

[編輯 | 編輯原始碼]


看來，核電站將在可預見的未來與我們同在。此外，重要的不是發電，而是管理產生的廢物。

廢物管理並非核電領域的獨有現象。當前，為了應對氣候變化和全球變暖，迫切需要一場綠色革命，而這場革命的關鍵取決於如何回收或焚燒塑膠等石油產品。許多國家都存在著猖獗的非法傾倒現象。

在本節中，我們將從核工業中借鑑的一個廢物管理方面進行研究，並展示它如何被重新用於一般的廢物管理。這種發展本身說明了 (軟體) 過程改進中的一個普遍原則。真實的系統不斷發展和遷移。它們很少從頭開始。任何軟體開發計劃都應該遵循與系統相同的過程改進以實現匹配。

跟蹤就像搜尋。它依賴於地址。現在我們知道，地址可能是放置 cookie 或 RFID 標記的問題。

靈感來源

[編輯 | 編輯原始碼]

我們將透過檢視一些已經發表的作品來開始我們的模型。也就是說，我們不會假裝有任何原創性或創造性。我們的起點將是“跟蹤管理器研究”（TMS）[1]，該研究是在“計算機跟蹤系統在核電技術安全案例中的應用研究”[2]中進行的。

本質上，有兩種型別的事物：容器和放入容器中的東西。不同型別的容器很容易辨認出來。在 TMS[3] 中，有 5 種容器

我們已經從之前關於 Alloy 的工作中知道，我們可以為 Container 引入一個抽象簽名，並將 5 種容器型別作為擴充套件引入

abstract sig Container {}
sig Crate, Package, Liner, Puck, Drum extends Container {}

放入某些型別容器中的那些東西可以稱為材料。在我們對 TMS 的第一次研究中，我們將只關注 4 種材料型別[6]

  • 玻璃
  • 塑膠
  • 金屬
  • 液體

就像上面的 Container 一樣，我們為 Material 引入了一個抽象簽名，然後四種材料型別就成為擴充套件

abstract sig Material {}
sig Glass, Plastic, Metal, Liquor extends Material {}

最後，對於本介紹，要注意的是，廢物管理系統中的處理階段可以類似地分類

abstract sig Phase {}
sig Unpacking, Sorting, Assaying, Compacting, Exporting extends Phase {}

除了使用“Phase”這個詞，人們可能更喜歡“Process”。以下是建模的階段列表

  • 開箱 (箱)
  • 分類 (內容)
  • 化驗 (材料)
  • 壓實 (材料)
  • 出口 (物品)

跟蹤管理系統 (TMS) 的合金模型

[編輯 | 編輯原始碼]

這是對以下文獻中描述的跟蹤系統的重新建模

  1. John Fitzgerald 和 Cliff Jones，1998 年，第 1-28 頁
  2. John. S. Fitzgerald，1999 年，第 69-94 頁
  3. John Fitzgerald 和 Peter Gorm Larsen，第 137-201 頁？


介紹性文字

[編輯 | 編輯原始碼]

一個詳細的系統形式模型距離實現只有一步之遙。這一步包括對形式數學表示式的推演。這種推演是硬體和軟體的混合。其中大部分將是現成的。其中一些將必須是手工製作的。但是，在我們進入這個詳細階段之前，我們需要一個抽象的鳥瞰圖。這種概述將抓住所有事物的本質，並且將是容易理解的。以下是 Alloy 支援的這種高層概述。

系統需求

[編輯 | 編輯原始碼]

跟蹤管理系統 (TMS) 監控著材料容器在工業廠 (IP)（如廢物管理設施 (WMF)）中經過各個處理階段時的位置。

每個容器只容納一種型別的材料，並且一次最多隻能處於一個處理階段。每個處理階段都有一個最大容器容量，並且只能接受某些型別的材料。

系統狀態

[編輯 | 編輯原始碼]

在任何時間點，TMS 的系統狀態必須記錄

  1. WMS 中每個容器的材料型別內容目錄。簡而言之，這隻需透過 cntCatalog 來表示
  2. 每個處理階段的容器集合。
  3. 每個處理階段的階段屬性
    • 最大容器容量 (maxCapacity) 和
    • 可接受的材料型別 (mtrType)。

系統狀態約束

[編輯 | 編輯原始碼]

在任何時間點，TMS 的系統狀態都必須滿足以下系統狀態約束

  1. 每個容器最多隻能容納一種型別的材料。每個容器在給定時間最多隻能處於一個處理階段。每個處理階段最多隻能有一個最大容量值。
  2. 所有處理階段都記錄了階段屬性：最大容量和可接受的材料型別。
  3. 工業廠中的每個處理階段的最大容量至少為 1。
  4. 任何給定處理階段中的容器都記錄了材料內容。
  5. 活動處理階段記錄了階段屬性：最大容量和可接受的材料型別。
  6. IP 中的每種材料型別都有一個可能的處理階段。
  7. IP 中的每個階段都在容量範圍內執行。
  8. 在任何階段，該階段中的所有容器都包含預期型別的材料。

系統操作

[編輯 | 編輯原始碼]

TMS 有一些操作可以修改系統狀態

  1. initOp：指定 TMS 初始狀態的屬性。
  2. insertOp：將一個新的容器（其內容是給定材料型別）新增到工業廠容器目錄中。（以前是引入操作）
  3. remOp：從給定的處理階段中移除一個容器
  4. delOp：從容器內容目錄和跟蹤系統中刪除一個容器。
  5. permitOp：決定是否允許將容器移入給定階段。
  6. moveOp：將容器移入跟蹤系統中的給定階段處理。

合金模組

[編輯 | 編輯原始碼]

模組 TrackingManagementSystem -- 簡稱 TMS

開啟 util/relation 作為 rel -- 二元關係模組。
開啟 util/natural 作為 nat -- 自然數模組。
開啟 util/boolean 作為 bool -- 布林模組

標識 Container, Material, Phase {} -- 容器、材料型別和處理階段。

標識 SystemState {

cntCatalog: Container -> Material, -- 容器目錄。

trkSystem: Container -> Phase, -- 跟蹤系統。

maxCapacity: Phase -> Natural, -- 階段最大容量記錄。

mtrType: Phase -> Material -- 階段材料型別記錄。

}

視覺化

[編輯 | 編輯原始碼]

我們從之前對 Alloy 的工作中知道，這些資訊足以讓我們視覺化元模型的結構。

跟蹤管理系統元模型投影在 SystemState 上。

系統約束

[編輯 | 編輯原始碼]

[1]

斷言 FieldTypeCns(s: SystemState) {
    functional[sysState.cntCatalog, dom[sysState.cntCatalog]]
    functional[sysState.trkSystem, dom[sysState.trkSystem]]
    functional[sysState.maxCapacity, dom[sysState.maxCapacity]]
    dom[sysState.maxCapacity] = dom[sysState.mtrType]
    所有 phase: dom[sysState.maxCapacity] | sysState.maxCapacity[phase] != Zero
}

[2]

斷言 TrackerContainerCns(sysState: SystemState) {
    dom[sysState.trkSystem] 在 dom[sysState.cntCatalog]
}

[3]

斷言 TrackerPhaseCns(sysState: SystemState) {
    ran[sysState.trkSystem] in dom[sysState.maxCapacity]
    ran[sysState.trkSystem] in dom[sysState.mtrType]
}

一個更簡單的廢物管理模型

[編輯 | 編輯原始碼]

容器

[編輯 | 編輯原始碼]


讓我們從容器開始？想象一下你在一個建築物裡，裡面有用於

  • 處理空水瓶的容器，
  • 使用過的噴墨墨盒，
  • 使用過的電池，以及
  • 廢紙。

這些容器每週都會由垃圾公司NoWasteNoWant收集，並運送到城市裡的廢物管理設施。

容器註釋

[編輯 | 編輯原始碼]

當我們談論“空水瓶”時，我們想到的是塑膠或玻璃材料。現在，我們將只限制自己使用兩種型別

  • 玻璃瓶
  • 塑膠瓶

容器型別

[編輯 | 編輯原始碼]

為了第一個廢物管理模型。我們將假設只有兩種型別的容器

  • 溼容器 — 用於所有液體物質，即塑膠瓶或玻璃瓶。
  • 幹容器 — 用於其他所有東西

註釋

[編輯 | 編輯原始碼]
  1. ↑ TMS 是我們的首字母縮略詞。它代表Tracking Manager Study。在計算機科學中廣泛使用首字母縮略詞。這個習慣可能是由於程式設計變數的概念。驗證這個假設會很好。我們將在自己的廢物管理系統模型中使用這個首字母縮略詞。但在這種情況下，TMS 代表Tracking Management System。首字母縮略詞可以靈活，即使模稜兩可。
  2. ↑ Fitzgerald&Jones 1998，第 28 頁。
  3. ↑ Fitzgerald&Jones 1998，第 3 頁
  4. ↑ 斯坦福大學 SLAC 的通用冰球的例子可能可以說明冰球是什麼，它可能是什麼樣子，以及它如何使用。
  5. ↑ 報告 WSRC-MS-98-00571 對核廢物管理問題進行了非常好的概述，包括關於使用冰球的非常有用的文字。
  6. ↑ Fitzgerald&Jones 1998，第 3 頁。

參考文獻

[編輯 | 編輯原始碼]


閱讀連結

[編輯 | 編輯原始碼]
  1. Bicarregui，Juan Carlos（編輯），（1988）。VDM 中的證明：案例研究。倫敦：施普林格出版社。 ISBN 978-3540761860. {{cite book}}: |first= has generic name (help); Cite has empty unknown parameter: |coauthors= (help)CS1 maint: extra punctuation (link)
  2. Fitzgerald，John（1998）。“跟蹤系統”。在 Bicarregui，Juan Carlos（編輯）中。VDM 中的證明：案例研究。倫敦：倫敦：施普林格出版社。第 1-29 頁。 {{cite book}}: Cite has empty unknown parameter: |coeditors= (help); Unknown parameter |coauthors= ignored (|author= suggested) (help)

電子連結

[編輯 | 編輯原始碼]
檢索自 "https://wikibook.tw/wiki/Modeling_from_A_to_Z/Modeling_the_Waste_Management_System"
華夏公益教科書