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 (SPNs) have become a widespread and reference formalism to model metabolic networks thanks to their natural expressiveness to represent metabolites, reactions, molecule interactions, and simulation randomness due to system fluctuations and environmental noise. In the literature, starting from the network model and the complete set of system parameters, there exist frameworks that allow for dynamic system simulation. Nevertheless, they do not allow for automatic model parameterization, 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 parameterization of the networks. The user formally defines the network properties to be observed and the framework automatically extrapolates, 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 behavioral differences in the regulation of the entire purine network. We also show the scalability of the approach through the modeling and simulation of four biological networks, each one with different structural characteristics.
On Temporal Properties of Nested Petri Nets
