報告題目：一種面向FRETish規約的結構化狀态圖自動生成方法
報告摘要：時序規約模式具有接近自然語言的形式，又具有精确的語義，有助于形式化方法在工業界中的應用。面向需求描述的狀态圖自動生成在需求和設計之間架起橋梁，有助于提高軟件設計的效率和正确性。現有的針對時序規約模式的狀态圖生成方法不能處理實時規約，對狀态之間的關系表達不夠全面，未能表達與狀态變遷相關的行為。為此，本文提出了針對實時規約描述語言FRETish的狀态圖結構化自動生成方法。該方法以規約生效的時間範圍以及規約控制對象的取值區分狀态，通過對進出狀态的條件進行分析，得到狀态之間的嵌套、變遷、并發關系以及相關的行為。狀态數量與規約規模線性關系，通過狀态命名體現其與規約之間的對應關系，具有良好的可追蹤性。本文設計并實現了狀态機自動合成工具 SMgen，生成的狀态圖可以通過工具FRET和CoCoSIM進行正确性驗證。
個人介紹：
包志文，1996年生，bet356手机版唯一官网計算機學院碩士生。主要研究方向為軟件工程，形式化方法與模型驅動開發。