In E-Process Design and Assurance Using Model Checking [231] W. Wang et
al. describe the application of Verisoft and Spin, two model checkers, to verify
an E-commerce application. The specification uses temporal logic, while the
implementation uses C or Promela, depending on which model-checker is