论有穷状态验证方法的局限性

Limitations of the Finite State Verification Approach

程序有穷状态验证方法是介于程序验证和程序测试之间的一种方法,一方面它如同程序验证一样可以证明某程序具有某些要求的性质,或找出反例证明该程序不具有所要求的性质。另一方面它又不像程序验证那样复杂,要求验证人员具有较高的形式化推理的专业理论和数学水平。但是,现有的有穷状态验证方法有很大的局限性,它要求所论证的性质是有穷自动机所接受的事件序列的集合,或等价地说该性质能表示成为正则表达式。众所周知,有穷自动机所能接受的语言类,按Chomsky字的集合的分类是很小的类。本文讨论了这种局限性,并尝试突破只能使用有穷自动机的限制,提出了一种新的验证方法——有穷路径验证法。在这种方法中,所论证的性质表示可以推广到使用任何一类自动机。作为代价,描写系统的模型限制是无环的。对于有环的描写系统的模型,本文提出了一种称之为“有穷路径测试”的方法。同一般的程序测试一样,用这种方法通过测试不能正面地验证程序的正确性,可是如果通不过测试,则能帮你发现反例,找出程序的错误。与一般的程序测试不同的是这里的测试是相对于模型的路径,而不执行实际的程序。

Finite state verification for programs is an approach between theorem proving and testing. On the one hand, it can prove that a program has some required properties, or find counterexamples to prove the program does not have these properties. On the other hand, it is not as complex as theorem proving which needs more special theory on formalized reasoning and more mathematical knowledge. However, there are some limitations on existing finite state veri fication approach. The properties being proved must be the sets of event sequences which can be accepted by finite state automata, or equivalently, these properties can be represented by regular expressions. As we all know that the set of languages accepted by the finite automata is the smallest set according to Chomsky＇s classification. In this paper, the limitation of using only finite automata is discussed, and as an attempt to break through this limitation, a new approach, finite path verification, is presented here. By this new approach, the properties being proved can be represented by automata of any kinds. The model describing system is restricted to be acyclic at a cost. An approach named finite path testing is also presented for the cyclic system model in this paper. The correctness of a program cannot be validated directly by this approach as by other common software testing. However, if the testing cannot be passed, counterexamples then can be found to reveal the faults in the program. The testing here is different form commontesting for it is not to execute the actual program, but testing according to paths of the model.