{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,11]],"date-time":"2026-07-11T08:14:20Z","timestamp":1783757660160,"version":"3.55.0"},"reference-count":88,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T00:00:00Z","timestamp":1782864000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T00:00:00Z","timestamp":1782864000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2026,6,2]],"date-time":"2026-06-02T00:00:00Z","timestamp":1780358400000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100002886","name":"China National Petroleum Corporation","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100002886","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100013076","name":"National Major Science and Technology Projects of China","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100013076","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Array"],"published-print":{"date-parts":[[2026,7]]},"DOI":"10.1016\/j.array.2026.100981","type":"journal-article","created":{"date-parts":[[2026,6,6]],"date-time":"2026-06-06T15:45:29Z","timestamp":1780760729000},"page":"100981","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":0,"special_numbering":"C","title":["Formal modeling and correctness verification of an AI drilling system based on Communicating Sequential Processes"],"prefix":"10.1016","volume":"30","author":[{"given":"Hao","family":"Yang","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Shunlei","family":"Xia","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yucheng","family":"Xue","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Xukun","family":"Yang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Fang","family":"Yang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-4669-6037","authenticated-orcid":false,"given":"Yang","family":"Yuan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Wanling","family":"Xie","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"78","reference":[{"key":"10.1016\/j.array.2026.100981_b1","series-title":"Communicating sequential processes: the first 25 years, symposium on the occasion of 25 years of CSP, London, UK, July 7-8, 2004, revised invited papers","first-page":"36","article-title":"Process algebra: A unifying approach","author":"Hoare","year":"2004"},{"key":"10.1016\/j.array.2026.100981_b2","series-title":"Automated technology for verification and analysis - 8th international symposium, ATVA 2010, Singapore, September 21-24, 2010. proceedings","first-page":"371","article-title":"Developing model checkers using PAT","author":"Liu","year":"2010"},{"key":"10.1016\/j.array.2026.100981_b3","series-title":"Principle of petri nets","author":"Yuan","year":"2025"},{"issue":"1","key":"10.1016\/j.array.2026.100981_b4","doi-asserted-by":"crossref","first-page":"49","DOI":"10.55730\/1300-0632.4162","article-title":"Distribution system reliability evaluation considering protection coordination using Petri nets","volume":"34","author":"Kumari","year":"2026","journal-title":"Turk J Electr Eng Comput Sci"},{"key":"10.1016\/j.array.2026.100981_b5","doi-asserted-by":"crossref","first-page":"833","DOI":"10.1109\/TR.2026.3656976","article-title":"Identification of deletion attacks in discrete-event systems through Petri nets enhanced with an observation structure","volume":"75","author":"Ahmed","year":"2026","journal-title":"IEEE Trans Reliab"},{"key":"10.1016\/j.array.2026.100981_b6","doi-asserted-by":"crossref","DOI":"10.1016\/j.eswa.2025.127803","article-title":"Formal verification of blockchain driven packet management in congested network using event B","volume":"283","author":"Singh","year":"2025","journal-title":"Expert Syst Appl"},{"key":"10.1016\/j.array.2026.100981_b7","doi-asserted-by":"crossref","DOI":"10.1016\/j.cosrev.2025.100758","article-title":"The beauty and the beast: A survey on process algebras and cybersecurity","volume":"57","author":"Costa","year":"2025","journal-title":"Comput Sci Rev"},{"issue":"11","key":"10.1016\/j.array.2026.100981_b8","doi-asserted-by":"crossref","first-page":"1573","DOI":"10.1142\/S0218194025410037","article-title":"Validating secure cloud communication mechanisms of graphene with CSP-based modeling","volume":"35","author":"Liu","year":"2025","journal-title":"Int J Softw Eng Knowl Eng"},{"key":"10.1016\/j.array.2026.100981_b9","doi-asserted-by":"crossref","DOI":"10.1016\/j.iot.2025.101543","article-title":"Formal verification and security analysis of fastdfs using process algebra","volume":"31","author":"Hou","year":"2025","journal-title":"Internet Things"},{"issue":"2","key":"10.1016\/j.array.2026.100981_b10","doi-asserted-by":"crossref","first-page":"301","DOI":"10.1142\/S0218194023500535","article-title":"Formalization and verification of enhanced group communication CoAP","volume":"34","author":"Chen","year":"2024","journal-title":"Int J Softw Eng Knowl Eng"},{"issue":"1","key":"10.1016\/j.array.2026.100981_b11","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1007\/s11036-024-02332-w","article-title":"Formalization and analysis of aeolus-based file system from process algebra perspective","volume":"29","author":"Hou","year":"2024","journal-title":"Mob Netw Appl"},{"issue":"1","key":"10.1016\/j.array.2026.100981_b12","doi-asserted-by":"crossref","first-page":"277","DOI":"10.2298\/CSIS210707057X","article-title":"Formalization and verification of kafka messaging mechanism using CSP","volume":"20","author":"Xu","year":"2023","journal-title":"Comput Sci Inf Syst"},{"issue":"4","key":"10.1016\/j.array.2026.100981_b13","doi-asserted-by":"crossref","first-page":"21:1","DOI":"10.1145\/3599731","article-title":"FVF-AKA: a formal verification framework of AKA protocols for multi-server IoT","volume":"35","author":"Fei","year":"2023","journal-title":"Form Asp Comput"},{"key":"10.1016\/j.array.2026.100981_b14","series-title":"48th IEEE annual computers, software, and applications conference","first-page":"2177","article-title":"Formal verification and security analysis of AMQP","author":"Liu","year":"2024"},{"issue":"3","key":"10.1016\/j.array.2026.100981_b15","doi-asserted-by":"crossref","first-page":"15","DOI":"10.3390\/software4030015","article-title":"Analysing concurrent queues using CSP: examining java\u2019s ConcurrentLinkedQueue","volume":"4","author":"Chalmers","year":"2025","journal-title":"Softw"},{"key":"10.1016\/j.array.2026.100981_b16","doi-asserted-by":"crossref","unstructured":"Edmonds C, Derrick J, Dongol B, Schellhorn G, Wehrheim H. Model Checking Buffered Durable Linearizability in CSP. In: Damiani F, Farrell M, editors. Integrated formal methods - 20th international conference, IFM 2025, Paris, France, November 19-21, 2025, proceedings. Lecture notes in computer science, p. 120\u201339.","DOI":"10.1007\/978-3-032-10794-7_7"},{"key":"10.1016\/j.array.2026.100981_b17","series-title":"33rd international symposium on modeling, analysis and simulation of computer and telecommunication systems","first-page":"1","article-title":"CSP based formal specification of a resource allocation for large-scale fog computing","author":"Hammal","year":"2025"},{"key":"10.1016\/j.array.2026.100981_b18","series-title":"Formal methods: foundations and applications - 27th Brazilian symposium, SBMF 2024, vit\u00f3ria, Brazil, December 4-6, 2024, proceedings","first-page":"68","article-title":"Verifying integrated designs of UML state machines and activities using CSP","author":"Ferreira","year":"2024"},{"issue":"1","key":"10.1016\/j.array.2026.100981_b19","first-page":"18:1","article-title":"Datapath combinational equivalence checking with hybrid sweeping engines and parallelization","volume":"31","author":"Chen","year":"2026","journal-title":"ACM Trans Des Autom Electr Syst"},{"key":"10.1016\/j.array.2026.100981_b20","doi-asserted-by":"crossref","DOI":"10.1016\/j.mejo.2023.106005","article-title":"An efficient circuit-based SAT solver and its application in logic equivalence checking","volume":"142","author":"Hu","year":"2023","journal-title":"Microelectron J"},{"issue":"4","key":"10.1016\/j.array.2026.100981_b21","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1007\/s10817-025-09742-9","article-title":"Theorem proving as constraint solving for coherent logic with function symbols","volume":"69","author":"Janicic","year":"2025","journal-title":"J Autom Reason"},{"issue":"3","key":"10.1016\/j.array.2026.100981_b22","doi-asserted-by":"crossref","first-page":"329","DOI":"10.1007\/s10836-024-06123-9","article-title":"Formal verification of universal numbers using theorem proving","volume":"40","author":"Rashid","year":"2024","journal-title":"J Electron Test"},{"key":"10.1016\/j.array.2026.100981_b23","article-title":"DM-check: Verifying invariants of concurrent systems by deductive model checking","volume":"149","author":"Bae","year":"2026","journal-title":"J Log Algebr Methods Program"},{"issue":"2","key":"10.1016\/j.array.2026.100981_b24","doi-asserted-by":"crossref","first-page":"14:1","DOI":"10.1145\/3736177","article-title":"Model checking of workflow nets with tables and constraints","volume":"20","author":"Song","year":"2025","journal-title":"ACM Trans Auton Adapt Syst"},{"issue":"5","key":"10.1016\/j.array.2026.100981_b25","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/32.588521","article-title":"The model checker SPIN","volume":"23","author":"Holzmann","year":"1997","journal-title":"IEEE Trans Softw Eng"},{"key":"10.1016\/j.array.2026.100981_b26","series-title":"19th IEEE international conference on industrial informatics","first-page":"1","article-title":"Promela formal modelling and verification of IEC 61499 systems with comparison to SMV","author":"Shatrov","year":"2021"},{"key":"10.1016\/j.array.2026.100981_b27","series-title":"Formal methods for the design of real-time systems, international school on formal methods for the design of computer, communication and software systems, SFM-RT 2004, bertinoro, Italy, September 13-18, 2004, revised lectures","first-page":"200","article-title":"A tutorial on uppaal","author":"Behrmann","year":"2004"},{"issue":"2","key":"10.1016\/j.array.2026.100981_b28","doi-asserted-by":"crossref","first-page":"272","DOI":"10.1002\/spe.3372","article-title":"A comprehensive survey of UPPAAL-assisted formal modeling and verification","volume":"55","author":"Zhou","year":"2025","journal-title":"Softw Pr Exp"},{"issue":"2","key":"10.1016\/j.array.2026.100981_b29","doi-asserted-by":"crossref","first-page":"667","DOI":"10.1007\/s10270-021-00916-8","article-title":"Probabilistic modelling and verification using RoboChart and PRISM","volume":"21","author":"Ye","year":"2022","journal-title":"Softw Syst Model"},{"key":"10.1016\/j.array.2026.100981_b30","series-title":"29th international symposium on distributed simulation and real time applications","first-page":"1","article-title":"Using uppaal and actors for property checking of mutual exclusion algorithms in anonymous memory","author":"Nigro","year":"2025"},{"key":"10.1016\/j.array.2026.100981_b31","doi-asserted-by":"crossref","DOI":"10.1016\/j.infsof.2022.107100","article-title":"A property specification pattern catalog for real-time system verification with UPPAAL","volume":"154","author":"Vogel","year":"2023","journal-title":"Inf Softw Technol"},{"issue":"2","key":"10.1016\/j.array.2026.100981_b32","doi-asserted-by":"crossref","first-page":"1611","DOI":"10.1007\/s10586-022-03963-y","article-title":"Abstracting IoT protocols using timed process algebra and SPIN model checker","volume":"26","author":"Kumar","year":"2023","journal-title":"Clust Comput"},{"key":"10.1016\/j.array.2026.100981_b33","series-title":"Model checking software - 31st international symposium, SPIN 2025, hamilton, on, Canada, May 7-8, 2025, proceedings","first-page":"44","article-title":"An efficient and versatile approach to shortest path problems in interprocedural programs","author":"Pinto","year":"2025"},{"issue":"1","key":"10.1016\/j.array.2026.100981_b34","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1016\/0304-3975(92)90182-F","article-title":"Conditioned rewriting logic as a united model of concurrency","volume":"96","author":"Meseguer","year":"1992","journal-title":"Theoret Comput Sci"},{"key":"10.1016\/j.array.2026.100981_b35","series-title":"Rewriting logic and its applications - 15th international workshop, WRLA 2024, Luxembourg city, Luxembourg, April 6-7, 2024, revised selected papers","first-page":"84","article-title":"Equivalence checking of quantum circuits based on Dirac notation in maude","author":"Do","year":"2024"},{"key":"10.1016\/j.array.2026.100981_b36","article-title":"Symbolic model checking quantum circuits in Maude","volume":"10","author":"Do","year":"2024","journal-title":"PeerJ Comput Sci"},{"key":"10.1016\/j.array.2026.100981_b37","series-title":"The 29th international DMS conference on visualization and visual languages, DMSVIVA 2023, KSIR virtual conference center, USA, June 29 - July 3, 2023","first-page":"1","article-title":"Formal specification and model checking of raft log replication in maude","author":"Ishibashi","year":"2023"},{"key":"10.1016\/j.array.2026.100981_b38","doi-asserted-by":"crossref","DOI":"10.1016\/j.future.2025.108148","article-title":"Formal specification and executable analysis of digital twin systems using Maude rewriting logic","volume":"176","author":"Alhazmi","year":"2026","journal-title":"Future Gener Comput Syst"},{"key":"10.1016\/j.array.2026.100981_b39","series-title":"Computer aided verification - 26th international conference, CAV 2014, held as part of the vienna summer of logic, VSL 2014, vienna, Austria, July 18-22, 2014. proceedings","first-page":"334","article-title":"The nuxmv symbolic model checker","author":"Cavada","year":"2014"},{"issue":"1","key":"10.1016\/j.array.2026.100981_b40","first-page":"4:1","article-title":"Specification and verification of the alpha swarm algorithm using NuXMV and GROOVE","volume":"38","author":"Saadat","year":"2026","journal-title":"Form Asp Comput"},{"key":"10.1016\/j.array.2026.100981_b41","series-title":"19th IEEE international conference on industrial informatics","first-page":"1","article-title":"Model-checking infinite-state nuclear safety I&C systems with nuXmv","author":"Pakonen","year":"2021"},{"key":"10.1016\/j.array.2026.100981_b42","series-title":"Specifying systems, the TLA+ language and tools for hardware and software engineers","author":"Lamport","year":"2002"},{"issue":"7","key":"10.1016\/j.array.2026.100981_b43","doi-asserted-by":"crossref","first-page":"1082","DOI":"10.3103\/S0146411625700373","article-title":"Using TLA+\/TLC for modeling and verification of cryptographic protocols","volume":"59","author":"Neyzov","year":"2025","journal-title":"Autom Control Comput Sci"},{"key":"10.1016\/j.array.2026.100981_b44","doi-asserted-by":"crossref","DOI":"10.1016\/j.scico.2024.103178","article-title":"Encoding TLA+ proof obligations safely for SMT","volume":"239","author":"Defourn\u00e9","year":"2025","journal-title":"Sci Comput Program"},{"key":"10.1016\/j.array.2026.100981_b45","series-title":"Advanced information networking and applications - proceedings of the 39th international conference on advanced information networking and applications, AINA 2025, Barcelona, Spain, 9-11 April 2025, volume 7","first-page":"314","article-title":"TLA+based specification and verification of a team formation protocol with message loss","author":"Niyogi","year":"2025"},{"key":"10.1016\/j.array.2026.100981_b46","series-title":"15th international conference on computing communication and networking technologies","first-page":"1","article-title":"TLA+ specification of aviation system with time analysis","author":"Das","year":"2024"},{"issue":"1","key":"10.1016\/j.array.2026.100981_b47","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1007\/s10009-025-00795-0","article-title":"Correct orchestration of federated learning generic algorithms: Python translation to CSP and verification by PAT","volume":"27","author":"Djukic","year":"2025","journal-title":"Int J Softw Tools Technol Transf"},{"key":"10.1016\/j.array.2026.100981_b48","series-title":"Formal methods and software engineering - 25th international conference on formal engineering methods, ICFEM 2024, hiroshima, Japan, December 2-6, 2024, proceedings","first-page":"391","article-title":"Model checking concurrency in smart contracts with a case study of safe remote purchase","author":"Yu","year":"2024"},{"key":"10.1016\/j.array.2026.100981_b49","doi-asserted-by":"crossref","DOI":"10.1016\/j.engappai.2020.104091","article-title":"GRAVITAS: A model checking based planning and goal reasoning framework for autonomous systems","volume":"97","author":"Bride","year":"2021","journal-title":"Eng Appl Artif Intell"},{"key":"10.1016\/j.array.2026.100981_b50","series-title":"2016 IEEE international conference on software quality, reliability and security","first-page":"244","article-title":"Modeling and verifying intelligent unit transmission protocol using CSP model checker PAT","author":"Shao","year":"2016"},{"issue":"4","key":"10.1016\/j.array.2026.100981_b51","doi-asserted-by":"crossref","first-page":"373","DOI":"10.1080\/17445760.2025.2493128","article-title":"Performance analysis of the shared memory system in stochastic process algebra dtsdPBC","volume":"40","author":"Tarasyuk","year":"2025","journal-title":"Int J Parallel Emergent Distrib Syst"},{"issue":"2","key":"10.1016\/j.array.2026.100981_b52","doi-asserted-by":"crossref","first-page":"475","DOI":"10.1007\/s11334-025-00611-7","article-title":"Formal model-driven security combining B-method and process algebra","volume":"21","author":"Idani","year":"2025","journal-title":"Innov Syst Softw Eng"},{"key":"10.1016\/j.array.2026.100981_b53","doi-asserted-by":"crossref","DOI":"10.1016\/j.scico.2025.103334","article-title":"Interleaving semantics and verification of UML 2 dynamic interactions using process algebra","volume":"246","author":"Belghiat","year":"2025","journal-title":"Sci Comput Program"},{"key":"10.1016\/j.array.2026.100981_b54","series-title":"NASA formal methods - 17th international symposium, NFM 2025, williamsburg, VA, USA, June 11-13, 2025, proceedings","first-page":"11","article-title":"Process-algebraic semantics for verifying intelligent robotic control software","author":"Attala","year":"2025"},{"key":"10.1016\/j.array.2026.100981_b55","series-title":"Proceedings of the 39th ACM SIGSIM conference on principles of advanced discrete simulation","first-page":"7","article-title":"Agent-based modeling in economics by process algebra","author":"Tschaikowski","year":"2025"},{"issue":"3","key":"10.1016\/j.array.2026.100981_b56","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1504\/IJCCBS.2024.143204","article-title":"Controlling dynamic crowdsourcing processes using multi-layered algebraic Petri nets","volume":"11","author":"Latreche","year":"2024","journal-title":"Int J Crit Comput Based Syst"},{"issue":"1","key":"10.1016\/j.array.2026.100981_b57","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1142\/S0218194023500468","article-title":"A modeling and verification method of cyber-physical systems based on AADL and process algebra","volume":"34","author":"Li","year":"2024","journal-title":"Int J Softw Eng Knowl Eng"},{"key":"10.1016\/j.array.2026.100981_b58","article-title":"Efficient analysis of belief properties in process algebra","volume":"141","author":"Moezkarimi","year":"2024","journal-title":"J Log Algebr Methods Program"},{"key":"10.1016\/j.array.2026.100981_b59","article-title":"Verification of data-aware process models: Checking soundness of data Petri nets","volume":"138","author":"Suvorov","year":"2024","journal-title":"J Log Algebr Methods Program"},{"issue":"2","key":"10.1016\/j.array.2026.100981_b60","doi-asserted-by":"crossref","first-page":"845","DOI":"10.1109\/TCST.2025.3647931","article-title":"Petri-net-based partial order reduction for model checking temporal epistemic logic on multiagent systems","volume":"34","author":"Guo","year":"2026","journal-title":"IEEE Trans Control Syst Technol"},{"issue":"3","key":"10.1016\/j.array.2026.100981_b61","doi-asserted-by":"crossref","first-page":"80:1","DOI":"10.1145\/3737698","article-title":"Modeling and verification of hybrid systems by extending AADL","volume":"35","author":"Xu","year":"2026","journal-title":"ACM Trans Softw Eng Methodol"},{"issue":"1","key":"10.1016\/j.array.2026.100981_b62","doi-asserted-by":"crossref","first-page":"16","DOI":"10.1007\/s11265-026-01986-x","article-title":"Formal analysis of lane-changing algorithms using probabilistic model checking","volume":"98","author":"Sarwar","year":"2026","journal-title":"J Signal Process Syst"},{"key":"10.1016\/j.array.2026.100981_b63","doi-asserted-by":"crossref","DOI":"10.1016\/j.artmed.2025.103154","article-title":"Symbolic and hybrid AI for brain tissue segmentation using spatial model checking","volume":"167","author":"Belmonte","year":"2025","journal-title":"Artif Intell Med"},{"issue":"5","key":"10.1016\/j.array.2026.100981_b64","doi-asserted-by":"crossref","first-page":"305","DOI":"10.1134\/S0361768825700185","article-title":"Software model checking for memory consistency verification","volume":"51","author":"Andrianov","year":"2025","journal-title":"Program Comput Softw"},{"key":"10.1016\/j.array.2026.100981_b65","series-title":"Application and theory of Petri nets and concurrency - 46th international conference, PETRI NETS 2025, Paris, France, June 22-27, 2025, proceedings","first-page":"174","article-title":"Statistical model checking of stochastic timed-arc Petri nets","author":"Dubois","year":"2025"},{"issue":"10","key":"10.1016\/j.array.2026.100981_b66","doi-asserted-by":"crossref","first-page":"4032","DOI":"10.1109\/TCAD.2025.3551658","article-title":"Revisiting assumptions ordering in CAR-based model checking","volume":"44","author":"Dong","year":"2025","journal-title":"IEEE Trans Comput Aided Des Integr Circuits Syst"},{"key":"10.1016\/j.array.2026.100981_b67","doi-asserted-by":"crossref","DOI":"10.1016\/j.automatica.2024.111625","article-title":"Liveness and deadlock-freeness verification and enforcement in bounded Petri nets using basis reachability graphs","volume":"164","author":"Gu","year":"2024","journal-title":"Autom"},{"issue":"2","key":"10.1016\/j.array.2026.100981_b68","article-title":"Safety and liveness of quantitative properties and automata","volume":"21","author":"Boker","year":"2025","journal-title":"Log Methods Comput Sci"},{"issue":"POPL","key":"10.1016\/j.array.2026.100981_b69","doi-asserted-by":"crossref","first-page":"1028","DOI":"10.1145\/3632877","article-title":"Mostly automated verification of liveness properties for distributed protocols with ranking functions","volume":"8","author":"Yao","year":"2024","journal-title":"Proc ACM Program Lang"},{"issue":"5","key":"10.1016\/j.array.2026.100981_b70","doi-asserted-by":"crossref","first-page":"2313","DOI":"10.1007\/s11276-021-02747-3","article-title":"Construction of data transmission consistency verification model of Petri net based on fuzzy C-means","volume":"28","author":"Wang","year":"2022","journal-title":"Wirel Netw."},{"key":"10.1016\/j.array.2026.100981_b71","series-title":"Knowledge-based and intelligent information & engineering systems: proceedings of the 26th international conference KES-2022, verona, Italy and virtual event, 7-9 September 2022","first-page":"4227","article-title":"A SERM based framework for defining and processing rules supporting the verification of data consistency and integrity","author":"Krakowiak","year":"2022"},{"key":"10.1016\/j.array.2026.100981_b72","doi-asserted-by":"crossref","DOI":"10.1016\/j.ress.2025.111691","article-title":"Enhanced verification of safety and security for advanced driver assistance systems","volume":"266","author":"Liu","year":"2026","journal-title":"Reliab Eng Syst Saf"},{"key":"10.1016\/j.array.2026.100981_b73","series-title":"Fortieth AAAI conference on artificial intelligence, thirty-eighth conference on innovative applications of artificial intelligence, sixteenth symposium on educational advances in artificial intelligence","first-page":"36438","article-title":"Probabilistic safety verification of neural policies via predicate abstraction","author":"Vinzent","year":"2026"},{"key":"10.1016\/j.array.2026.100981_b74","doi-asserted-by":"crossref","DOI":"10.1016\/j.sysconle.2024.106014","article-title":"Formal safety verification of non-deterministic systems based on probabilistic reachability computation","volume":"196","author":"Xiao","year":"2025","journal-title":"Syst Control Lett"},{"issue":"3","key":"10.1016\/j.array.2026.100981_b75","doi-asserted-by":"crossref","first-page":"767","DOI":"10.3390\/s24030767","article-title":"Process algebraic approach for probabilistic verification of safety and security requirements of smart IoT (internet of things) systems in digital twin","volume":"24","author":"Song","year":"2024","journal-title":"Sensors"},{"key":"10.1016\/j.array.2026.100981_b76","doi-asserted-by":"crossref","first-page":"249","DOI":"10.1016\/0304-3975(88)90030-8","article-title":"A timed model for communicating sequential processes","volume":"58","author":"Reed","year":"1988","journal-title":"Theoret Comput Sci"},{"key":"10.1016\/j.array.2026.100981_b77","series-title":"2014 theoretical aspects of software engineering conference","first-page":"90","article-title":"Modeling and verifying the TTCAN protocol using timed CSP","author":"Ran","year":"2014"},{"issue":"1","key":"10.1016\/j.array.2026.100981_b78","doi-asserted-by":"crossref","first-page":"3:1","DOI":"10.1145\/2430536.2430537","article-title":"Modeling and verifying hierarchical real-time systems using stateful timed CSP","volume":"22","author":"Sun","year":"2013","journal-title":"ACM Trans Softw Eng Methodol"},{"issue":"1","key":"10.1016\/j.array.2026.100981_b79","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1007\/s00607-024-01384-w","article-title":"Model verification of real-time and distributed stream processing architecture","volume":"107","author":"Ganji","year":"2025","journal-title":"Computing"},{"key":"10.1016\/j.array.2026.100981_b80","series-title":"Conference record of the fourth ACM symposium on principles of programming languages","first-page":"238","article-title":"Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints","author":"Cousot","year":"1977"},{"key":"10.1016\/j.array.2026.100981_b81","article-title":"Fundamentals of logic and computation - with practical automated reasoning and verification","author":"Hou","year":"2021"},{"key":"10.1016\/j.array.2026.100981_b82","article-title":"Interactive theorem proving and program development - coq\u2019art: The calculus of inductive constructions","author":"Bertot","year":"2004"},{"key":"10.1016\/j.array.2026.100981_b83","article-title":"Isabelle\/HOL - a proof assistant for higher-order logic","volume":"vol. 2283","author":"Nipkow","year":"2002"},{"issue":"POPL","key":"10.1016\/j.array.2026.100981_b84","doi-asserted-by":"crossref","first-page":"687","DOI":"10.1145\/3704860","article-title":"A verified foreign function interface between Coq and C","volume":"9","author":"Korkut","year":"2025","journal-title":"Proc ACM Program Lang"},{"key":"10.1016\/j.array.2026.100981_b85","series-title":"6th international workshop on formal methods for blockchains","first-page":"11:1","article-title":"Formally specifying contract optimizations with bisimulations in coq","author":"Sorensen","year":"2025"},{"issue":"6","key":"10.1016\/j.array.2026.100981_b86","doi-asserted-by":"crossref","first-page":"2450112:1","DOI":"10.1142\/S0218126624501123","article-title":"Formalizing the semantics of a classical-quantum imperative language in coq","volume":"33","author":"Shi","year":"2024","journal-title":"J Circuits Syst Comput"},{"key":"10.1016\/j.array.2026.100981_b87","doi-asserted-by":"crossref","DOI":"10.1016\/j.sysarc.2026.103724","article-title":"Formal semantics for hierarchical simulink diagrams in isabelle\/HOL","volume":"174","author":"Qi","year":"2026","journal-title":"J Syst Archit"},{"issue":"2","key":"10.1016\/j.array.2026.100981_b88","doi-asserted-by":"crossref","first-page":"15:1","DOI":"10.1145\/3700601","article-title":"Isabelle\/solidity: A deep embedding of solidity in Isabelle\/HOL","volume":"37","author":"Marmsoler","year":"2025","journal-title":"Form Asp Comput"}],"container-title":["Array"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S2590005626003048?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S2590005626003048?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2026,7,11]],"date-time":"2026-07-11T07:54:09Z","timestamp":1783756449000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S2590005626003048"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,7]]},"references-count":88,"alternative-id":["S2590005626003048"],"URL":"https:\/\/doi.org\/10.1016\/j.array.2026.100981","relation":{},"ISSN":["2590-0056"],"issn-type":[{"value":"2590-0056","type":"print"}],"subject":[],"published":{"date-parts":[[2026,7]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Formal modeling and correctness verification of an AI drilling system based on Communicating Sequential Processes","name":"articletitle","label":"Article Title"},{"value":"Array","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/j.array.2026.100981","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"\u00a9 2026 The Authors. Published by Elsevier Inc.","name":"copyright","label":"Copyright"}],"article-number":"100981"}}