此專案是位於瑞士的一間金屬表面處理雜誌公司，在使用網站時常發現有圖片、文件或連結等資料消失的情況，且網站已有許多年無維護，業主希望將網站錯誤解決並翻修網站。

此網站原始 PHP 語法老舊且架構相當雜亂，故決定改以 Laravel 將程式重構，並將資料庫重整，專案主要內容包括響應式前端介面、頁面 API 與後台資料存取，而目前專案進度已處於收尾階段。

這個仿 IG 網站是我學習 Laravel 後第一個作品，用意是希望能透過專案來練習學到的技術，並了解網站實際上的架構流程運作。這網站擁有的功能與實際 IG 雷同，如帳號管理、貼文 CRUD 功能、使用者追蹤留言等。 而在這專案中更加體會 Laravel 的強大，例如內建架構的完善性、Composer 套件支援，與 Eloquent ORM 的方便性，更透過這專案學習到了 MySQL、Bootstrap4 與 Vue.js。

在模型驗證中，要去驗證即時系統之行為時，會使用時間狀態機來模擬。然而對於時間狀態機的呈現方法中，狀態進行轉換動作的部分是沒有強迫語意的，代表系統可能未在轉換允許的時間範圍內動作，而系統時間繼續處在原狀態中演進，卻再無可滿足該時間範圍之轉換可進行，導致系統應有的行為可能因為建模語言的缺失而呈現錯誤。

針對這項問題，先前的研究中提出了緊急型語意的概念來解決，透過緊急型語意會使時間狀態機之轉換具有能強制動作的功用，依照給予的語意在所規範的時間內必須進行轉換，使系統行為能準確地被描述。

然而在以往模型驗證器中，緊急型語意都只應用於單純的即時系統模型驗證，考量於現今系統功能逐漸複雜化之趨勢，許多系統除了時間的特性外更擁有機率的行為，像是網路溝通協定等。所以我們將緊急型語意運用至可分析機率行為之即時系統中，建立了可針對緊急型即時系統之機率模型驗證，並且可透過實驗數據量化分析，比較系統在應用緊急型語意後之行為差異。

在此碩論中使用 PRISM 開源碼模型驗證器，並使用 Java 和 JavaCC 撰寫編譯器與演算法。