The recent explosion of experimental data in biological research exposes the complexity of biological systems in unprecedented detail. The wealth of data simultaneously enables and necessitates the construction of models, which allow us to analyse and, ultimately, understand the biological system. Unfortunately, this data does not include the detailed quantitative information that would be needed construct mathematical models of such a system. Formal modelling and analysis techniques that have been developed for distributed computer systems, on the other hand, are starting to be recognised in the biological community as a powerful approach to exploit the available data. We propose to use Petri nets to construct such network models and to apply formal methods for analysis of the model state space. Our Petri net approach will enable the automated construction of models in Systems Biology for cases where existing data is insufficient to construct detailed mathematical models. Petri nets provide a formally defined, intuitive graphical representation that can unambiguously describe biological knowledge. Moreover, the same model can be executed to make testable predictions on the behaviour of the biological system. Model behaviour is sufficiently complex, that the analysis of the state-space will be challenging task and require the development of novel analysis approaches. The automation of parameter calibration together with the graphical formulation will bridge the gap between biology and formal methods, making formal methods directly applicable as an executable biology tool. Specifically, we will engineer Petri net models for the differentiation of blood stem cells into mature blood cells. A better understanding of the blood cell circuitry will help the development of clinical applications such as leukaemia treatment and secure and cheap blood transfusions.