A significant part of the call processing software for Lucent's new PathStar~TM Access Server was checked with formal verification techniques. The verification system we Built for this purpose, named FeaVer, is accessed via a standard Web browser. The System maintains a database of feature requirements, together with the results of The most recently performed verifications. Via the browser the user can invoke new Verification runs, which are performed in the background with the help of a logic Model checking tool.
展开▼
