Using the Extensible Model Checker XTL to Verify StAC Business Specifications
Juan Carlos Augusto, Michaël Leuschel, Michael J. Butler, Carla Ferreira · ePrints Soton (University of Southampton) · 2003
Abstract. StAC is a business specification language that has been developed as part of a partnership program between IBM UK Labs. and the University of Southampton. It is highly desirable for Business specification languages like StAC to have a way to explore the correctness of specifications. We provide some details about how XTL can provide model checking capabilities for StAC and why it proved to be more successful than SPIN and STeP in that sense. 1