Recent progress in high-throughput data-production technologies pushes research towardsystems biology, focusing on the global interaction between the components ofbiomolecular processes. In this article we present a formal modelling environment fornetwork biology, called the Biochemical Abstract Machine (BIOCHAM). Biochamdelivers precise semantics to biomolecular interaction maps. Based on this formalsemantics, the Biocham system offers automated reasoning tools for querying the temporalproperties of the system under all its possible behaviours. We present the main features ofBiocham and report on our modelling experience with this language