关于软件形式化方法.pdf

苇19卷第2期 重庆师范学院学报(自然科学版) 2002年6月 Science Jun．2002 VuJ．I9No．2 Journalof Normal Edition) ChongqingUniversity(Natural 关于软件形式化方法鬻 张广泉“2 摘 要：简要回顾了形式化方法的发展历程，阐述了形式化方法的定义、重要性及主要研究内容。着重讨论了形式 规约语言与方法，以及演绎证明和模型检测等形式验证方法。 关键词：形式化方法；规约；验证；演绎证明；模型检测 中匣分类号：TP311 文献标识码：A FormalMethodsforSoftware ZHANG Guang．quart“‘ Mathematicsand Normal 400047； (1．Dept．of ComputerScience，ChongqingUniversity。Chongqing Lab．of Chinese of 2．Key ComputerScience，TheAcademySciences，Beijing100080，China) Abstract：This thedefinitionand offormalmethodsafter backonthe of paperpresents importance simplylooking history overviewofformal discusses formalmethods。andan methods．Theauthor provides mainly specificationlanguages(rneth— verificationmethodsthatincludedeductiveandmodel ods)and proving checking． words：formal Key methods；specification；verification；deductiveproving；modelchecking 随着软件系统的结构越来越复杂，规模越来越庞大，复杂程度越来越高，软件出现错误的可能性及其造 成的危害也日益突出，由于软件错误而导致灾难性后果的报道屡见不鲜。如1996年6月4日，耗资80亿美 和姿态信息完全遗失，而信息遗失是由于惯性制导系统的软件出现规约和设计错误。又如2000年lO月，由 于诺基亚提供的软件中的一个错误，造成德国一家移动电话公司的通信服务被中断3个多小时，这样的问题 如果发生在战争环境下，后果将不堪设想。 上述两例可以看到．软件是否可信赖已成为国家经济与国防等系统能否正常运转的关键因素之一，尤其 成熟的方法学，还没有令人信服的办法能够论证或确认一个复杂软件系统是高度可靠安全的。 软件领域存在的这种深层次的问题已经引起西方发达国家尤其是美国政府部门和计算机专家的高度重 视：美国总统信息技术顾问委员会(PITAC)于1999年向白宫递交一份报告，认为美国“依赖于脆弱的软件”， “缺乏构造可靠安全软件的技术”。其主要建议是“把软件基础研究列为绝对优先”；美国国防高等研究规划 局(DARPA)资助的“FormalMethods”(形式化方法)计划，重点支持对高可信软件系统的原理和相应支撑工 (FormalMethods andVerification