Abstract

Recent advances in Biology have shown that the amount and heterogeneity of the (post-genomic) data now available call for new techniques able to cope with such input and to build high-level models of the complex systems involved [18]. Arguably two key open issues in this emerging area of Computational Systems Biology concern the integration of qualitative and quantitative models and the revision of such integrated models.  The purpose of the Biochemical Abstract Machine (BIOCHAM) modelling environment is to provide for-malisms to describe biological mechanisms, including both the studied system and its properties, at different abstraction levels. Based on these formalisms it gives access to a set of tools, mostly focused around model-checking, that help the user in developing, curating, exchanging and refining his models. In this article we will take as an example invariant computation of the Petri net representing a biological reaction system, and show both a new efficient method for this step, as resolution of a constraint problem, and also how this analysis brings both qualitative and quantitative information on the models, in the form of con-servation laws, consistency checking, etc. ranging over all the above defined abstraction levels.