Achieving fault tolerance by a formally validated interaction policy