报告题目：一种面向FRETish规约的结构化状态图自动生成方法
报告摘要：时序规约模式具有接近自然语言的形式，又具有精确的语义，有助于形式化方法在工业界中的应用。面向需求描述的状态图自动生成在需求和设计之间架起桥梁，有助于提高软件设计的效率和正确性。现有的针对时序规约模式的状态图生成方法不能处理实时规约，对状态之间的关系表达不够全面，未能表达与状态变迁相关的行为。为此，本文提出了针对实时规约描述语言FRETish的状态图结构化自动生成方法。该方法以规约生效的时间范围以及规约控制对象的取值区分状态，通过对进出状态的条件进行分析，得到状态之间的嵌套、变迁、并发关系以及相关的行为。状态数量与规约规模线性关系，通过状态命名体现其与规约之间的对应关系，具有良好的可追踪性。本文设计并实现了状态机自动合成工具 SMgen，生成的状态图可以通过工具FRET和CoCoSIM进行正确性验证。
个人介绍：
包志文，1996年生，东南大学计算机学院硕士生。主要研究方向为软件工程，形式化方法与模型驱动开发。
