登入選單

返回Google圖書搜尋

Formalizing Routing Models in ACL2

Warren A. Hunt

出版	Computer Science Department, University of Texas at Austin, 2008
URL	http://books.google.com.hk/books?id=MJGXDAEACAAJ&hl=&source=gbs_api

註釋

We present two preliminary formalizations of router networks, both expressed in the logic of the ACL2 theorem prover. One formalization focuses on connectivity requirements by formalizing validity, visibility, and a trivial example routing policy, and demonstrates the ability to execute specifications. The other formalization focuses on network security properties, specifically information-flow and non-interference, and includes theorems demonstrating these properties for a simple formalization of a router network.