The use of formal modelling in Systems Biology is a process of counter-example driven model refinement. We necessarily have to measure the quality of our models by comparing them to phenotype observations - simulation and verification are the tools we employ for this.  

In this talk we present a static analysis approach to early screening of model quality. Based on the formalism of BioAmbients we use our technique to establish provably sound over-approximations of system behaviours. 

We demonstrate the usefulness of the approach on a model of the LDL degradation pathway. Here we are able to show that our model captures enough detail to postdict the system perturbations arrising from certain genetic defects.