FeaVer: Web GUI

Some viewgraphs and a random collection of screenshots of the FeaVer Web Gui and utilities from 1999.

Overview of the verification process as it is initiated through a Web browser, executed on the FeaVer hardware, and reported back to the user via the Web database.

The generic entry point to the verification system for PathStar.

A sample page with feature properties for call waiting.

The verification status report on that page.

The feature interaction table, defining all known feature interactions based on the Bellcore (Telcordia) documents.

The FeaVer hardware, while it was being constructed (here shown with 11 nodes online; 5 more were stacked on top of the column of CPUs shortly after this picture was taken. The two plugboards in the middle are console switches that allow us to link a keyboard, mouse, and display to any one of the nodes. The system is connected via a 100 MBs ethernet to our local network (and to the Windows NT server that runs the webserver and stores the Feaver database.)

A display that tracks the load on each of the 16 nodes in the FeaVer multiprocessor. The nodes have names chosen from a book on pig diseases: atresia, brucellosis, carbadox, colitis, cryptococcus, dermatosis, heptatosis, metritis, orf, pox, steatatis, tailfan, mad, mange, lice, pest. Each node runs as a compute server under the Plan9 operating system. It connects to a standard Windows NT PC, of the same speed, that stores the database and runs the webserver.

The progress of the checking progress for all feature properties simultaneously is tracked with the help of the above display. Each column represents a phase in the search iteration. Starting at the left of the screen, the search progresses from fast and coarse to slow and precise, for each new phase marking progress with a colored line. Each growing horizontal line is green while no errors are found; it turns red and stops growing as soon as a violation of the corresponding property was detected. By clicking the appropriate line segments, details on the property, on the violation of that property, or on the feature that the property belongs to can be inspected. The first errors are typically reported in just a few minutes after a new global sweep of the properties starts. To checks can be run as far as desired, up to extremely thorough overnight checks to identify also the most complex and unlikely types of bugs in an application (e.g. those requiring long sequences of unlikely event interleavings to occur).

Example of a graphical version of an error sequence.

And, yes, if you run 16 fast computers in parallel, things do go faster than if you use just one computer. Because the verification of each property can be performed independently from all others, FeaVer achieves a speedup in the verification process that is linear in the number of computers we use, without noticeable overhead.

Back to Main Page