Automated formal verification of protocols

被引：0

作者：

Avresky, DR

Vassilaras, S

机构：

来源：

SIXTH INTERNATIONAL CONFERENCE ON COMPUTER COMMUNICATIONS AND NETWORKS, PROCEEDINGS | 1997年

关键词：

D O I：

10.1109/ICCCN.1997.623308

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

We adopt a formalism to describe protocols that is close to the human way of thinking and can be easily used to perform reachability analysis of the described protocol in a state-transition format. This formalism allows for can execution tree (ET) to be generated from a set of assertions such that all paths from the root to the leaves are well-defined formulas. We then extend the formalism with regards to real-time properties. Finally, we present a software verification tool, Verify, that implements the above features in the analysis of protocols.

引用

页码：166 / 169

页数：4