SystemC implementation of Stochastic Petri Nets for Simulation and Parametrization of Biological Networks

Model development and simulation of biological networks is recognized as a key task in Systems Biology. Integrated with in-vitro and in-vivo experimental data, network simulation allows for the discovery of the dynamics that regulate biological systems. Stochastic Petri Nets (SPN) have become a widespread and reference formalism to model metabolic networks thanks to their natural expressiveness to represent metabolites, reactions, molecule interactions as well as simulation randomness due to system fluctuations and environmental noise. In literature, starting from the network model and the complete set of system parameters, there exist frameworks that allow for the dynamic system simulation. Nevertheless, they do not allow for automatic model parametrization, which is a crucial task to identify, in-silico, the network configurations that lead the model to satisfy specific temporal properties. To cover such a gap, this work first presents a framework to implement SPN models into SystemC code. Then, it shows how the framework allows for automatic parametrization of the networks. The user formally defines the network properties to be observed and the framework automatically extrapolate, through Assertion-based Verification (ABV), the parameter configurations that satisfy such properties. We present the results obtained by applying the proposed framework to model the complex metabolic network of the purine metabolism. We show how the automatic extrapolation of the system parameters allowed us to simulate the model under different conditions, which led to the understanding of behavioural differences in the regulation of the entire purine network. We also show the scalability of the approach through the modelling and simulation of four biological networks, each one with different structural characteristics.