Model Checking

Try basic model checking

• On classroom.cs.unc.edu
  • -- directory ~stotts/public_html/590/mcheck
  • -- remote login, must use this host,
  • -- it is a linux box with general public access


• You can go to that directory using a remote shell
  • cd ~stotts/public_html/590/mcheck


• You can also access the files there with a browser
  • https://www.cs.unc.edu/~stotts/590/mcheck


• Model checker program is mcb


• Files with “.net” suffix are petri net models
  • -- cannot be model checked directly
  • -- Must be converted to FSM form


• Files with “.fsm” suffix are in mcb state machine format and can be checked with mcb

More MCB Information