《软件形式化方法》实验教学大纲

1、软件形式化方法实验教学大纲课程代码：EMST3002课程名称：软件形式化方法 英文名称：Formal Method in Software Engineering 实验室名称：计算机信息系统实验室课程学时：54 实验学时：18一、本课程实验教学目的与要求软件形式化方法是采用数学的方法处理软件开发所涉及的各种要素，主要包括形式化规约、形式化验证及形式化转换等，以确保开发出质量可靠的软件。通过这门课程的实验教学，使得学生初步地掌握各种与软件形式化方法有关的数学原理，主要包括命题逻辑、一阶逻辑及时序逻辑、软件开发语言的语法、语义及执行模型等程序语义理论和形式法验证的算法知识，熟练使用模型检测器SPI

2、N，能够用SPIN对C语言程序进行模型检测，理解及分析检测结果，在掌握使用逻辑描述系统及系统属性的基础上，初步掌握定理证明器Z3的使用方法，掌握基本的程序验证方法。所有实验中，基础性和综合实验各约占二分之一。二、主要仪器设备及现有台套数 实验时每人一台PC。三、实验课程内容和学时分配序号实验项目名称目的、要求实验内容学时分配实验类型每组人数必开、选开1SPIN的了解与安装了解SPIN工具的基本操作熟悉ispin（1）下载开源工具SPIN，ActiveTCL,了解这些工具基本使用方法和功能。（2）学会使用图形化界面ispin,并详细了解与界面相关的各种功能。2基础性1必开2SPIN接口语言Pro

3、mela演示掌握使用promela进行简单的顺序和并发程序的设计利用promela语言设计简单的顺序和并发程序，并使用spin进行模拟执行3综合性1必开3系统时序属性规约掌握使用时序逻辑对系统的安全性和活性属性进行规约的方法（1）设计简单的并发程序（2）使用时序逻辑对并发程序的属性进行规约（3）了解并发程序的关键属性特征2综合性1必开4SPIN模型检验系统地使用SPIN进行模型检验设计规模较大，复杂度较高的程序，进行系统的，完整的模型检验4设计性1必开5Z3的了解和安装了解Z3的安装，基本使用方法及接口命令和语言（1）下载定理证明器Z3及相关的辅助材料，安装Z3。（2）对用一阶逻辑描述的定理进

4、行证明2基础性1必开6简单程序的验证使用定理证明器证明不含循环的顺序程序和并发程序正确性的证明使用Z3对简单的顺序程序进行证明，程序中只含有顺序结构和选择结构2基础性1必开7基于循环不变式的程序程序证明使用定理证明器对复杂程序进行正确性证明，例如含有循环的程序。（1）设计含有循环的程序，并对该程序的功能进行规约（2）根据证明任务，写出循环不变式，使用Z3进行证明3综合性1必开四、考核方式1、实验报告：每项实验学生都应该撰写相应的实验报告。实验报告应完整地反映整个实验中各个环节的内容及过程，并对本次实验相关的内容进行总结，包括知识重点，难点及疑点。实验报告的格式应结构清晰，包括实验名称、实验目的

5、、实验内容、实验过程及实验总结等。2、考核方式课程实验的考核方式：提交实验报告课程实验考核成绩的确定，课程实验成绩占课程总成绩的比例：课程实验考核成绩由学生的三部分考察结果决定，分别为学生实验课出勤率、实验课实验过程的质量和实验报告质量。课程实验成绩占课程总成绩的比例为30%五、实验教材、参考书1、教材：古天龙.软件开发的形式化方法M.高等教育出版社.20052、参考书：（1） HYPERLINK /s/?key1=%cd%f5%c1%d6%d5%c2&zyandor=and t _blank 王林章, HYPERLINK /s/?key1=%b2%b7%c0%da&zyandor=and t _blank 卜磊, HYPERLINK /s/?key1=%b3%c2%f6%ce&zyandor=and t _blan