Specification of an Integrated Circuit Card Protocol Application Using the B Method and Linear Temporal Logic. - Jacques Julliand; Bruno Legeard; Thierry Machicoane; Benoit Parreaux; Bruno Tatibouët (B, 1998)