In this paper we propose a construction method of multiformalism specifications based on B and linear temporal logic. We examined this method with a case study of a communication protocol between an integrated circuit card and a device such a terminal. This study has been carried out in collaboration with the Schlumberger company. We show the current advantages and limits in combining many specifications formalisms and the associated toolkits: Atelier B and SPIN. Finally, we draw conclusions about future directions of research on the proof of heterogeneous specifications, incremental verification and ontool cooperation to assist in the verification step (e.g. a prover, a model-checker and an animator).