%0 Journal Article
%T 论有穷状态验证方法的局限性
%A 葛玮 龚晓庆 郝克刚？
%J 计算机科学
%D 2007
%X 程序有穷状态验证方法是介于程序验证和程序测试之间的一种方法，一方面它如同程序验证一样可以证明某程序具有某些要求的性质，或找出反例证明该程序不具有所要求的性质。另一方面它又不像程序验证那样复杂，要求验证人员具有较高的形式化推理的专业理论和数学水平。但是，现有的有穷状态验证方法有很大的局限性，它要求所论证的性质是有穷自动机所接受的事件序列的集合，或等价地说该性质能表示成为正则表达式。众所周知，有穷自动机所能接受的语言类，按chomsky字的集合的分类是很小的类。本文讨论了这种局限性，井尝试突破只能使用有穷自动
%K 程序验证程序测试有穷自动机有穷状态验证有穷路径验证
%U http://www.jsjkx.com/jsjkx/ch/reader/view_abstract.aspx?file_no=23783908&flag=1