Animation and Model Checking of CSP and B using Prolog Technology
Michaël Leuschel, Laksono Adhianto, Michael J. Butler, Carla Ferreira, L. A. Mikhailov · ePrints Soton (University of Southampton) · 2001
We describe practical experiences of using a logic programming based approach to model and reason about critical systems. We argue that logic programming with co-routining, constraints, and tabling is a good foundation for developing, animating, and model checking new specification languages. We present animators and model checkers currently being developed for two different extensions of CSP and for the B method.