{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:24:12Z","timestamp":1750220652299,"version":"3.41.0"},"reference-count":52,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2021,5,29]],"date-time":"2021-05-29T00:00:00Z","timestamp":1622246400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"ERC advanced","award":["695714"],"award-info":[{"award-number":["695714"]}]},{"name":"IMPEDE","award":["693606"],"award-info":[{"award-number":["693606"]}]},{"name":"European Research Council","award":["IMMUNOALZHEIMER"],"award-info":[{"award-number":["IMMUNOALZHEIMER"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2021,7,31]]},"abstract":"<jats:p>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.<\/jats:p>","DOI":"10.1145\/3427091","type":"journal-article","created":{"date-parts":[[2021,5,30]],"date-time":"2021-05-30T01:14:27Z","timestamp":1622337267000},"page":"1-20","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["SystemC Implementation of Stochastic Petri Nets for Simulation and Parameterization of Biological Networks"],"prefix":"10.1145","volume":"20","author":[{"given":"Nicola","family":"Bombieri","sequence":"first","affiliation":[{"name":"Dept. Computer Science - Univ. Verona, Italy"}]},{"given":"Silvia","family":"Scaffeo","sequence":"additional","affiliation":[{"name":"Dept. Computer Science - Univ. Verona, Italy"}]},{"given":"Antonio","family":"Mastrandrea","sequence":"additional","affiliation":[{"name":"Dept. Computer Science - Univ. Verona, Italy"}]},{"given":"Simone","family":"Caligola","sequence":"additional","affiliation":[{"name":"Dept. Computer Science - Univ. Verona, Italy"}]},{"given":"Tommaso","family":"Carlucci","sequence":"additional","affiliation":[{"name":"Dept. Medicine - Univ. Verona, Italy"}]},{"given":"Franco","family":"Fummi","sequence":"additional","affiliation":[{"name":"Dept. Computer Science - Univ. Verona, Italy"}]},{"given":"Carlo","family":"Laudanna","sequence":"additional","affiliation":[{"name":"Dept. Medicine - Univ. Verona, Italy"}]},{"given":"Gabriela","family":"Constantin","sequence":"additional","affiliation":[{"name":"Dept. Medicine - Univ. Verona, Italy"}]},{"given":"Rosalba","family":"Giugno","sequence":"additional","affiliation":[{"name":"Dept. Computer Science - Univ. Verona, Italy"}]}],"member":"320","published-online":{"date-parts":[[2021,5,29]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1371\/journal.pcbi.1003334"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1186\/s12859-015-0596-y"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1038\/nrg1272"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCBB.2016.2614301"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-12982-2_11"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10836-015-5514-8"},{"key":"e_1_2_1_7_1","first-page":"1","article-title":"On the evaluation of transactor-based verification for reusing TLM assertions and testbenches at RTL","volume":"1","author":"Bombieri N.","year":"2006","unstructured":"N. Bombieri , F. Fummi , and G. Pravadelli . 2006 . On the evaluation of transactor-based verification for reusing TLM assertions and testbenches at RTL . In Proc. of ACM\/IEEE DATE , Vol. 1. 1 \u2013 6 . N. Bombieri, F. Fummi, and G. Pravadelli. 2006. On the evaluation of transactor-based verification for reusing TLM assertions and testbenches at RTL. In Proc. of ACM\/IEEE DATE, Vol. 1. 1\u20136.","journal-title":"Proc. of ACM\/IEEE DATE"},{"key":"e_1_2_1_8_1","doi-asserted-by":"crossref","unstructured":"M. Boul\u00e9 and Z. Zilic. 2008. Generating Hardware Assertion Checkers: For Hardware Verification Emulation Post-fabrication Debugging and On-line Monitoring. Springer.  M. Boul\u00e9 and Z. Zilic. 2008. Generating Hardware Assertion Checkers: For Hardware Verification Emulation Post-fabrication Debugging and On-line Monitoring. Springer.","DOI":"10.1007\/978-1-4020-8586-4"},{"volume-title":"Proc. of the 2019 Forum on Specification and Design Languages (FDL\u201919)","author":"Caligola S.","key":"e_1_2_1_9_1","unstructured":"S. Caligola , T. Carlucci , F. Fummi , C. Laudanna , G. Constantin , N. Bombieri , and R. Giugno . 2019. Efficient simulation and parametrization of stochastic Petri nets in SystemC: A case study from systems biology . In Proc. of the 2019 Forum on Specification and Design Languages (FDL\u201919) . S. Caligola, T. Carlucci, F. Fummi, C. Laudanna, G. Constantin, N. Bombieri, and R. Giugno. 2019. Efficient simulation and parametrization of stochastic Petri nets in SystemC: A case study from systems biology. In Proc. of the 2019 Forum on Specification and Design Languages (FDL\u201919)."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1063\/1.1778376"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1093\/bib\/bbm029"},{"key":"e_1_2_1_12_1","first-page":"347","article-title":"Quantitative Petri net model of gene regulated metabolic networks in the cell","volume":"3","author":"Chen Ming","year":"2003","unstructured":"Ming Chen and Ralf Hofestaedt . 2003 . Quantitative Petri net model of gene regulated metabolic networks in the cell . In Silico Biology 3 , 3 (2003), 347 \u2013 365 . Ming Chen and Ralf Hofestaedt. 2003. Quantitative Petri net model of gene regulated metabolic networks in the cell. In Silico Biology 3, 3 (2003), 347\u2013365.","journal-title":"Silico Biology"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/225871.225880"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1186\/1742-4682-3-25"},{"volume-title":"17th IEEE Latin-American Test Symposium (LATS\u201916)","author":"Coati D.","key":"e_1_2_1_15_1","unstructured":"D. Coati , R. Distefano , N. Bombieri , F. Fummi , M. Mirenda , C. Laudanna , and R. Giugno . 2016. A SystemC-based platform for assertion-based verification and mutation analysis in systems biology . 17th IEEE Latin-American Test Symposium (LATS\u201916) , 159\u2013164. D. Coati, R. Distefano, N. Bombieri, F. Fummi, M. Mirenda, C. Laudanna, and R. Giugno. 2016. A SystemC-based platform for assertion-based verification and mutation analysis in systems biology. 17th IEEE Latin-American Test Symposium (LATS\u201916), 159\u2013164."},{"key":"e_1_2_1_16_1","volume-title":"Foster","author":"Coelho Claudionor-Nunes","year":"2008","unstructured":"Claudionor-Nunes Coelho Jr . and Harry D . Foster . 2008 . Assertion-Based Verification. Vol. 4 . Springer . Claudionor-Nunes Coelho Jr. and Harry D. Foster. 2008. Assertion-Based Verification. Vol. 4. Springer."},{"volume-title":"Proc. of the ACM Great Lakes Symposium on VLSI (GLSVLSI\u201915)","author":"Distefano R.","key":"e_1_2_1_17_1","unstructured":"R. Distefano , F. Fummi , C. Laudanna , N. Bombieri , and R. Giugno . 2015. A systemc platform for signal transduction modelling and simulation in systems biology . In Proc. of the ACM Great Lakes Symposium on VLSI (GLSVLSI\u201915) , 233\u2013236. R. Distefano, F. Fummi, C. Laudanna, N. Bombieri, and R. Giugno. 2015. A systemc platform for signal transduction modelling and simulation in systems biology. In Proc. of the ACM Great Lakes Symposium on VLSI (GLSVLSI\u201915), 233\u2013236."},{"volume-title":"2016 IEEE International High Level Design Validation and Test Workshop (HLDVT\u201916)","author":"Distefano R.","key":"e_1_2_1_18_1","unstructured":"R. Distefano , N. Goncharenko , F. Fummi , R. Giugno , G. D. Badery , and N. Bombieri . 2016. SyQUAL: A platform for qualitative modelling and simulation of biological systems . In 2016 IEEE International High Level Design Validation and Test Workshop (HLDVT\u201916) , 155\u2013161. R. Distefano, N. Goncharenko, F. Fummi, R. Giugno, G. D. Badery, and N. Bombieri. 2016. SyQUAL: A platform for qualitative modelling and simulation of biological systems. In 2016 IEEE International High Level Design Validation and Test Workshop (HLDVT\u201916), 155\u2013161."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCMS.2009.42"},{"key":"e_1_2_1_20_1","first-page":"141","article-title":"Uric acid induces caspase-1 activation, IL-1 secretion and P2X7 receptor dependent proliferation in primary human lymphocytes","volume":"17","author":"Eleftheriadis T.","year":"2013","unstructured":"T. Eleftheriadis , G. Pissas , A. Karioti , G. Antoniadi , S. Golfinopoulos , V. Liakopoulos , A. Mamara , M. Speletas , G. Koukoulis , and I. Stefanidis . 2013 . Uric acid induces caspase-1 activation, IL-1 secretion and P2X7 receptor dependent proliferation in primary human lymphocytes . Hippokratia 17 , 2 (2013), 141 . T. Eleftheriadis, G. Pissas, A. Karioti, G. Antoniadi, S. Golfinopoulos, V. Liakopoulos, A. Mamara, M. Speletas, G. Koukoulis, and I. Stefanidis. 2013. Uric acid induces caspase-1 activation, IL-1 secretion and P2X7 receptor dependent proliferation in primary human lymphocytes. Hippokratia 17, 2 (2013), 141.","journal-title":"Hippokratia"},{"volume-title":"Petri Net Synthesis","author":"Darondeau Philippe","key":"e_1_2_1_21_1","unstructured":"Philippe Darondeau , Eric Badouel , and Luca Bernardinello . 2015. Petri Net Synthesis . Springer-Verlag , Berlin . DOI:https:\/\/doi.org\/10.1007\/978-3-662-47967-4 Philippe Darondeau, Eric Badouel, and Luca Bernardinello. 2015. Petri Net Synthesis. Springer-Verlag, Berlin. DOI:https:\/\/doi.org\/10.1007\/978-3-662-47967-4"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1038\/nbt1356"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/s100090100058"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/0021-9991(76)90041-3"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1021\/j100540a008"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1093\/bioinformatics\/btn470"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.3389\/fbioe.2014.00091"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31131-4_22"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27793-4_13"},{"key":"e_1_2_1_30_1","volume-title":"The IB-NF-B signaling module: Temporal control and selective gene activation. Science 298, 5596","author":"Hoffmann Alexander","year":"2002","unstructured":"Alexander Hoffmann , Andre Levchenko , Martin L. Scott , and David Baltimore . 2002. The IB-NF-B signaling module: Temporal control and selective gene activation. Science 298, 5596 ( 2002 ), 1241\u20131245. Alexander Hoffmann, Andre Levchenko, Martin L. Scott, and David Baltimore. 2002. The IB-NF-B signaling module: Temporal control and selective gene activation. Science 298, 5596 (2002), 1241\u20131245."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1093\/bioinformatics\/btg015"},{"key":"e_1_2_1_32_1","unstructured":"IEEE. 2017. Property Specification Language - PSL. https:\/\/standards.ieee.org\/findstds\/standard\/1850-2010.html.  IEEE. 2017. Property Specification Language - PSL. https:\/\/standards.ieee.org\/findstds\/standard\/1850-2010.html."},{"key":"e_1_2_1_33_1","volume-title":"Oltvai","author":"Jeong Hawoong","year":"2001","unstructured":"Hawoong Jeong , Sean P. Mason , A.-L. Barab\u00e1si , and Zoltan N . Oltvai . 2001 . Lethality and centrality in protein networks. Nature 411, 6833 (2001), 41. Hawoong Jeong, Sean P. Mason, A.-L. Barab\u00e1si, and Zoltan N. Oltvai. 2001. Lethality and centrality in protein networks. Nature 411, 6833 (2001), 41."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1186\/1471-2105-7-56"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-014-0421-5"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03845-7_19"},{"key":"e_1_2_1_37_1","first-page":"389","article-title":"Biopathways representation and simulation on hybrid functional Petri net","volume":"3","author":"Matsuno Hiroshi","year":"2003","unstructured":"Hiroshi Matsuno , Yukiko Tanaka , Hitoshi Aoshima , Mika Matsui , Satoru Miyano , et\u00a0al. 2003 . Biopathways representation and simulation on hybrid functional Petri net . In Silico Biology 3 , 3 (2003), 389 \u2013 404 . Hiroshi Matsuno, Yukiko Tanaka, Hitoshi Aoshima, Mika Matsui, Satoru Miyano, et\u00a0al. 2003. Biopathways representation and simulation on hybrid functional Petri net. In Silico Biology 3, 3 (2003), 389\u2013404.","journal-title":"Silico Biology"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.compbiolchem.2005.10.007"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1021\/bi902202q"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0006-3495(04)74207-1"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCBB.2017.2733529"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.compbiolchem.2006.09.005"},{"key":"e_1_2_1_43_1","unstructured":"Karsten Schmidt. 2005. Controllability of open workflow nets. In EMISA. 236\u2013249.  Karsten Schmidt. 2005. Controllability of open workflow nets. In EMISA. 236\u2013249."},{"key":"e_1_2_1_44_1","first-page":"105","article-title":"Computational models of metabolism: Stability and regulation in metabolic networks","volume":"142","author":"Steuer Ralf","year":"2009","unstructured":"Ralf Steuer and Bjorn H. Junker . 2009 . Computational models of metabolism: Stability and regulation in metabolic networks . Advances in Chemical Physics 142 (2009), 105 . Ralf Steuer and Bjorn H. Junker. 2009. Computational models of metabolism: Stability and regulation in metabolic networks. Advances in Chemical Physics 142 (2009), 105.","journal-title":"Advances in Chemical Physics"},{"key":"e_1_2_1_45_1","unstructured":"Synopsys Inc.2003. Assertion-Based Verification. White paper http:\/\/www.synopsys.com.  Synopsys Inc.2003. Assertion-Based Verification. White paper http:\/\/www.synopsys.com."},{"key":"e_1_2_1_46_1","unstructured":"Systems Biology - A portal suite for Systems Biology. 2019. Model Repositories. http:\/\/systems-biology.org\/resources\/model-repositories.  Systems Biology - A portal suite for Systems Biology. 2019. Model Repositories. http:\/\/systems-biology.org\/resources\/model-repositories."},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1063\/1.4896985"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1186\/1742-4682-1-8"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1021\/acssynbio.8b00078"},{"volume-title":"How Petri Net Theory Serves Petri Net Model Checking: A Survey","author":"Wolf Karsten","key":"e_1_2_1_50_1","unstructured":"Karsten Wolf . 2019. How Petri Net Theory Serves Petri Net Model Checking: A Survey . Springer , Berlin , 36\u201363. DOI:https:\/\/doi.org\/10.1007\/978-3-662-60651-3_2 Karsten Wolf. 2019. How Petri Net Theory Serves Petri Net Model Checking: A Survey. Springer, Berlin, 36\u201363. DOI:https:\/\/doi.org\/10.1007\/978-3-662-60651-3_2"},{"key":"e_1_2_1_51_1","doi-asserted-by":"crossref","unstructured":"Y. Abarbanel et al. 2000. FOCS\u2013Automatic generation of simulation checkers from formal specifications. In Computer Aided Verification. Springer 538\u2013542.  Y. Abarbanel et al. 2000. FOCS\u2013Automatic generation of simulation checkers from formal specifications. In Computer Aided Verification. Springer 538\u2013542.","DOI":"10.1007\/10722167_40"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1186\/1752-0509-5-14"}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3427091","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3427091","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:02:24Z","timestamp":1750197744000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3427091"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,5,29]]},"references-count":52,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2021,7,31]]}},"alternative-id":["10.1145\/3427091"],"URL":"https:\/\/doi.org\/10.1145\/3427091","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"type":"print","value":"1539-9087"},{"type":"electronic","value":"1558-3465"}],"subject":[],"published":{"date-parts":[[2021,5,29]]},"assertion":[{"value":"2020-01-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2020-09-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-05-29","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}