{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,21]],"date-time":"2026-08-21T05:26:00Z","timestamp":1787289960146,"version":"build-2736575974"},"reference-count":42,"publisher":"IEEE","license":[{"start":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T00:00:00Z","timestamp":1782864000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T00:00:00Z","timestamp":1782864000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T00:00:00Z","timestamp":1782864000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026,7]]},"DOI":"10.1109\/compsac69091.2026.00065","type":"proceedings-article","created":{"date-parts":[[2026,8,20]],"date-time":"2026-08-20T19:09:51Z","timestamp":1787252991000},"page":"446-455","source":"Crossref","is-referenced-by-count":0,"title":["Stepwise PCTL Generation with Closed-Loop Validation for Automated SysML Activity Diagram Verification"],"prefix":"10.1109","author":[{"given":"Jia","family":"Xu","sequence":"first","affiliation":[{"name":"Institute of Software, University of Chinese Academy of Sciences"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lei","family":"Yu","sequence":"additional","affiliation":[{"name":"Institute of Software, University of Chinese Academy of Sciences"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Peng","family":"Wang","sequence":"additional","affiliation":[{"name":"Institute of Software, University of Chinese Academy of Sciences"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Li","family":"Yang","sequence":"additional","affiliation":[{"name":"Institute of Software, University of Chinese Academy of Sciences"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Changzhi","family":"Deng","sequence":"additional","affiliation":[{"name":"Institute of Software, University of Chinese Academy of Sciences"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"YuSheng","family":"Liu","sequence":"additional","affiliation":[{"name":"Zhejiang University"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"DongXing","family":"Teng","sequence":"additional","affiliation":[{"name":"Institute of Software, University of Chinese Academy of Sciences"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Fengjun","family":"Zhang","sequence":"additional","affiliation":[{"name":"Institute of Software, University of Chinese Academy of Sciences"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"ref1","article-title":"INCOSE","volume-title":"INCOSE Systems Engineering Handbook","year":"2023"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1002\/sys.21438"},{"key":"ref3","year":"2023","journal-title":"OMG Systems Modeling Language (OMG SysML) Version 1.6"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211866"},{"key":"ref6","volume-title":"Model Based System Engineering applied to Small Satellite Systems","author":"Calo","year":"2020"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2019.110453"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.64808\/engineeringperspective.1760896"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1145\/3631976"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1115\/1.4051781"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1109\/ETFA65518.2025.11205621"},{"key":"ref12","first-page":"234","article-title":"Template-based PCTL generation for model checking","volume-title":"Proc. 41st Int. Conf. Softw. Eng. (ICSE)","author":"Johnson"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-017-0465-2"},{"key":"ref14","volume-title":"GPT-4 technical report","year":"2024"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-99447-0_3"},{"key":"ref16","article-title":"FVDebug: An LLM-Driven Debugging Assistant for Automated Root Cause Analysis of Formal Verification Failures","author":"Bai","year":"2025","journal-title":"arXiv preprint"},{"key":"ref17","first-page":"456","article-title":"VeriPlan: LLM-assisted PCTL generation for probabilistic model checking","volume-title":"Proc. 47th Int. Conf. Softw. Eng. (ICSE)","author":"Lee"},{"key":"ref18","article-title":"Communication and Concurrency","volume-title":"Upper Saddle River","author":"Milner","year":"1989"},{"key":"ref19","volume-title":"DO-178C: Software Considerations in Airborne Systems and Equipment Certification","year":"2011"},{"key":"ref20","volume-title":"ISO 26262: Road Vehicles-Functional Safety","year":"2018"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1002\/qre.2715"},{"issue":"8","key":"ref22","first-page":"1","article-title":"Survey of model-based systems engineering (MBSE) methodologies","volume":"25","author":"Estefan","year":"2007","journal-title":"INCOSE MBSE Focus Group"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2025.3587786"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.31891\/csit-2023-3-11"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1016\/j.rico.2024.100511"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.52202\/075280-2019"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1109\/CGO.2004.1281665"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1145\/3716167"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1201\/b10094"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1109\/ieeestd.1998.87820"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1002\/9780470249260"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1976.233837"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1201\/b17461"},{"key":"ref34","article-title":"IBM Rational Rhapsody: Model-driven development for systems and software","volume-title":"IBM Corp.","year":"2024"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1017\/cbo9780511612398"},{"key":"ref36","volume-title":"The Art of Computer Systems Performance Analysis: Techniques for Experimental Design, Measurement, Simulation, and Modeling","author":"Jain","year":"1991"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-29044-2"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1177\/001316446002000104"},{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1007\/bfb0058022"},{"key":"ref40","volume-title":"Principles of Model Checking","author":"Baier","year":"2008"},{"key":"ref41","first-page":"203","article-title":"The PRISM benchmark suite","volume-title":"Proc. 20th Int. Conf. Quant. Eval. Syst. (QEST)","author":"Kwiatkowska"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2025.3635153"}],"event":{"name":"2026 IEEE 50th Annual Computers, Software, and Applications Conference (COMPSAC)","location":"Madrid, Spain","start":{"date-parts":[[2026,7,7]]},"end":{"date-parts":[[2026,7,10]]}},"container-title":["2026 IEEE 50th Annual Computers, Software, and Applications Conference (COMPSAC)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx8\/11645011\/11645104\/11645121.pdf?arnumber=11645121","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,8,21]],"date-time":"2026-08-21T05:04:52Z","timestamp":1787288692000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/11645121\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,7]]},"references-count":42,"URL":"https:\/\/doi.org\/10.1109\/compsac69091.2026.00065","relation":{},"subject":[],"published":{"date-parts":[[2026,7]]}}}