{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T12:47:52Z","timestamp":1740142072276,"version":"3.37.3"},"reference-count":27,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2023,5,25]],"date-time":"2023-05-25T00:00:00Z","timestamp":1684972800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,5,25]],"date-time":"2023-05-25T00:00:00Z","timestamp":1684972800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/100010661","name":"Horizon 2020 Framework Programme","doi-asserted-by":"publisher","award":["732016"],"award-info":[{"award-number":["732016"]}],"id":[{"id":"10.13039\/100010661","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100012818","name":"Comunidad de Madrid","doi-asserted-by":"publisher","award":["S2018\/TCS-4314"],"award-info":[{"award-number":["S2018\/TCS-4314"]}],"id":[{"id":"10.13039\/100012818","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100004837","name":"Ministerio de Ciencia e Innovaci\u00f3n","doi-asserted-by":"publisher","award":["FAME-RTI2018-093608-B-C31"],"award-info":[{"award-number":["FAME-RTI2018-093608-B-C31"]}],"id":[{"id":"10.13039\/501100004837","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Innovations Syst Softw Eng"],"published-print":{"date-parts":[[2024,3]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>High-level Petri nets such as coloured Petri nets (CPNs) are characterized by the combination of Petri nets and a high-level programming language. In CPNs and CPN Tools, the inscriptions (e.g. arc expressions and guards) are specified using Standard ML. The application of simulation and state space exploration for validating CPN models traditionally focuses on behavioural properties related to net structure, i.e. places and transitions. This means that the net inscriptions are only implicitly validated, and the extent to which their sub-expressions have been covered is not made explicit. This paper extends our previous work on coverage analysis of net inscriptions of CPN models. In particular, we improve the CPN Tools library responsible for annotating, instrumenting and collecting the evaluation of Boolean conditions for determining the coverage criteria based on model executions. The library now automates most of the instrumentation parts that were done manually before and integrates the reports of the coverage analysis into the CPN Tools GUI. We evaluate our approach on new publicly available CPN models.<\/jats:p>","DOI":"10.1007\/s11334-023-00528-z","type":"journal-article","created":{"date-parts":[[2023,5,25]],"date-time":"2023-05-25T08:02:07Z","timestamp":1685001727000},"page":"17-30","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Coverage visualization and analysis of net inscriptions in coloured Petri net models"],"prefix":"10.1007","volume":"20","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1571-0964","authenticated-orcid":false,"given":"Faustin","family":"Ahishakiye","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5111-8357","authenticated-orcid":false,"given":"Jos\u00e9 Ignacio Requeno","family":"Jarabo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1465-5791","authenticated-orcid":false,"given":"Lars Michael","family":"Kristensen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1031-6936","authenticated-orcid":false,"given":"Volker","family":"Stolz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,5,25]]},"reference":[{"key":"528_CR1","unstructured":"Hayhurst KJ, Veerhusen DS, Chilenski JJ, Rierson LK (2001) A practical tutorial on modified condition\/decision coverage. Technical Report NASA\/TM-2001-210876, NASA Langley Server. https:\/\/dl.acm.org\/doi\/book\/10.5555\/886632"},{"key":"528_CR2","first-page":"13","volume-title":"Developing safety-critical software: a practical guide for aviation software and DO-178C compliance","author":"L Rierson","year":"2013","unstructured":"Rierson L (2013) Developing safety-critical software: a practical guide for aviation software and DO-178C compliance, 1st edn. CRC Press, Boca Raton, pp 13\u201346","edition":"1"},{"key":"528_CR3","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1145\/2663340","volume":"58","author":"K Jensen","year":"2015","unstructured":"Jensen K, Kristensen LM (2015) Colored petri nets: a graphical language for formal modeling and validation of concurrent systems. Commun ACM 58:61\u201370. https:\/\/doi.org\/10.1145\/2663340","journal-title":"Commun ACM"},{"key":"528_CR4","unstructured":"Jensen K, Christensen S, Kristensen LM, Michael W (2010) CPN tools. http:\/\/cpntools.org\/"},{"key":"528_CR5","unstructured":"Pothon F (2012) DO-178C\/ED-12C versus DO-178B\/ED-12B: changes and improvements. Technical report, AdaCore"},{"issue":"5","key":"528_CR6","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1049\/sej.1994.0025","volume":"9","author":"JC John","year":"1994","unstructured":"John JC, Steven PM (1994) Applicability of modified condition\/decision coverage to software testing. Softw Eng J 9(5):193\u2013200","journal-title":"Softw Eng J"},{"key":"528_CR7","doi-asserted-by":"publisher","unstructured":"Ahishakiye F, Jarabo JR, Kristensen LM, Stolz V (2020) Coverage analysis of net inscriptions in Coloured Petri Net models. In: Hedia BB, Chen Y, Liu G, Yu Z (eds) 14th International conference on verification and evaluation of computer and communication systems (VECOS). LNCS, vol 12519, Springer, Cham, pp 68\u201383. https:\/\/doi.org\/10.1007\/978-3-030-65955-4_6","DOI":"10.1007\/978-3-030-65955-4_6"},{"key":"528_CR8","doi-asserted-by":"publisher","unstructured":"Stolz V, Jarabo JR, Ahishakiye F, Kristensen LM (2023) Data set for \u201ccoverage visualization and analysis of net inscriptions in coloured petri net models\u201d https:\/\/doi.org\/10.5281\/zenodo.7957119","DOI":"10.5281\/zenodo.7957119"},{"key":"528_CR9","unstructured":"Cornett S (1996\u20132014) Code coverage analysis. Available at https:\/\/www.bullseye.com\/coverage.html, Accessed 20 Mar 2023"},{"key":"528_CR10","unstructured":"John JC (2001) An investigation of three forms of the modified condition decision coverage (MC\/DC) criterion. Technical report, Office of Aviation Research"},{"key":"528_CR11","doi-asserted-by":"publisher","unstructured":"Heimdahl MPE, Whalen MW, Rajan A, Staats M (2008) On MC\/DC and implementation structure: an empirical study. In: Proceedings of IEEE\/AIAA 27th digital avionics systems conference, pp 5\u2013315. https:\/\/doi.org\/10.1109\/DASC.2008.4702848","DOI":"10.1109\/DASC.2008.4702848"},{"key":"528_CR12","doi-asserted-by":"publisher","unstructured":"Vilkomir S, Bowen J (2002) Reinforced condition\/decision coverage (RC\/DC): a new criterion for software testing. In: Proceedings of ZB 2002: formal specification and development in Z and B. LNCS, vol 2272, Springer, Berlin, Heidelberg, pp 291\u2013308. https:\/\/doi.org\/10.1007\/3-540-45648-1_15","DOI":"10.1007\/3-540-45648-1_15"},{"key":"528_CR13","unstructured":"Certification authorities software team (CAST): rationale for accepting masking MC\/DC in certification projects. Technical report, Position Paper CAST-6 (2001)"},{"issue":"2","key":"528_CR14","doi-asserted-by":"publisher","first-page":"7515","DOI":"10.4249\/scholarpedia.7515","volume":"4","author":"M Tofte","year":"2009","unstructured":"Tofte M (2009) Standard ML language. Scholarpedia 4(2):7515. https:\/\/doi.org\/10.4249\/scholarpedia.7515","journal-title":"Scholarpedia"},{"key":"528_CR15","doi-asserted-by":"publisher","first-page":"254","DOI":"10.1016\/j.jlamp.2019.02.004","volume":"104","author":"R Wang","year":"2019","unstructured":"Wang R, Kristensen LM, Meling H, Stolz V (2019) Automated test case generation for the Paxos single-decree protocol using a Coloured Petri Net model. J Log Algebraic Methods Program 104:254\u2013273. https:\/\/doi.org\/10.1016\/j.jlamp.2019.02.004","journal-title":"J Log Algebraic Methods Program"},{"key":"528_CR16","doi-asserted-by":"publisher","unstructured":"Rodr\u00edguez A, Kristensen L.M, Rutle A (2019) Formal modelling and incremental verification of the MQTT IoT protocol. In: Proceedings of transaction on Petri Nets and other models of concurrency. LNCS, vol 11790, pp 126\u2013145. Berlin, Heidelberg. https:\/\/doi.org\/10.1007\/978-3-662-60651-3_5","DOI":"10.1007\/978-3-662-60651-3_5"},{"issue":"18","key":"528_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1002\/cpe.4179","volume":"29","author":"C Pascal","year":"2017","unstructured":"Pascal C, Panescu D (2017) A Colored Petri Net model for DisCSP algorithms. Concurr Comput Pract Exp 29(18):1\u201323","journal-title":"Concurr Comput Pract Exp"},{"key":"528_CR18","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.scico.2019.04.002","volume":"181","author":"A Gkolfi","year":"2019","unstructured":"Gkolfi A, Din CC, Johnsen EB, Kristensen LM, Steffen M, Yu IC (2019) Translating active objects into Colored Petri Nets for communication analysis. Sci Comput Program 181:1\u201326. https:\/\/doi.org\/10.1016\/j.scico.2019.04.002","journal-title":"Sci Comput Program"},{"key":"528_CR19","unstructured":"Caesarea Medical Electronics: Niki T34 syringe pump instruction manual (2008) https:\/\/manuals.plus\/cme\/cme-niki-t34-stringe-pump-manual-pdf"},{"key":"528_CR20","doi-asserted-by":"publisher","unstructured":"Silva BCF, Carvalho G, Sampaio A (2015) Test case generation from natural language requirements using CPN simulation. In: Proceedings of 19th Brazilian symposium on formal methods. LNCS, vol 9526. Springer, Berlin, Heidelberg. pp 178\u2013193. https:\/\/doi.org\/10.1007\/978-3-319-29473-5_11","DOI":"10.1007\/978-3-319-29473-5_11"},{"key":"528_CR21","doi-asserted-by":"publisher","unstructured":"Ghosh S, France R, Braganza C, Kawane N, Andrews A (2003) Orest Pilskalns: test adequacy assessment for UML design model testing. In: Proceedings of 14th international symposium on software reliability engineering, ISSRE\u201903., pp 332\u2013343. https:\/\/doi.org\/10.1109\/ISSRE.2003.1251054","DOI":"10.1109\/ISSRE.2003.1251054"},{"issue":"1","key":"528_CR22","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1109\/TR.2014.2354172","volume":"64","author":"D Xu","year":"2015","unstructured":"Xu D, Xu W, Kent M, Thomas L, Wang L (2015) An automated test generation technique for software quality assurance. IEEE Reliabil 64(1):247\u2013268. https:\/\/doi.org\/10.1109\/TR.2014.2354172","journal-title":"IEEE Reliabil"},{"key":"528_CR23","doi-asserted-by":"publisher","unstructured":"Paul TK, Lau MF (2014) A systematic literature review on modified condition and decision coverage. In: Proceedings of the 29th annual ACM symposium on applied computing. SAC \u201914, Association for Computing Machinery, New York, USA, pp 1301\u20131308. https:\/\/doi.org\/10.1145\/2554850.2555004","DOI":"10.1145\/2554850.2555004"},{"key":"528_CR24","doi-asserted-by":"publisher","unstructured":"Ahishakiye F, Jak\u0161i\u0107 S, Stolz V, Lange FD, Schmitz M, Thoma D (2019) Non-intrusive MC\/DC measurement based on traces. In: M\u00e9ry D, Qin S (eds) Intlernational symposium on theoretical aspects of software engineering, IEEE, Guilin, China, pp 86\u201392 https:\/\/doi.org\/10.1109\/TASE.2019.00-15","DOI":"10.1109\/TASE.2019.00-15"},{"key":"528_CR25","unstructured":"Simulink: types of model coverage. https:\/\/se.mathworks.com\/help\/slcoverage\/ug\/types-of-model-coverage.html Accessed 06 Apr 2022"},{"key":"528_CR26","unstructured":"Lill R, Saglietti F (2013) Model-based Testing of cooperating robotic systems using Coloured Petri Nets. In: Proceedings of SAFECOMP 2013 - Workshop DECS (ERCIM\/EWICS Workshop on Dependable Embedded and Cyber-physical Systems) of the 32nd international conference on computer safety, reliability and security, Toulouse, France. https:\/\/hal.archives-ouvertes.fr\/hal-00848597"},{"key":"528_CR27","doi-asserted-by":"crossref","unstructured":"Sim\u00e3o A, Do S, Souza S, Maldonado J (2003) A family of coverage testing criteria for Coloured Petri Nets. In: Proceedings of 17th Brazilian symposium on software engineering (SBES\u20192003), pp 209\u2013224","DOI":"10.5753\/sbes.2003.23862"}],"container-title":["Innovations in Systems and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-023-00528-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11334-023-00528-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-023-00528-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,20]],"date-time":"2024-02-20T10:20:45Z","timestamp":1708424445000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11334-023-00528-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,5,25]]},"references-count":27,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2024,3]]}},"alternative-id":["528"],"URL":"https:\/\/doi.org\/10.1007\/s11334-023-00528-z","relation":{},"ISSN":["1614-5046","1614-5054"],"issn-type":[{"type":"print","value":"1614-5046"},{"type":"electronic","value":"1614-5054"}],"subject":[],"published":{"date-parts":[[2023,5,25]]},"assertion":[{"value":"12 April 2022","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"15 March 2023","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"25 May 2023","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}