search

nimble-code / Modex

a model extractor, to automatically extract Spin verification models from multi-threaded C code
18 stars 3 forks source link

Feaver #3

Closed RusherCircle closed 3 years ago

RusherCircle commented 3 years ago

i want to find the tools for modex,called FeaVer. But I can't find it. can you give me some suggestion? Thank you very much.

nimble-code commented 3 years ago

FeaVer was a system developed at Bell Labs about 22 years ago (1998-2000), see: http://spinroot.com/feaver/components.html there was a graphical user interface for it, written in tcl/tk, but that was linked closely to the feature verification effort for the voice/and data switch we were verifying at the time. Modex is the main model extraction tool that was used in this project.

RusherCircle commented 3 years ago

sorry，I have read the link of the FEAVER. But i can't find the download link of the Feaver. I have read some paper in which they use the Feaver. Can this tool be downloaded?

nimble-code commented 3 years ago

like I said above: feaver was a gui for the feature verification work we did on the Pathstar data switch. it's not a standalone application