{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,7]],"date-time":"2025-12-07T13:02:00Z","timestamp":1765112520723},"reference-count":52,"publisher":"Oxford University Press (OUP)","issue":"2","license":[{"start":{"date-parts":[[2021,10,25]],"date-time":"2021-10-25T00:00:00Z","timestamp":1635120000000},"content-version":"vor","delay-in-days":2,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"Ministero dell'Istruzione, dell\u2019Universit\u00e0 e della Ricerca, Italy"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023,2,19]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Unmanned aerial vehicle (UAV) co-operative systems are complex cyber-physical systems that integrate a high-level control algorithm with pre-existing closed implementations of lower-level vehicle kinematics. In model-driven development, simulation is one of the techniques that are usually applied, together with testing, in the analysis of system behaviours. This work proposes a method and tools to validate the design of UAV co-operative systems based on co-simulation and formal verification. The method uses the Prototype Verification System, an interactive theorem prover based on a higher-order logic language, and the Functional Mock-up Interface, a widely accepted standard for co-simulation. In this paper, results on the co-simulation and proofs of safety requirements of a representative co-ordination algorithm are shown and discussed in a scenario where quadcopters are deployed and perform space-coverage operations.<\/jats:p>","DOI":"10.1093\/comjnl\/bxab161","type":"journal-article","created":{"date-parts":[[2021,9,30]],"date-time":"2021-09-30T19:28:29Z","timestamp":1633030109000},"page":"295-317","source":"Crossref","is-referenced-by-count":7,"title":["Co-simulation and Formal Verification of Co-operative Drone Control With Logic-Based Specifications"],"prefix":"10.1093","volume":"66","author":[{"given":"Cinzia","family":"Bernardeschi","sequence":"first","affiliation":[{"name":"Department of Information Engineering , University of Pisa, Pisa, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrea","family":"Domenici","sequence":"additional","affiliation":[{"name":"Department of Information Engineering , University of Pisa, Pisa, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Adriano","family":"Fagiolini","sequence":"additional","affiliation":[{"name":"Department of Engineering , University of Palermo, Palermo, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Maurizio","family":"Palmieri","sequence":"additional","affiliation":[{"name":"Department of Information Engineering , University of Pisa, Pisa, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"286","published-online":{"date-parts":[[2021,10,23]]},"reference":[{"key":"2023022013494759700_","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","article-title":"A theory of timed automata","volume":"126","author":"Alur","year":"1994","journal-title":"Theor. Comput. Sci."},{"key":"2023022013494759700_","first-page":"238","article-title":"Co-simulation of Embedded Systems in a Heterogeneous MoC-Based Modeling Framework","volume-title":"The 6th IEEE Int. Symposium on Industrial and Embedded Systems","author":"Attarzadeh Niaki","year":"2011"},{"key":"2023022013494759700_","first-page":"125","article-title":"UPPAAL 4.0","volume-title":"The 3rd Int. Conf. on Quantitative Evaluation of Systems (QEST 2006)","author":"Behrmann","year":"2006"},{"key":"2023022013494759700_","first-page":"1","article-title":"Block-Based Models and Theorem Proving in Model-Based Development","volume-title":"The 2nd Interactive Workshop on the Industrial Application of Verification and Testing, ETAPS 2020 Workshop (InterAVT 2020)","author":"Bernardeschi","year":"2020"},{"key":"2023022013494759700_","doi-asserted-by":"crossref","first-page":"1","DOI":"10.3390\/en13164057","article-title":"Formal verification and co-simulation in the design of a synchronous motor control algorithm","volume":"13","author":"Bernardeschi","year":"2020","journal-title":"Energies"},{"key":"2023022013494759700_","doi-asserted-by":"crossref","first-page":"409","DOI":"10.1016\/j.ipl.2016.02.001","article-title":"Verifying safety properties of a nonlinear control by interactive theorem proving with the prototype verification system","volume":"116","author":"Bernardeschi","year":"2016","journal-title":"Inf. Process. Lett."},{"key":"2023022013494759700_","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1109\/ISCC.2016.7543728","article-title":"Modeling Communication Network Requirements for an Integrated Clinical Environment in the Prototype Verification System","volume-title":"The 2016 IEEE Symposium on Computers and Communication (ISCC)","author":"Bernardeschi","year":"2016"},{"key":"2023022013494759700_","doi-asserted-by":"crossref","first-page":"512","DOI":"10.1109\/TSE.2017.2694423","article-title":"A PVS-Simulink integrated environment for model-based analysis of cyber-physical systems","volume":"44","author":"Bernardeschi","year":"2018","journal-title":"IEEE Trans. Softw. Eng."},{"key":"2023022013494759700_","first-page":"1","article-title":"Formal verification in the loop to enhance verification of safety-critical cyber-physical systems","volume":"77","author":"Bernardeschi","year":"2019","journal-title":"Electronic Communications of the EASST, Interactive Workshop on the Industrial Application of Verification and Testing, ETAPS 2019 Workshop"},{"key":"2023022013494759700_","first-page":"105","article-title":"The Functional Mockup Interface for Tool independent Exchange of Simulation Models","volume-title":"Proc. of the 8th Int. Modelica Conf.","author":"Blochwitz","year":"2011"},{"key":"2023022013494759700_","first-page":"208","article-title":"Formally Verified Differential Dynamic Logic","volume-title":"Proc. of the 6th ACM SIGPLAN Conf. on Certified Programs and Proofs, CPP 2017","author":"Bohrer","year":"2017"},{"key":"2023022013494759700_","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1016\/j.trc.2002.10.002","article-title":"Hardware-in-the-loop simulation","volume":"12","author":"Bullock","year":"2004","journal-title":"Transport. Res. Part C Emerg. Technol."},{"key":"2023022013494759700_","first-page":"1","article-title":"Review of unmanned aerial vehicle swarm communication architectures and routing protocols","volume":"10","author":"Chen","year":"2020","journal-title":"Appl. Sci."},{"key":"2023022013494759700_","doi-asserted-by":"crossref","first-page":"243","DOI":"10.1109\/TRA.2004.824698","article-title":"Coverage control for mobile sensing networks","volume":"20","author":"Cort\u00e9s","year":"2004","journal-title":"IEEE Trans. Robotics Automation"},{"key":"2023022013494759700_","doi-asserted-by":"crossref","first-page":"1655","DOI":"10.1007\/s10270-017-0633-6","article-title":"Hybrid co-simulation: it\u2019s about time","volume":"18","author":"Cremona","year":"2019","journal-title":"Softw. Syst. Model."},{"key":"2023022013494759700_","doi-asserted-by":"crossref","DOI":"10.4204\/EPTCS.338.7","article-title":"A Logic Theory Pattern for Linearized Control Systems","volume-title":"The 6th Workshop on Formal Integrated Development Environment (F-IDE 2021) \u2013 Affiliated to NASA Formal Methods 2021, Virtual event, Electronic Proceedings in Theoretical Computer Science (EPTCS)","author":"Domenici","year":"2021"},{"key":"2023022013494759700_","doi-asserted-by":"crossref","first-page":"300","DOI":"10.1007\/978-3-319-74781-1_21","article-title":"Integrated Simulation and Formal Verification of a Simple Autonomous Vehicle","volume-title":"Software Engineering and Formal Methods (SEFM 2017), volume 10729 of LNCS","author":"Domenici","year":"2018"},{"key":"2023022013494759700_","doi-asserted-by":"crossref","first-page":"1465","DOI":"10.1109\/TAC.2004.834433","article-title":"Information flow and cooperative control of vehicle formations","volume":"49","author":"Fax","year":"2004","journal-title":"IEEE Trans. Automat. Contr."},{"key":"2023022013494759700_","first-page":"1","volume-title":"Vienna Development Method","author":"Fitzgerald","year":"2007"},{"key":"2023022013494759700_","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1109\/MCS.2016.2643244","article-title":"High-assurance SPIRAL: end-to-end guarantees for robot and car control","volume":"37","author":"Franchetti","year":"2017","journal-title":"IEEE Contr. Syst."},{"key":"2023022013494759700_","doi-asserted-by":"crossref","first-page":"5640","DOI":"10.1109\/ACC.2012.6314944","article-title":"Fuzzy Opinion Dynamics","volume-title":"The 2012 American Control Conference (ACC)","author":"Gasparri","year":"2012"},{"key":"2023022013494759700_","first-page":"81","article-title":"Stable Adaptive Co-simulation: A Switched Systems Approach","volume-title":"IUTAM Symposium on Co-Simulation and Solver Coupling, number 35 in IUTAM Bookseries","author":"Gomes","year":"2017"},{"key":"2023022013494759700_","first-page":"49:1","article-title":"Co-simulation: a survey","volume":"51","author":"Gomes","year":"2018","journal-title":"ACM Comput. Surv"},{"key":"2023022013494759700_","doi-asserted-by":"crossref","first-page":"278","DOI":"10.1109\/LICS.1996.561342","article-title":"The Theory of Hybrid Automata","volume-title":"Proc. of the 11th Annual IEEE Symposium on Logic in Computer Science","author":"Henzinger","year":"1996"},{"key":"2023022013494759700_","doi-asserted-by":"crossref","DOI":"10.1049\/PBPC007E","volume-title":"SysML for Systems Engineering","author":"Holt","year":"2008"},{"key":"2023022013494759700_","doi-asserted-by":"crossref","first-page":"988","DOI":"10.1109\/TAC.2003.812781","article-title":"Coordination of groups of mobile autonomous agents using nearest neighbor rules","volume":"48","author":"Jadbabaie","year":"2003","journal-title":"IEEE Trans. Automat. Control"},{"key":"2023022013494759700_","doi-asserted-by":"crossref","first-page":"1268","DOI":"10.1177\/0037549714553151","article-title":"Simulation integration: Using multidatabase systems concepts","volume":"90","author":"Jalali","year":"2014","journal-title":"Simulation"},{"key":"2023022013494759700_","doi-asserted-by":"crossref","first-page":"3575","DOI":"10.1109\/TIT.2012.2191450","article-title":"Distributed parameter estimation in sensor networks: nonlinear observation models and imperfect communication","volume":"58","author":"Kar","year":"2012","journal-title":"IEEE Trans. Inf. Theory"},{"key":"2023022013494759700_","first-page":"2149","article-title":"Design and Use Paradigms for Gazebo, An Open-Source Multi-robot Simulator","volume-title":"The 2004 IEEE\/RSJ Int. Conf. on Intelligent Robots and Systems (IROS)","author":"Koenig","year":"2004"},{"key":"2023022013494759700_","first-page":"1","article-title":"Integrated Tool Chain for Model-Based Design of Cyber-Physical Systems: The INTO-CPS Project","volume-title":"The 2nd Int. Workshop on Modelling, Analysis, and Control of Complex CPS (CPS Data)","author":"Larsen","year":"2016"},{"key":"2023022013494759700_","first-page":"97","article-title":"Support for Co-modelling and Co-simulation: The Crescendo Tool","author":"Larsen","year":"2014"},{"key":"2023022013494759700_","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1093\/oso\/9780198537465.003.0004","article-title":"Higher order logic","volume-title":"Handbook of Logic in Artificial Intelligence and Logic Programming","author":"Leivant","year":"1994"},{"key":"2023022013494759700_","doi-asserted-by":"crossref","first-page":"20","DOI":"10.1109\/MRA.2012.2206474","article-title":"Multirotor aerial vehicles: Modeling, estimation, and control of quadrotor","volume":"19","author":"Mahony","year":"2012","journal-title":"IEEE Robot. Autom. Mag."},{"key":"2023022013494759700_","volume-title":"The Temporal Logic of Reactive Systems: Safety","author":"Manna","year":"1995"},{"key":"2023022013494759700_","first-page":"81","article-title":"Verification of Interactive Software for Medical Devices: PCA Infusion Pumps and FDA Regulation as an Example","volume-title":"The EICS2013, 5th ACM SIGCHI Symposium on Engineering Interactive Computing Systems","author":"Masci","year":"2013"},{"key":"2023022013494759700_","article-title":"DAIDALUS: Detect and Avoid Alerting Logic for Unmanned Systems","volume-title":"Proc. of the 34th Digital Avionics Systems Conf. (DASC 2015)","author":"Mu\u00f1oz","year":"2015"},{"key":"2023022013494759700_","first-page":"93","article-title":"The Minerva Software Development Process","volume-title":"Automated Formal Methods","author":"Narkawicz","year":"2018"},{"key":"2023022013494759700_","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1007\/s10817-017-9415-7","article-title":"Translation of IEC 61131-3 function block diagrams to PVS for formal verification with real-time nuclear application","volume":"60","author":"Newell","year":"2018","journal-title":"J. Autom. Reason."},{"key":"2023022013494759700_","article-title":"Rapid prototyping in PVS","author":"NIA 2003\u201303, NASA\/CR-2003-212418","year":"2003"},{"key":"2023022013494759700_","first-page":"1","article-title":"PVSio-web: a tool for rapid prototyping device user interfaces in PVS","volume":"69","author":"Oladimeji","year":"2013","journal-title":"Electron. Commun. EASST"},{"key":"2023022013494759700_","doi-asserted-by":"crossref","first-page":"215","DOI":"10.1109\/JPROC.2006.887293","article-title":"Consensus and Cooperation in Networked Multi-agent Systems","volume":"95","author":"Olfati-Saber","year":"2007","journal-title":"Proc. of the IEEE"},{"key":"2023022013494759700_","first-page":"411","article-title":"PVS: Combining Specification, Proof Checking, and Model Checking","volume-title":"Computer-Aided Verification, CAV \u201896, number 1102 in LNCS","author":"Owre","year":"1996"},{"key":"2023022013494759700_","doi-asserted-by":"crossref","first-page":"423","DOI":"10.1007\/978-3-319-74781-1_29","article-title":"Co-simulation of semi-autonomous systems: the Line Follower Robot case study","volume-title":"Software Engineering and Formal Methods (SEFM 2017)","author":"Palmieri","year":"2018"},{"key":"2023022013494759700_","doi-asserted-by":"crossref","first-page":"601","DOI":"10.1007\/s10270-019-00754-9","article-title":"A framework for FMI-based co-simulation of human\u2013machine interfaces","volume":"19","author":"Palmieri","year":"2020","journal-title":"Softw. Syst. Model."},{"key":"2023022013494759700_","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1007\/978-3-540-71070-7_15","article-title":"KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description)","volume-title":"Automated Reasoning","author":"Platzer","year":"2008"},{"key":"2023022013494759700_","doi-asserted-by":"crossref","first-page":"232","DOI":"10.1109\/JPROC.2004.840306","article-title":"SPIRAL: code generation for DSP transforms","volume":"93","author":"P\u00fcschel","year":"2005","journal-title":"Proc. of the IEEE"},{"key":"2023022013494759700_","first-page":"1859","article-title":"A Survey of Consensus Problems in Multi-agent Coordination","volume-title":"Proc. of the 2005 American Control Conf.","author":"Wei","year":"2005"},{"key":"2023022013494759700_","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1109\/TCAD.2003.819898","article-title":"System modeling and transformational design refinement in ForSyDe","volume":"23","author":"Sander","year":"2004","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"key":"2023022013494759700_","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1109\/MS.2003.1231146","article-title":"The pragmatics of model-driven development","volume":"20","author":"Selic","year":"2003","journal-title":"IEEE Software"},{"key":"2023022013494759700_","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1142\/S2301385020500090","article-title":"Multiple UAV systems: a survey","volume":"8","author":"Skorobogatov","year":"2020","journal-title":"Unmanned Systems"},{"key":"2023022013494759700_","volume-title":"First-Order Logic","author":"Smullyan","year":"1995"},{"key":"2023022013494759700_","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1109\/DS-RT.2013.12","article-title":"HybridSim: A Modeling and Co-simulation Toolchain for Cyber-Physical Systems","volume-title":"The 2013 IEEE\/ACM 17th Int. Symposium on Distributed Simulation and Real Time Applications (DS-RT)","author":"Wang","year":"2013"}],"container-title":["The Computer Journal"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/academic.oup.com\/comjnl\/article-pdf\/66\/2\/295\/49256600\/bxab161.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/academic.oup.com\/comjnl\/article-pdf\/66\/2\/295\/49256600\/bxab161.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,11,9]],"date-time":"2023-11-09T19:34:24Z","timestamp":1699558464000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/comjnl\/article\/66\/2\/295\/6408792"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,10,23]]},"references-count":52,"journal-issue":{"issue":"2","published-online":{"date-parts":[[2021,10,23]]},"published-print":{"date-parts":[[2023,2,19]]}},"URL":"https:\/\/doi.org\/10.1093\/comjnl\/bxab161","relation":{},"ISSN":["0010-4620","1460-2067"],"issn-type":[{"value":"0010-4620","type":"print"},{"value":"1460-2067","type":"electronic"}],"subject":[],"published-other":{"date-parts":[[2023,2]]},"published":{"date-parts":[[2021,10,23]]}}}