《软件系统形式化验证》课程简介
课程号* 英文课程名 课程名* 软件系统形式化验证 基本面向 考核方式 上机总学时 软件工程本科 Formal Verification of Software System Designs 先修课程名 Software or digital systems, Discrete Mathematics. 总学时* 32 讲课总学时 32 考试 考查 （名称、作者、出版社、出版时间） 教 材 E. Clark, O. Grumberg, D. Peled, \"Model Checking\ （名称、作者、出版社、出版时间） 参考书 M. Huth, M. Ryan, Logic in Computer Science: Modeling and Reasoning about Systems, Cambridge University Press, 2000. 随着系统复杂性的增加，设计出错的可能性也正在增加。在系统设计过程中, 由于顶层说明的定义是人工的，并且综合设计的细化过程通常需要人工的精细调整才能达到更高的性能，所以有必要保证中间设计步骤与用户说明的特性的一致性和正确性。成功的设计方法要求验证设计是设计过程的必需部分，而不是可有可无的。对于一个数字系统，花费在验证设计上的时间是花费在设计上时间的80%。设计验证是课程说明 内 容 简 介 任何重大系统开发过程面临的主要挑战。虽然传统的模拟技术仍被用于验证设计，但是越来越复杂的设计使得该技术创建足够多的向量集变得很困难，甚至是不可能。所以，需要一种新的验证方法来应付这种情况。形式化验证技术已经成为保证系统正确性的一种强有力的方法。 本课程将介绍形式化验证技术的基本方法及原理。这种方法在实际中已经成功地用于验证复杂的数字系统设计和通信协议。通过参加本课的学习, 可以对系统功能的模型的建立, 系统行为描述有更深的理解。本课程的内容是从事信息产业人材的必备基础。 备注
四川大学软件学院课程简介
Course Outline
Course Number Intended Audience Course Title Formal Verification of Software System Designs Undergraduate Students on Software Engineering Prerequisites Evaluation of Learning Total Hours Textbooks Software or digital systems, Discrete Mathematics. The written test (100%) (including Lecture hours Lab hours) （Including title, author, press and publication date ） E. Clark, O. Grumberg, D. Peled, \"Model Checking\ （Including title, author, press and publication date ） Reference M. Huth, M. Ryan, Logic in Computer Science: Modeling and Reasoning about Systems, Cambridge Books and Other Materials University Press, 2000. Academic Statement Software systems are widely used in applications where failure is unacceptable. Because of the success of the Internet and embedded systems in automobiles, airplanes, and other safety critical systems, we are likely to become even more dependent on the proper functioning of computing devices in the future. Due to this rapid growth in technology, it will become more important to develop methods that increase our confidence in the correctness of such systems. Traditional verification techniques use simulators with handcrafted or random test vectors to validate the design. Unfortunately, generating test vectors is very labor-intensive. The overall complexity of the designed systems implies that simulation cannot remain the sole means of design verification, and one must look at alternative methods to complement simulation. Recent years have brought about the development of powerful formal verification tools for verifying of software systems. By now, the information technology industry has realized the impact and importance of such tools in their own design and implementation processes. The objective of the course is to introduce the participants to the practical formal verification techniques for hardware/software systems that are beginning to penetrate industrial applications. Topics to be covered include: system modeling, formal logics for system verification (Boolean & first-order logic, higher-order logic, temporal logic), formal specifications, CTL model checking, BDDs, applications of theorem proving systems, microprocessor verification, and SAT solvers. Exercises are provided in the class. 四川大学软件学院课程简介
Course Description Software systems are widely used in applications where failure is unacceptable. Because of the success of the Internet and embedded systems in automobiles, airplanes, and other safety critical systems, we are likely to become even more dependent on the proper functioning of computing devices in the future. Due to this rapid growth in technology, it will become more important to develop methods that increase our confidence in the correctness of such systems. Traditional verification techniques use simulators with handcrafted or random test vectors to validate the design. Unfortunately, generating test vectors is very labor-intensive. The overall complexity of the designed systems implies that simulation cannot remain the sole means of design verification, and one must look at alternative methods to complement simulation. Recent years have brought about the development of powerful formal verification tools for verifying of software systems. By now, the information technology industry has realized the impact and importance of such tools in their own design and implementation processes. The objective of the course is to introduce the participants to the practical formal verification techniques for hardware/software systems that are beginning to penetrate industrial applications. Topics to be covered include: system modeling, formal logics for system verification (Boolean & first-order logic, higher-order logic, temporal logic), formal specifications, CTL model checking, BDDs, applications of theorem proving systems, microprocessor verification, and SAT solvers. Exercises are provided in the class. Notes 四川大学软件学院课程简介
