软件系统形式化验证课程简介

软件系统形式化验证课程简介

ID:15042516

大小:54.00 KB

页数:3页

时间:2018-08-01

软件系统形式化验证课程简介_第1页
软件系统形式化验证课程简介_第2页
软件系统形式化验证课程简介_第3页
资源描述:

《软件系统形式化验证课程简介》由会员上传分享,免费在线阅读,更多相关内容在学术论文-天天文库

1、《软件系统形式化验证》课程简介课程号*课程名*软件系统形式化验证英文课程名FormalVerificationofSoftwareSystemDesigns基本面向软件工程本科先修课程名Softwareordigitalsystems,DiscreteMathematics.考核方式5考试5考查总学时*32讲课总学时32上机总学时教材(名称、作者、出版社、出版时间)E.Clark,O.Grumberg,D.Peled,"ModelChecking",MITPress,2000.参考书(名称、作者、出版社、出版时间)M.Huth,M.Ryan,LogicinComputerScie

2、nce:ModelingandReasoningaboutSystems,CambridgeUniversityPress,2000.课程说明内容简介随着系统复杂性的增加,设计出错的可能性也正在增加。在系统设计过程中,由于顶层说明的定义是人工的,并且综合设计的细化过程通常需要人工的精细调整才能达到更高的性能,所以有必要保证中间设计步骤与用户说明的特性的一致性和正确性。成功的设计方法要求验证设计是设计过程的必需部分,而不是可有可无的。对于一个数字系统,花费在验证设计上的时间是花费在设计上时间的80%。设计验证是任何重大系统开发过程面临的主要挑战。虽然传统的模拟技术仍被用于验证设计,

3、但是越来越复杂的设计使得该技术创建足够多的向量集变得很困难,甚至是不可能。所以,需要一种新的验证方法来应付这种情况。形式化验证技术已经成为保证系统正确性的一种强有力的方法。本课程将介绍形式化验证技术的基本方法及原理。这种方法在实际中已经成功地用于验证复杂的数字系统设计和通信协议。通过参加本课的学习,可以对系统功能的模型的建立,系统行为描述有更深的理解。本课程的内容是从事信息产业人材的必备基础。备注四川大学软件学院课程简介CourseOutlineCourseNumberCourseTitleFormalVerificationofSoftwareSystemDesignsInte

4、ndedAudienceUndergraduateStudentsonSoftwareEngineeringPrerequisitesSoftwareordigitalsystems,DiscreteMathematics.EvaluationofLearningThewrittentest(100%)TotalHours(includingLecturehoursLabhours)Textbooks(Includingtitle,author,pressandpublicationdate)E.Clark,O.Grumberg,D.Peled,"ModelChecking",M

5、ITPress,2000.ReferenceBooksandOtherMaterials(Includingtitle,author,pressandpublicationdate)M.Huth,M.Ryan,LogicinComputerScience:ModelingandReasoningaboutSystems,CambridgeUniversityPress,2000.AcademicStatementSoftwaresystemsarewidelyusedinapplicationswherefailureisunacceptable.Becauseofthesucc

6、essoftheInternetandembeddedsystemsinautomobiles,airplanes,andothersafetycriticalsystems,wearelikelytobecomeevenmoredependentontheproperfunctioningofcomputingdevicesinthefuture.Duetothisrapidgrowthintechnology,itwillbecomemoreimportanttodevelopmethodsthatincreaseourconfidenceinthecorrectnessof

7、suchsystems.Traditionalverificationtechniquesusesimulatorswithhandcraftedorrandomtestvectorstovalidatethedesign.Unfortunately,generatingtestvectorsisverylabor-intensive.Theoverallcomplexityofthedesignedsystemsimpliesthatsimulationcannotremain

当前文档最多预览五页,下载文档查看全文

此文档下载收益归作者所有

当前文档最多预览五页,下载文档查看全文
温馨提示:
1. 部分包含数学公式或PPT动画的文件,查看预览时可能会显示错乱或异常,文件下载后无此问题,请放心下载。
2. 本文档由用户上传,版权归属用户,天天文库负责整理代发布。如果您对本文档版权有争议请及时联系客服。
3. 下载前请仔细阅读文档内容,确认文档内容符合您的需求后进行下载,若出现内容与标题不符可向本站投诉处理。
4. 下载文档时可能由于网络波动等原因无法下载或下载错误,付费完成后未能成功下载的用户请联系客服处理。