Towards a framework for certification of reliable autonomous systems Autonomous Agents and Multi-Agent Systems

Wpt Global Franch

Authors: MichaelFisher, VivianaMascardi, Kristin YvonneRozier, Bernd-HolgerSchlingloff, MichaelWinikoff, NeilYorke-SmithAuthors Info & Claims Autonomous Agents and Multi-Agent Systems, Volume 35, Issue 1https://doi.org/10.1007/s10458-020-09487-2 Published: 01 April 2021Publication History 10citation0DownloadsMetricsTotal Citations10Total Downloads0Last 12 Months0Last 6 weeks0Get Citation Alerts

New Citation Alert added!

This alert has been successfully added and will be sent to:

You will be notified whenever a record that you have chosen has been cited.

To manage your alert preferences, click on the button below.

Manage my Alerts

New Citation Alert!

Please log in to your account

A computational system is called autonomous if it is able to make its own decisions, or take its own actions, without human supervision or control. The capability and spread of such systems have reached the point where they are beginning to touch much of everyday life. However, regulators grapple with how to deal with autonomous systems, for example how could we certify an Unmanned Aerial System for autonomous use in civilian airspace? We here analyse what is needed in order to provide verified reliable behaviour of an autonomous system, analyse what can be done as the state-of-the-art in automated verification, and propose a roadmap towards developing regulatory guidelines, including articulating challenges to researchers, to engineers, and to regulators. Case studies in seven distinct domains illustrate the article. 124me Company. 24me Smart Personal Assistant. URL https://www.twentyfour.me/.Google Scholar2Abate, A., Katoen, J.-P., & Mereacre, A. (2011). Quantitative automata model checking of autonomous stochastic hybrid systems. In Proceedings of the 14th ACM International Conference on Hybrid Systems: Computation and Control (HSCC) (pp. 83–92). ACM.Google Scholar3Adolf, F.-M., Faymonville, P., Finkbeiner, B., Schirmer, S., & Torens, C. (2017). Stream runtime monitoring on UAS. In Proceedings of International Conference on Runtime Verification (pp. 33–49).Google Scholar4Alexander, R., Hall-May, M., & Kelly, T. (2007). Certification of autonomous systems. In Proceedings of 2nd Systems Engineering for Autonomous Systems (SEAS) Defence Technology Centre (DTC) Annual Technical Conference.Google Scholar5Alur R, Henzinger TA, Lafferriere G, and Pappas GJ Discrete abstractions of hybrid systems Proceedings of the IEEE 2000 88 7 971-984CrossrefGoogle Scholar6Alves GV, Dennis L, Fernandes L, and Fisher M Leitner A, Watzenig D, and Ibanez-Guzman J Reliable Decision-Making in Autonomous Vehicles Validation and verification of automated systems: Results of the ENABLE-S3 Project 2020 Cham Springer, New york 105-117CrossrefGoogle Scholar7Amirabdollahian, F., Dautenhahn, K., Dixon, C., Eder, K., Fisher, M., Koay, K. L., Magid, E., Pipe, A., Salem, M., Saunders, J., & Webster, M. (2013). Can You Trust Your Robotic Assistant? In International Conference on Social Robotics, volume 8239 of LNCS (pp. 571–573). Springer.Google Scholar8Ancona, D., Ferrando, A., & Mascardi, V. (2016). Comparing trace expressions and Linear Temporal Logic for runtime verification. In Theory and Practice of Formal Methods, (pp. 47–64). Springer, New yorkGoogle Scholar9Ancona D, Ferrando A, and Mascardi V Parametric runtime verification of multiagent systems AAMAS 2017 17 1457-1459Google Scholar10Anderson, M., & Anderson, S. L. (2008). EthEl: Toward a principled ethical eldercare robot. In Proc. AAAI Fall Symposium on AI in Eldercare: New Solutions to Old Problems.Google Scholar11Anderson, M., & Anderson, S. L. (2011). Machine Ethics. : Cambridge University Press.Google Scholar12Appel, K., & Haken, W. (1989). Every Planar Map is Four-Colorable, volume 98 of Contemporary Mathematics. Providence, RI: American Mathematical Society. ISBN 0-8218-5103-9.CrossrefGoogle Scholar13Arcaini, P., Bonfanti, S., Gargantini, A., Mashkoor, A., & Riccobene, E. (2015). Formal validation and verification of a medical software critical component. In 13th ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2015, Austin, TX, USA, September 21-23, 2015 (pp. 80–89). IEEE.CrossrefGoogle Scholar14Areias, C., Cunha, J. C., Iacono, D., & Rossi, F. (2014). Towards certification of automotive software. In Proceedings of 25th IEEE International Symposium on Software Reliability Engineering Workshops ISSRE (pp. 491–496).CrossrefGoogle Scholar15Arkin, R. C. (2008). Governing lethal behavior: embedding ethics in a hybrid deliberative/reactive robot architecture. In Proceedings of 3rd ACM/IEEE international conference on Human Robot Interaction (HRI’08) (pp. 121–128).CrossrefGoogle Scholar16AV-TEST Institute. (2019). Robot vacuums undergo a security check: trustworthy helpers around the house or chatty cleaning appliances? URL https://www.av-test.org/en/news/robot-vacuums-undergo-a-security-check-trustworthy-helpers-around-the-house-or-chatty-cleaning-appli/. Archived from the original URL at: https://web.archive.org/web/20200613234231/https://www.av-test.org/en/news/robot-vacuums-undergo-a-security-check-trustworthy-helpers-around-the-house-or-chatty-cleaning-appli/.Google Scholar17Baier, C., & Katoen, J.-P. (2008). Principles of Model Checking. MIT Press. ISBN 026202649X.Google Scholar18Bao W, Yue J, and Rao Y A deep learning framework for financial time series using stacked autoencoders and long-short term memory PLOS One 2017 12 7 e0180944CrossrefGoogle Scholar19Bartocci E, Bortolussi L, Brázdil T, Milios D, and Sanguinetti G Policy learning in continuous-time markov decision processes using gaussian processes Perform. Eval. 2017 116 84-100CrossrefGoogle Scholar20Basin, D. A., Klaedtke, F., Müller, S., & Pfitzmann, B. (2008). Runtime monitoring of metric first-order temporal properties. In Proceedings of 28th IARCS Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS’08) (pp. 49–60).CrossrefGoogle Scholar21Bauer, B., Müller, J. P., & Odell, J. (2000). Agent UML: A formalism for specifying multiagent software systems. In P. Ciancarini, & M. J. Wooldridge (Eds.), Agent-Oriented Software Engineering, First International Workshop, AOSE 2000, Limerick, Ireland, June 10, 2000, Revised Papers, volume 1957 of Lecture Notes in Computer Science (pp. 91–104). Springer.CrossrefGoogle Scholar22Beck K Test-driven development: by example 2003 Boston Addison-Wesley ProfessionalGoogle Scholar23Beedle, M., van Bennekum, A., Cockburn, A., Cunningham, W., Fowler, M., Highsmith, J., Hunt, A., Jeffries, R., Kern, J., Marick, B., Martin, R. C., Schwaber, K., Sutherland, J., & Thomas, D. (2001). Manifesto for agile software development. URL http://agilemanifesto.org/.Google Scholar24Bensalem, S., Ganesh, V., Lakhnech, Y., Munoz, C., Owre, S., Rueß, H., Rushby, J., Rusu, V., Saıdi, H., Shankar, N., et al. (2000). An overview of SAL. In Proceedings of 5th NASA Langley Formal Methods Workshop. Williamsburg, VA.Google Scholar25Bentzen, M., Lindner, F., Dennis, L., & Fisher, M. (2018). Moral Permissibility of Actions in Smart Home Systems. In Proceedings of FLoC 2018 Workshop on Robots, Morality, and Trust through the Verification Lens.Google Scholar26Benzel, T. (1984). Analysis of a kernel verification. In Proceedings of 1984 IEEE Symposium on Security and Privacy (pp. 125–133).CrossrefGoogle Scholar27Bergenhem, C., Huang, Q., Benmimoun, A., & Robinson, T. (2010). Challenges of platooning on public motorways. In Proceedings of 17th World Congress on Intelligent Transport Systems (pp. 1–12).Google Scholar28Berry PM, Gervasio MT, Peintner B, and Yorke-Smith N PTIME: personalized assistance for calendaring ACM Trans. Intelligent Systems and Technology 2011 2 4 40:1-40:22CrossrefGoogle Scholar29Bertolino, A. (2007). Software testing research: Achievements, challenges, dreams. In L. C. Briand, & A. L. Wolf (Eds.), International Conference on Software Engineering, ISCE 2007, Workshop on the Future of Software Engineering, FOSE 2007, May 23-25, 2007, Minneapolis, MN, USA (pp. 85–103). IEEE Computer Society.CrossrefGoogle Scholar30Biere, A., Heljanko, K., & Wieringa, S. (2011). AIGER 1.9 and beyond. Available at fmv.jku.at/hwmcc11/beyond1.pdf.Google Scholar31Birnbacher D and Birnbacher W Fully autonomous driving: Where technology and ethics meet IEEE Intelligent Systems 2017 32 5 3-4CrossrefGoogle Scholar32Bloomfield R and Bishop P Dale C and Anderson T Safety and assurance cases: Past, present and possible future - an adelard perspective Making systems safer 2010 London, UK Springer 51-67CrossrefGoogle Scholar33Booch G, Rumbaugh J, and Jacobson I The unified modeling language user guide 1999 Redwood City, CA, USA Addison Wesley Longman Publishing Co. Inc. ISBN 0-201-57168-4Google Scholar34Bordini, R. H., Fisher, M., Pardavila, C., & Wooldridge, M. J. (2003). Model checking AgentSpeak. In The Second International Joint Conference on Autonomous Agents & Multiagent Systems, AAMAS 2003, July 14-18, 2003, Melbourne, Victoria, Australia, Proceedings (pp. 409–416). ACM.CrossrefGoogle Scholar35Bordini RH, Fisher M, Visser W, and Wooldridge MJ Model checking rational agents IEEE Intelligent Systems 2004 19 5 46-52CrossrefGoogle Scholar36Bordini RH, Fisher M, Visser W, and Wooldridge MJ Verifying multi-agent programs by model checking Autonomous Agents and Multi-Agent Systems 2006 12 2 239-256CrossrefGoogle Scholar37Bozzano, M., Cimatti, A., Pires, A. F., Jones, D., Kimberly, G., Petri, T., Robinson, R., Tonetta, S. (2015). Formal design and safety analysis of air6110 wheel brake system. In International Conference on Computer Aided Verification (pp. 518–535). Springer.Google Scholar38Brat, G., & Venet, A. (2005). Precise and scalable static program analysis of NASA flight software. In 2005 IEEE Aerospace Conference, (pp. 1–10). IEEE.Google Scholar39Brat, G., Navas, J. A., Shi, N., & Venet, A. (2014). IKOS: A framework for static analysis based on abstract interpretation. In International Conference on Software Engineering and Formal Methods (pp. 271–277). Springer.Google Scholar40Bremner P, Dennis LA, Fisher M, and Winfield AFT On Proactive, transparent, and verifiable ethical reasoning for robots Proceedings of the IEEE 2019 107 3 541-561CrossrefGoogle Scholar41Bringsjord S, Arkoudas K, and Bello P Toward a general logicist methodology for engineering ethically correct robots IEEE Intelligent Systems 2006 21 4 38-44CrossrefGoogle Scholar42British Standards Institution. BSI web site. URL https://www.bsigroup.com/.Google Scholar43British Standards Institution (BSI) (2016). BS 8611 – robots and robotic devices — guide to the ethical design and application. URL https://shop.bsigroup.com/ProductDetail/?pid=000000000030320089.Google Scholar44Brooks RA A robust layered control system for a mobile robot IEEE J. Robotics Autom. 1986 2 1 14-23CrossrefGoogle Scholar45Butler, R. (1996). An introduction to requirements capture using PVS: specification of a simple autopilot. Technical report, NASA Langley Technical Report Server.Google Scholar46Butler RW and Finelli GB The infeasibility of quantifying the reliability of life-critical real-time software IEEE Transactions on Software Engineering 1993 19 1 3-12CrossrefGoogle Scholar47Cambridge Academic Content Dictionary (2020). Definition of ‘certification’. URL https://dictionary.cambridge.org/dictionary/english/certification.Google Scholar48Cambridge English Dictionary (2020). Definition of ‘autopilot’. URL https://dictionary.cambridge.org/dictionary/english/autopilot.Google Scholar49Cambridge English Dictionary (2020). Definition of ‘regulation’. URL https://dictionary.cambridge.org/dictionary/english/regulation.Google Scholar50Cauwels, M., Hammer, A., Hertz, B., Jones, P., & Rozier, K. Y. (September 2020). Integrating runtime verification into an automated uas traffic management system. In Proceedings of DETECT: international workshop on moDeling, vErification and Testing of dEpendable CriTical systems, Communications in Computer and Information Science (CCIS), page TBD, L’Aquila, Italy. Springer.Google Scholar51CENELEC (2011). CENELEC - EN 50128 – railway applications - communication, signalling and processing systems - software for railway control and protection systems. URL https://standards.globalspec.com/std/1678027/EN%2050128Google Scholar52Chapman D Planning for conjunctive goals Artif. Intell. 1987 32 3 333-377CrossrefGoogle Scholar53Charisi, V., Dennis, L., Fisher, M., Lieck, R., Matthias, A., Slavkovik, M., Sombetzki, J., Winfield, A. F. T., & Yampolskiy, R. (Mar. 2017). Towards moral autonomous systems. ArXiv e-prints.Google Scholar54Cimatti, A., Gario, M., & Tonetta, S. (2016). A lazy approach to temporal epistemic logic model checking. In Proceedings of the 2016 International Conference on Autonomous Agents & Multiagent Systems (pp. 1218–1226).Google Scholar55Clarke EM and Schlingloff B-H Robinson A and Voronkov A Model Checking Handbook of Automated Reasoning 2001 Amesterdam Elsevier 1635-1790CrossrefGoogle Scholar56Clarke EM, Grumberg O, and Peled DA Model Checking 2000 London The MIT Press ISBN 0262032708Google Scholar57Cobleigh, J. M., Giannakopoulou, D., & Păsăreanu, C. S. (2003). Learning assumptions for compositional verification. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems (pp. 331–346). Springer, NewyorkGoogle Scholar58Cofer DD, Hatcliff J, Huhn M, and Lawford M Software certification: Methods and tools (Dagstuhl seminar 13051) Dagstuhl Reports 2013 3 1 111-148CrossrefGoogle Scholar59Cousot, P., Cousot, R., Feret, J., Miné, A., Rival, X., Blanchet, B., Monniaux, D., & Mauborgne, L. Astrée. URL http://www.astree.ens.fr/.Google Scholar60Currit PA, Dyer MG, and Mills HD Certifying the reliability of software IEEE Trans. Software Eng. 1986 12 1 3-11CrossrefGoogle Scholar61de Araújo, R. P., Mota, A. C., & Nogueira, S. d. C. (Aug 2017). Probabilistic analysis applied to cleaning robots. In 2017 IEEE International Conference on Information Reuse and Integration (IRI) (pp. 275–282).CrossrefGoogle Scholar62Dalpiaz F, Ferrari A, Franch X, and Palomares C Natural language processing for requirements engineering: The best is yet to come IEEE Software 2018 35 5 115-119CrossrefGoogle Scholar63Dastani M, Torroni P, and Yorke-Smith N Monitoring norms: A multi-disciplinary perspective Knowledge Eng. Review 2018 33 e25CrossrefGoogle Scholar64Dennett DC The Intentional Stance 1989 Cambridge, MA, USA MIT PressGoogle Scholar65Denney E and Pai G Tool support for assurance case development Autom. Softw. Eng. 2018 25 3 435-499CrossrefGoogle Scholar66Dennis, L. A. (2018). The MCAPL Framework including the Agent Infrastructure Layer and Agent Java Pathfinder. The Journal of Open Source Software, 3(24)Google Scholar67Dennis LA and Fisher M Verifiable self-aware agent-based autonomous systems Proceedings of the IEEE 2020 108 7 1011-1026CrossrefGoogle Scholar68Dennis LA, Fisher M, Webster M, and Bordini RH Model checking agent programming languages Automated Software Engineering 2012 19 1 5-63CrossrefGoogle Scholar69Dennis LA, Fisher M, Lincoln NK, Lisitsa A, and Veres SM Practical verification of decision-making in agent-based autonomous systems Automated Software Engineering 2016 23 3 305-359 ISSN 0928-8910CrossrefGoogle Scholar70Dennis LA, Fisher M, Slavkovik M, and Webster M Formal verification of ethical choices in autonomous systems Robotics and Autonomous Systems 2016 77 1-14CrossrefGoogle Scholar71Dixon, C., Webster, M., Saunders, J., Fisher, M., & Dautenhahn, K. (2014). The Fridge Door is Open — Temporal Verification of a Robotic Assistant’s Behaviours. In Advances in Autonomous Robotics Systems (TAROS),volume Lecture Notes in Computer Science (pp. 97–108). Springer. NewyorkGoogle Scholar72Dutilleul, S. C., Lecomte, T., & Romanovsky, A. B. (Eds.) (2019). Proceedings of 3rd International Conference on Reliability, Safety, and Security of Railway Systems (RSSRail’19), volume 11495 of Lecture Notes in Computer Science. Springer. ISBN 978-3-030-18743-9.CrossrefGoogle Scholar73Dutt ND, Regazzoni CS, Rinner B, and Yao X Self-awareness for autonomous systems Proceedings of the IEEE 2020 108 7 971-975CrossrefGoogle Scholar74Economic, U. N., & Council, S. (1968). Vienna Convention on Road Traffic. http://www.unece.org/trans/conventn/crt1968e.pdf.Google Scholar75Edelkamp S, Leue S, and Lluch-Lafuente A Directed explicit-state model checking in the validation of communication protocols International Journal on Software Tools For Technology Transfer 2004 5 2–3 247-267CrossrefGoogle Scholar76Emerson, E. A. (1990). Temporal and modal logic. In Formal Models and Semantics (pp. 995–1072). Elsevier, NewyorkGoogle Scholar77Espejo-García B, Martínez-Guanter J, Pérez-Ruiz M, López-Pellicer FJ, and Zarazaga-Soria FJ Machine learning for automatic rule classification of agricultural regulations: A case study in Spain Computers and Electronics in Agriculture 2018 150 343-352CrossrefGoogle Scholar78European Aviation Artificial Intelligence High Level Group (2020). The FLY AI report – demystifying and accelerating AI in aviation/ATM. URL https://www.eurocontrol.int/publication/fly-ai-report.Google Scholar79European Committee for Electrotechnical Standardisation. CENELEC web site. URL https://www.cenelec.eu/.Google Scholar80European Parliament (2016). Regulation (eu) 2016/679 of the european parliament and of the council of 27 april 2016 on the protection of natural persons with regard to the processing of personal data and on the free movement of such data, and repealing directive 95/46/ec (general data protection regulation). URL https://eur-lex.europa.eu/legal-content/EN/TXT/?uri=CELEX:32016R0679.Google Scholar81European Union Aviation Safety Agency. EASA web site. URL https://www.easa.europa.eu/.Google Scholar82FAA (November 2010). Qantas flight 32, airbus a380-842, vh-oqa. Online: https://lessonslearned.faa.gov/ll_main.cfm?TabID=1&LLID=83.Google Scholar83Falcone, Y., Krstic, S., Reger, G., & Traytel, D. (2018). A taxonomy for classifying runtime verification tools. In C. Colombo, & M. Leucker (Eds.), Runtime Verification - 18th International Conference, RV 2018, Limassol, Cyprus, November 10-13, 2018, Proceedings, volume 11237 of Lecture Notes in Computer Science (pp. 241–262). Springer.CrossrefGoogle Scholar84Farrell, M., Luckcuck, M., & Fisher, M. (2018). Robotics and Integrated Formal Methods: Necessity Meets Opportunity. In Proceedings of 14th International Conference on Integrated Formal Methods (IFM’18), volume LNCS 11023 (pp. 161–171). Springer.CrossrefGoogle Scholar85Federal Aviation Administration. FAA web site. URL https://www.faa.gov/.Google Scholar86Federal Aviation Administration (2004). Title 14 code of Federal Regulations Part 145 approved training program – research and recommendations. URL https://www.faa.gov/about/initiatives/maintenance_hf/library/documents/media/human_factors_maintenance/ar04-36.pdf.Google Scholar87Federal Aviation Administration (2016). Part 107: Operation and certification of small unmanned aircraft systems. URL https://www.faa.gov/uas/media/RIN_2120-AJ60_Clean_Signed.pdf.Google Scholar88Ferrando, A., Ancona, D., & Mascardi, V. (2017). Decentralizing MAS monitoring with DecAMon. In AAMAS (pp. 239–248). ACM.Google Scholar89Ferrando, A., Dennis, L. A., Ancona, D., Fisher, M., & Mascardi, V. (2018). Recognising Assumption Violations in Autonomous Systems Verification. In AAMAS (pp. 1933–1935). International Foundation for Autonomous Agents and Multiagent Systems Richland, SC, USA / ACM.Google Scholar90Ferrando, A., Dennis, L. A., Ancona, D., Fisher, M., & Mascardi, V. (2018). Verifying and Validating Autonomous Systems: Towards an Integrated Approach. In RV, volume 11237 of Lecture Notes in Computer Science (pp. 263–281). Springer.Google Scholar91FINRA. Algorithmic trading: Rules. https://www.finra.org/rules-guidance/key-topics/algorithmic-trading#rules. Accessed 2019-10-15.Google Scholar92Fisher M, Dennis LA, and Webster MP Verifying autonomous systems Communications of the ACM 2013 56 9 84-93CrossrefGoogle Scholar93Franchetti F, Low TM, Mitsch S, Mendoza JP, Gui L, Phaosawasdi A, Padua D, Kar S, Moura JM, Franusich M, et al. High-assurance spiral: End-to-end guarantees for robot and car control IEEE Control Systems Magazine 2017 37 2 82-103CrossrefGoogle Scholar94Frauenberger C and Purgathofer P Ways of thinking in informatics Communications of the ACM 2019 62 7 58-64CrossrefGoogle Scholar95FreeBSD. lint – a c program verifier. URL https://www.freebsd.org/cgi/man.cgi?query=lint&apropos=0&sektion=0&manpath=FreeBSD+11.1-RELEASE&arch=default&format=html.Google Scholar96Fulton, N., Ji, R., Platzer, A., et al. (2016). Proving autonomous vehicle and advanced driver assistance systems safety: final research report.Google Scholar97Galdino, A. L., Munoz, C., & Ayala-Rincón, M. (2007). Formal verification of an optimal air traffic conflict resolution and recovery algorithm. In International Workshop on Logic, Language, Information, and Computation (pp. 177–188). Springer, Berline, Heidelberg.Google Scholar98Gario, M., Cimatti, A., Mattarei, C., Tonetta, S., & Rozier, K. Y. (July 2016). Model checking at scale: Automated air traffic control design space exploration. In Proceedings of 28th International Conference on Computer Aided Verification (CAV 2016), volume 9780 of LNCS (pp. 3–22) Toronto, ON, Canada. Springer.CrossrefGoogle Scholar99Geist, J., Rozier, K. Y., & Schumann, J. (September 2014). Runtime observer pairs and bayesian network reasoners On-board FPGAs: Flight-certifiable system health management for embedded systems. In Proceedings of the 14th International Conference on Runtime Verification (RV14), volume 8734 (pp. 215–230). Springer-Verlag.Google Scholar100Ghosh, S., Elenius, D., Li, W., Lincoln, P., Shankar, N., & Steiner, W. (2016). ARSENAL: automatic requirements specification extraction from natural language. In S. Rayadurgam, & O. Tkachuk (eds.), NASA Formal Methods - 8th International Symposium, NFM 2016, Minneapolis, MN, USA, June 7-9, 2016, Proceedings, volume 9690 of Lecture Notes in Computer Science (pp. 41–46). Springer.CrossrefGoogle Scholar101Gunkel D and Bryson JJ Introduction to the special issue on machine morality: The machine as moral agent and patient Philosophy & Technology 2014 27 1 5-8CrossrefGoogle Scholar102Havelund, K., & Reger, G. (2017). Runtime verification logics a language design perspective. In Models, Algorithms, Logics and Tools - Essays Dedicated to Kim Guldstrand Larsen on the Occasion of His 60th Birthday, volume 10460 of Lecture Notes in Computer Science (pp. 310–338). Springer, New yorkGoogle Scholar103Heitmeyer CL On the role of formal methods in software certification: An experience report Electronic Notes on Theoretical Computer Science 2009 238 4 3-9CrossrefGoogle Scholar104Heitmeyer CL, Archer M, Leonard EI, and McLean J Applying formal methods to a certifiably secure software system IEEE Trans. Software Eng. 2008 34 1 82-98CrossrefGoogle Scholar105Helle, P., Schamai, W., & Strobel, C. (2016). Testing of autonomous systems – challenges and current state-of-the-art. In INCOSE International Symposium, volume 26-1 (pp. 571–584). Wiley Online Library.CrossrefGoogle Scholar106Henzinger TA, Ho P-H, and Wong-Toi H HYTECH: A model checker for hybrid systems International Journal on Software Tools for Technology Transfer 1997 1 1–2 110-122CrossrefGoogle Scholar107Hoare CAR An axiomatic basis for computer programming Commun. ACM 1969 12 10 576-580 ISSN 0001-0782CrossrefGoogle Scholar108Hodgkins, K. (5 Oct. 2011). Apple’s Knowledge Navigator, Siri and the iPhone 4S. Engadget.Google Scholar109Holzmann GJ The Spin Model Checker: Primer and Reference Manual 2003 Boston Addison-Wesley ISBN 0-321-22862-6Google Scholar110Huhns MN and Singh MP Agents on the web: Personal assistants IEEE Internet Computing 1998 2 5 90-92CrossrefGoogle Scholar111Industry Research (2019). Software testing services market by product, end-users, and geography – global forecast and analysis 2019-2023. URL https://www.industryresearch.co/software-testing-services-market-by-product-end-users-and-geography-global-forecast-and-analysis-2019-2023-14620379.Google Scholar112Institute of Electrical and Electronics Engineers. The IEEE global initiative on ethics of autonomous and intelligent systems, a. URL https://standards.ieee.org/industry-connections/ec/autonomous-systems.html.Google Scholar113Institute of Electrical and Electronics Engineers. IEEE web site, b. URL https://www.ieee.org/.Google Scholar114Institute of Electrical and Electronics Engineers (2006). IEEE 1512-2006 – standard for common incident management message sets for use by emergency management centers. URL https://standards.ieee.org/standard/1512-2006.html.Google Scholar115Institute of Electrical and Electronics Engineers (2015). IEEE standard ontologies for robotics and automation. URL https://ieeexplore.ieee.org/document/7084073.Google Scholar116Institute of Electrical and Electronics Engineers (2016). P2020 – standard for automotive system image quality. URL https://standards.ieee.org/project/2020.html.Google Scholar117Institute of Electrical and Electronics Engineers (2016). P7000 – model process for addressing ethical concerns during system design. URL https://standards.ieee.org/project/7000.html.Google Scholar118Institute of Electrical and Electronics Engineers (2016c). P7001 – transparency of autonomous systems. URL https://standards.ieee.org/project/7001.html.Google Scholar119Institute of Electrical and Electronics Engineers (2016d). P7002 – data privacy process. URL https://standards.ieee.org/project/7002.html.Google Scholar120Institute of Electrical and Electronics Engineers (2017). P7003 – algorithmic bias considerations. URL https://standards.ieee.org/project/7003.html.Google Scholar121Institute of Electrical and Electronics Engineers (2017). P7006 – standard for personal data artificial intelligence (AI) agent. URL https://standards.ieee.org/project/7006.html.Google Scholar122Institute of Electrical and Electronics Engineers (2017c). P7007 – ontological standard for ethically driven robotics and automation systems. URL https://standards.ieee.org/project/7007.html.Google Scholar123Institute of Electrical and Electronics Engineers (2017d). P7008 – standard for ethically driven nudging for robotic, intelligent and autonomous systems. URL https://standards.ieee.org/project/7008.html.Google Scholar124Institute of Electrical and Electronics Engineers (2017e). P7009 – standard for fail-safe design of autonomous and semi-autonomous systems. URL https://standards.ieee.org/project/7009.html.Google Scholar125Institute of Electrical and Electronics Engineers – Robotics and Automation Society (2019). IEEE-RAS technical committee for verification of autonomous systems. URL https://www.ieee-ras.org/verification-of-autonomous-systems.Google Scholar126International Association of Public Transport – L’Union internationale des transports publics. UITP web site. URL https://www.uitp.org/.Google Scholar127International Civil Aviation Organization (2001). Annex 11 to the convention on international civil aviation, thirteenth edition. URL https://store.icao.int/products/annex-11-air-traffic-services.Google Scholar128International Electrotechnical Commission. IEC TC 107 – process management for avionics, a. URL https://www.iec.ch/dyn/www/f?p=103:7:0::::FSP_ORG_ID:1304.Google Scholar129International Electrotechnical Commission. IEC TC 97 – electrical installations for lighting and beaconing of aerodromes, b. URL https://www.iec.ch/dyn/www/f?p=103:7:0::::FSP_ORG_ID:1294.Google Scholar130International Electrotechnical Commission. IEC web site, c. URL https://www.iec.ch/.Google Scholar131International Electrotechnical Commission (2002). IEC 62278 – railway applications - specification and demonstration of reliability, availability, maintainability and safety (RAMS). URL https://webstore.iec.ch/publication/6747.Google Scholar132International Electrotechnical Commission (2010). Functional safety and IEC 61508. URL https://www.iec.ch/functionalsafety/.Google Scholar133International Electrotechnical Commission (2010). IEC 62278-3 – railway applications - specification and demonstration of reliability, availability, maintainability and safety (RAMS) - Part 3: Guide to the application of IEC 62278 for rolling stock RAM. URL https://webstore.iec.ch/publication/6746.Google Scholar134International Electrotechnical Commission (2016). IEC 62278-4 – railway applications - specification and demonstration of reliability, availability, maintainability and safety (RAMS) - Part 4: RAM risk and RAM life cycle aspects. URL https://webstore.iec.ch/publication/29621.Google Scholar135International Electrotechnical Commission (2017). IEC TC 69 – electric road vehicles and electric industrial trucks. URL https://www.iec.ch/dyn/www/f?p=103:7:0::::FSP_ORG_ID:1255.Google Scholar136International Electrotechnical Commission (2017). IEC TC 9 – electrical equipment and systems for railways. URL https://www.iec.ch/dyn/www/f?p=103:7:0::::FSP_ORG_ID,FSP_LANG_ID:1248,25.Google Scholar137International Electrotechnical Commission (2017c). IEC TR 60601-4-1 – medical electrical equipment – part 4-1: Guidance and interpretation - medical electrical equipment and medical electrical systems employing a degree of autonomy. URL https://webstore.iec.ch/publication/29312.Google Scholar138International Electrotechnical Commission (2019). IEC 63243 ED1 – interoperability and safety of dynamic wireless power transfer (WPT) for electric vehicles. URL https://www.iec.ch/dyn/www/f?p=103:38:1864379252239.Google Scholar139International Organization for Standardization. ISO web site. URL https://www.iso.org/.Google Scholar140International Organization for Standardization (1947). ISO/TC 20 – Aircraft and space vehicles. URL https://www.iso.org/committee/46484.html.Google Scholar141International Organization for Standardization (1951). ISO/TC 76 – transfusion, infusion and injection, and blood processing equipment for medical and pharmaceutical use. URL https://www.iso.org/committee/50044.html.Google Scholar142International Organization for Standardization (1988). ISO/TC 194 – biological and clinical evaluation of medical devices. URL https://www.iso.org/committee/54508.html.Google Scholar143International Organization for Standardization (1994). ISO/TC 210 – quality management and corresponding general aspects for medical devices. URL https://www.iso.org/committee/54892.html.Google Scholar144International Organization for Standardization (1998). ISO/TC 215 – health informatics. URL https://www.iso.org/committee/54960.html.Google Scholar145International Organization for Standardization (2012). ISO 21500 – guidance on project management. URL https://www.iso.org/standard/50003.html.Google Scholar146International Organization for Standardization (2012). ISO/TC 269 – railway applications. URL https://www.iso.org/committee/661629.html.Google Scholar147International Organization for Standardization (2014). ISO 13482 – robots and robotic devices – safety requirements for personal care robots. URL https://www.iso.org/standard/53820.html.Google Scholar148International Organization for Standardization (2015). ISO/TC 299 – robotics. URL https://www.iso.org/committee/5915511.html.Google Scholar149International Organization for Standardization (2016). ISO and road vehicles. URL https://www.iso.org/publication/PUB100292.html.Google Scholar150International Organization for Standardization (2018). ISO 21245 – railway applications – railway project planning process – guidance on railway project planning. URL https://www.iso.org/standard/74012.html.Google Scholar151International Organization for Standardization (2018). ISO 26262-1 – road vehicles – functional safety. URL https://www.iso.org/standard/68383.html.Google Scholar152International Organization for Standardization (2019). ISO and health. URL https://www.iso.org/publication/PUB100343.html.Google Scholar153International Organization for Standardization (ISO) (2014). ISO 13482 – robots and robotic devices — safety requirements for personal care robots. URL https://www.iso.org/standard/53820.html.Google Scholar154International Organization for Standardization (ISO) (2016). ISO/TS 15066 – robots and robotic devices – collaborative robots. URL https://www.iso.org/standard/62996.html.Google Scholar155International Organization for Standardization (ISO) (2017). ISO/TR 20218-2 – robotics – safety design for industrial robot systems – part 2: Manual load/unload stations. URL https://www.iso.org/standard/70584.html.Google Scholar156International Organization for Standardization (ISO) (2017). ISO/TR 23482-2 – robotics – application of ISO 13482 – part 2: Application guidelines. URL https://www.iso.org/standard/71627.html.Google Scholar157International Organization for Standardization (ISO) (2018). ISO/TR 20218-1 – robotics – safety design for industrial robot systems – part 1: End-effectors. URL https://www.iso.org/standard/69488.html.Google Scholar158International union of railways – Union Internationale des Chemins de fer. UIC web site. URL https://uic.org/.Google Scholar159Jasim, O. A., & Veres, S. M. (Oct 2017). Towards formal proofs of feedback control theory. In Proc. 21st International Conference on System Theory, Control and Computing (ICSTCC) (pp. 43–48).CrossrefGoogle Scholar160Jennings NR, Sycara KP, and Wooldridge M A roadmap of agent research and development Autonomous Agents and Multi-Agent Systems 1998 1 1 7-38CrossrefGoogle Scholar161Jovinelly J and Netelkos J The crafts and culture of a medieval guild 2006 New York, NY Rosen PublishingGoogle Scholar162Julius A and Pappas G Approximations of stochastic hybrid systems IEEE Transactions on Automatic Control 2009 54 6 1193-1203CrossrefGoogle Scholar163Kempa, B., Zhang, P., Jones, P. H., Zambreno, J., & Rozier, K. Y. (September 2020). Embedding Online Runtime Verification for Fault Disambiguation on Robonaut2. In Proceedings of the 18th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS), volume TBD of Lecture Notes in Computer Science (LNCS), page TBD, Vienna, Austria: Springer. : TBD. URL http://research.temporallogic.org/papers/KZJZR20.pdf.Google Scholar164Kepuska, V., & Bohouta, G. (2018). Next-generation of virtual personal assistants (microsoft cortana, apple siri, amazon alexa and google home). In 2018 IEEE 8th Annual Computing and Communication Workshop and Conference (CCWC) (pp. 99–103). IEEE.Google Scholar165Khan SG, Herrmann G, Pipe AG, Melhuish C, and Spiers A Safe adaptive compliance control of a humanoid robotic arm with anti-windup compensation and posture Control Int. J. Social Robotics 2010 2 3 305-319CrossrefGoogle Scholar166Knight, J. C. (2002). Safety critical systems: challenges and directions. In W. Tracz, M. Young, & J. Magee (Eds.), Proceedings of the 24th International Conference on Software Engineering, ICSE 2002, 19-25 May 2002, Orlando, Florida, USA (pp. 547–550). ACM.CrossrefGoogle Scholar167Kohlberg, L. (1969). Stage and sequence: The cognitive-developmental approach to socialization. In D. Goslin (Ed.), Handbook of Socialization Theory and Research (pp. 347–480). Rand McNally.Google Scholar168Kohlberg L Essays on Moral Development. Volume I: The philosophy of moral development 1981 New York Harper & RowGoogle Scholar169Kohlberg L Essays on Moral Development. Volume II: The psychology of moral development: the nature and validity of moral stages 1984 NewYork Harper & RowGoogle Scholar170Kong, J., & Lomuscio, A. (2017). Symbolic model checking multi-agent systems against CTLK specifications. In K. Larson, M. Winikoff, S. Das, & E. H. Durfee (Eds.), Proceedings of the 16th Conference on Autonomous Agents and MultiAgent Systems, AAMAS 2017, São Paulo, Brazil, May 8-12, 2017* (pp. 114–122). ACM. URL http://dl.acm.org/citation.cfm?id=3091147.Google Scholar171Kong, J., & Lomuscio, A. (2018). Model checking multi-agent systems against LDLK specifications on finite traces. In E. André, S. Koenig, M. Dastani, & G. Sukthankar (Eds.), Proceedings of the 17th International Conference on Autonomous Agents and MultiAgent Systems, AAMAS 2018, Stockholm, Sweden, July 10-15, 2018 (pp. 166–174). International Foundation for Autonomous Agents and Multiagent Systems Richland, SC, USA / ACM. URL http://dl.acm.org/citation.cfm?id=3237414.Google Scholar172Kowalski, R. A., & Sadri, F. (1996). Towards a unified agent architecture that combines rationality with reactivity. In D. Pedreschi, & C. Zaniolo (Eds.), Logic in Databases, International Workshop LID’96, San Miniato, Italy, July 1-2, 1996, Proceedings, volume 1154 of Lecture Notes in Computer Science (pp. 137–149). Springer.CrossrefGoogle Scholar173Leveson NG and Turner CS An investigation of the Therac-25 accidents Computer 1993 26 7 18-41 ISSN 1558-0814CrossrefGoogle Scholar174Levine, D. M. (23May 2013). A day in the quiet life of a NYSE floor trader. Fortune. URL https://fortune.com/2013/05/29/a-day-in-the-quiet-life-of-a-nyse-floor-trader/.Google Scholar175Li, J., & Rozier, K. Y. (November 2018). MLTL Benchmark Generation via Formula Progression. In Proceedings of the 18th International Conference on Runtime Verification (RV18), Limassol, Cyprus. Springer-Verlag.Google Scholar176Li, J., Vardi, M., & Rozier, K. Y. (July 2019). Satisfiability checking for mission-time LTL. In Proceedings of 31st International Conference on Computer Aided Verification (CAV’19), LNCS. Springer.CrossrefGoogle Scholar177Lomuscio, A., & Raimondi, F. (2006). Model checking knowledge, strategies, and games in multi-agent systems. In H. Nakashima, M. P. Wellman, G. Weiss, & P. Stone (Eds.), 5th International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS 2006), Hakodate, Japan, May 8-12, 2006 (pp. 161–168). ACM.CrossrefGoogle Scholar178Luckcuck M, Farrell M, Dennis L, Dixon C, and Fisher M Formal specification and verification of autonomous robotic systems: A survey ACM Computing Surveys 2019 52 5 100:1-100:41CrossrefGoogle Scholar179Luckow KS and Păsăreanu CS Symbolic pathfinder v7 ACM SIGSOFT Software Engineering Notes 2014 39 1 1-5CrossrefGoogle Scholar180Maggi, F. M., Montali, M., Westergaard, M., & van der Aalst, W. M. P. (2011). Monitoring business constraints with linear temporal logic: An approach based on colored automata. In S. Rinderle-Ma, F. Toumani, & K. Wolf (Eds.), Proceedings of 9th International Conference on Business Process Management (BPM’11), volume 6896 of LNCS (pp. 132–147). Springer.CrossrefGoogle Scholar181Marr, B. (2017). The biggest challenges facing artificial intelligence (AI) in business and society. Forbes. URL https://www.forbes.com/sites/bernardmarr/2017/07/13/the-biggest-challenges-facing-artificial-intelligence-ai-in-business-and-society/.Google Scholar182MathWorks. Polyspace bug finder. URL https://in.mathworks.com/products/polyspace-bug-finder.html.Google Scholar183Mattarei, C., Cimatti, A., Gario, M., Tonetta, S., Rozier, K. Y., & (September 2015). Comparing different functional allocations in automated air traffic control design. In Proceedings of Formal Methods in Computer-Aided Design (FMCAD,. (2015). Austin, Texas, U.S.A, IEEE/ACM.Google Scholar184Matthias A Robot lies in health care: when is deception morally permissible? Kennedy Institute of Ethics Journal 2011 25 2 279-301Google Scholar185McMillan, K. L. (1999). The SMV language. Cadence Berkeley Labs (pp. 1–49).Google Scholar186Merriam-Webster Dictionary (2020). Definition of ‘reliable’. URL https://www.merriam-webster.com/dictionary/reliable.Google Scholar187Moosbrugger, P., Rozier, K. Y., & Schumann, J. (April 2017). R2U2: Monitoring and Diagnosis of Security Threats for Unmanned Aerial Systems. In Formal Methods in System Design (FMSD) (pp. 1–31). Springer-Verlag.CrossrefGoogle Scholar188Munoz, C., Narkawicz, A., & Chamberlain, J. (2013). A TCAS-II resolution advisory detection algorithm. In AIAA Guidance, Navigation, and Control (GNC) Conference, page 4622.Google Scholar189Muñoz, C., Narkawicz, A., Hagen, G., Upchurch, J., Dutle, A., Consiglio, M., & Chamberlain, J. (2015). Daidalus: detect and avoid alerting logic for unmanned systems. In 2015 IEEE/AIAA 34th Digital Avionics Systems Conference (DASC) (pp. 5A1–1). IEEE.Google Scholar190Musuvathi M, Engler DR, et al. Model checking large network protocol implementations NSDI 2004 4 12-12Google Scholar191Negroponte N Being Digital 1996 New York, NY, USA Random House ISBN 0-679-43919-6Google Scholar192Nguyen, C. D., Perini, A., Bernon, C., Pavón, J., & Thangarajah, J. (2009). Testing in multi-agent systems. In M. P. Gleizes, & J. J. Gómez-Sanz (Eds.), Agent-Oriented Software Engineering X - 10th International Workshop, AOSE. (2009). Budapest, Hungary, May 11–12, 2009, Revised Selected Papers (Vol. 6038, pp. 180–190)., Lecture Notes in Computer Science New york: Springer.Google Scholar193Patchett C, Jump M, and Fisher M Institution of engineering and technology:in engineering and technology reference Safety and Certification of Unmanned Air Systems 2015CrossrefGoogle Scholar194Paulson LC A Generic Theorem Prover 1994 New york SpringerGoogle Scholar195Penczek, W., & Lomuscio, A. (2003). Verifying epistemic properties of multi-agent systems via bounded model checking. In The Second International Joint Conference on Autonomous Agents & Multiagent Systems, AAMAS 2003, July 14-18, 2003, Melbourne, Victoria, Australia, Proceedings (pp. 209–216). ACM.CrossrefGoogle Scholar196Perez, I., Dedden, F., & Goodloe, A. (2020). Copilot 3. Technical Report NASA/TM-2020-220587, National Aeronautics and Space Administration.Google Scholar197Pietrantuono, R., & Russo, S. (2018). Robotics software engineering and certification: Issues and challenges. In S. Ghosh, R. Natella, B. Cukic, R. Poston, & N. Laranjeiro (Eds.), 2018 IEEE International Symposium on Software Reliability Engineering Workshops, ISSRE Workshops, Memphis, TN, USA, October 15-18, 2018 (pp. 308–312). IEEE Computer Society.CrossrefGoogle Scholar198Pietronudo, E. (2018). ”Japanese women’s language” and artificial intelligence: Azuma Hikari, gender stereotypes and gender norms. http://hdl.handle.net/10579/12791.Google Scholar199Pike, L. (2007). Modeling time-triggered protocols and verifying their real-time schedules. In Formal Methods in Computer Aided Design (FMCAD’07) (pp. 231–238). IEEE.Google Scholar200platoon. Current State of EU Legislation- Cooperative Dynamic Formation of Platoons for Safe and Energy-optimized Goods Transportation. URL http://www.companion-project.eu/wp-content/uploads/COMPANION-D2.2-Current-state-of-the-EU-legislation.pdf.Google Scholar201Platzer A Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics 2010 Heidelberg Springer ISBN 978-3-642-14508-7CrossrefGoogle Scholar202Platzer, A., & Quesel, J.-D. (2008). KeyMaera: A Hybrid Theorem Prover for Hybrid Systems. In A. Armando, P. Baumgartner, & G. Dowek (Eds.), Proceedings of 4th International Joint Conference on Automated Reasoning (IJCAR), volume 5195 of LNCS (pp. 171–178). Springer.Google Scholar203Poore JH, Mills HD, and Mutchler D Planning and certifying software system reliability IEEE Software 1993 10 1 88-99CrossrefGoogle Scholar204Quirchmayr, T. (2018). Retrospective semi-automated software feature extraction from natural language user manuals. PhD thesis, University of Heidelberg, Germany. URL http://www.ub.uni-heidelberg.de/archiv/25322.Google Scholar205Radio Technical Commission for Aeronautics. RTCA web site. URL https://www.rtca.org/.Google Scholar206Radio Technical Commission for Aeronautics (1992). DO-178B – software considerations in airborne systems and equipment certification. URL https://www.rtca.org/content/standards-guidance-materials.Google Scholar207Radio Technical Commission for Aeronautics (1992). DO-278A – software integrity assurance considerations for communication, navigation, surveillance and air traffic management (CNS/ATM) systems. URL https://www.rtca.org/content/standards-guidance-materials.Google Scholar208Radio Technical Commission for Aeronautics (2000). DO-254 – design assurance guidance for airborne electronic hardware. URL https://www.rtca.org/content/standards-guidance-materials.Google Scholar209Radio Technical Commission for Aeronautics (2011). DO-333 – formal methods supplement to DO-178C and DO-278A. URL https://www.rtca.org/content/standards-guidance-materials.Google Scholar210Radio Technical Commission for Aeronautics (2012). DO-178C/ED-12C – software considerations in airborne systems and equipment certification. URL https://www.rtca.org/content/standards-guidance-materials.Google Scholar211Raman, V., Lignos, C., Finucane, C., Lee, K. C., Marcus, M. P., & Kress-Gazit, H. (2013). Sorry dave, i’m afraid i can’t do that: Explaining unachievable robot tasks using natural language. volume 2. Citeseer.Google Scholar212Ramesh B and Jarke M Toward reference models for requirements traceability IEEE Transactions on Software Engineering 2001 27 1 58-93CrossrefGoogle Scholar213Reinbacher, T., Rozier, K. Y., & Schumann, J. (2014). Temporal-logic based runtime observer pairs for system health management of real-time systems. In Proceedings of 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’14), volume LNCS 8413 (pp. 357–372). Springer.CrossrefGoogle Scholar214Rinehart, D. J., Knight, J. C., & Rowanhill, J. (2017). Understanding what it means for assurance cases to “work”. Technical report, NASA. NASA/CR–2017-219582.Google Scholar215Rosu G On safety properties and their monitoring Science Annals of Computer Science. 2012 22 2 327-365CrossrefGoogle Scholar216Rozier K and Vardi M LTL satisfiability checking International Journal on Software Tools for Technology Transfer (STTT) 2010 12 2 123-137CrossrefGoogle Scholar217Rozier KY Linear Temporal Logic Symbolic Model Checking Computer Science Review Journal 2011 5 2 163-203CrossrefGoogle Scholar218Rozier, K. Y. (2016). Specification: The biggest bottleneck in formal methods and autonomy. In Proceedings of 8th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE’16), volume LNCS 9971 (pp. 1–19). Springer.CrossrefGoogle Scholar219Rozier, K. Y. (April 2019). From simulation to runtime verification and back: Connecting single-run verification techniques. In Proceedings of the Spring Simulation Conference (SpringSim) (pp. 1–10), Tucson, AZ, USA. Society for Modeling & Simulation International. https://dl.acm.org/doi/10.5555/3338027.3338054.Google Scholar220Rozier, K. Y., & Schumann, J. (2017). R2U2: Tool overview. In Proceedings of International Workshop on Competitions, Usability, Benchmarks, Evaluation, and Standardisation for Runtime Verification Tools (RV-CUBES) (pp. 138–156).CrossrefGoogle Scholar221SAE International (2018). SAE J3016\_201806 – taxonomy and definitions for terms related to driving automation systems for on-road motor vehicles. URL https://www.sae.org/standards/content/j3016_201806/.Google Scholar222Salem, M., Lakatos, G., Amirabdollahian, F., & Dautenhahn, K. (2015). Would you trust a (faulty) robot?: Effects of error, task type and personality on human-robot cooperation and trust. In Proceedings of 10th ACM/IEEE International Conference on Human-Robot Interaction, HRI 2015, Portland, OR, USA, March 2-5, 2015, (pp. 141–148). ACM.Google Scholar223Salem, M., Lakatos, G., Amirabdollahian, F., & Dautenhahn, K. (2015). Towards Safe and Trustworthy Social Robots: Ethical Challenges and Practical Issues. In Proc. 7th International Conference on Social Robotics (ICSR), volume 9388 of LNCS (pp. 584–593). Springer.Google Scholar224Sartre. SARTRE project. URL https://cordis.europa.eu/project/rcn/92577/brief/en.Google Scholar225Schlatow, J., Möstl, M., Ernst, R., Nolte, M., Jatzkowski, I., Maurer, M., Herber, C., & Herkersdorf, A. (2017). Self-awareness in autonomous automotive systems. In D. Atienza, & G. D. Natale (Eds.), Design, Automation & Test in Europe Conference & Exhibition, DATE 2017, Lausanne, Switzerland, March 27-31, 2017 (pp. 1050–1055). IEEE.CrossrefGoogle Scholar226Schumann, J., Moosbrugger, P., & Rozier, K. Y. (September 2016). Runtime Analysis with R2U2: A Tool Exhibition Report. In Proceedings of the 16th International Conference on Runtime Verification (RV16). Madrid, Spain: Springer-Verlag.Google Scholar227Scrapper, C., Balakirsky, S., & Messina, E. (2006). MOAST and USARSim: a combined framework for the development and testing of autonomous systems. In Unmanned Systems Technology VIII, volume 6230, page 62301T. International Society for Optics and Photonics.Google Scholar228SCSC - The Safety-Critical Systems Club. SCSC – goal structuring notation community standard (version 2). URL https://scsc.uk/scsc-141B.Google Scholar229Shankar, N. (2008). Trust and automation in verification tools. In Automated Technology for Verification and Analysis, 6th International Symposium, ATVA 2008, Seoul, Korea, October 20-23, 2008. Proceedings (pp. 4–17).CrossrefGoogle Scholar230Sharkey, A., & Wood, N. (2014). The paro seal robot: demeaning or enabling. In Proceedings of AISB, volume 36.Google Scholar231Stout D Stone toolmaking and the evolution of human culture and cognition Philosophical Transactions of the Royal Society B: Biological Sciences 2011 366 1567 1050-1059CrossrefGoogle Scholar232Swaroop, D. (1997). String stability of interconnected systems: An application to platooning in automated highway systems. California Partners for Advanced Transit and Highways (PATH).Google Scholar233Tabakov D, Rozier KY, and Vardi MY Optimized temporal monitors for SystemC Formal Methods in System Design 2012 41 3 236-268CrossrefGoogle Scholar234The European Parliament (2018). Regulation (EU) 2018/1139 of the European Parliament and of the Council of 4 July 2018 on common rules in the field of civil aviation and establishing a European Union Aviation Safety Agency, and amending Regulations (EC) No 2111/2005, (EC) No 1008/2008, (EU) No 996/2010, (EU) No 376/2014 and Directives 2014/30/EU and 2014/53/EU of the European Parliament and of the Council, and repealing Regulations (EC) No 552/2004 and (EC) No 216/2008 of the European Parliament and of the Council and Council Regulation (EEC) No 3922/91 (Text with EEA relevance). URL https://eur-lex.europa.eu/legal-content/EN/TXT/?uri=CELEX:32018R1139.Google Scholar235The IEEE Global Initiative on Ethics of Autonomous and Intelligent Systems, (Ed.) (2019). Ethically Aligned Design: A Vision for Prioritizing Human Well-being with Autonomous and Intelligent Systems. IEEE. URL https://standards.ieee.org/content/ieee-standards/en/industry-connections/ec/ autonomous-systems.html.Google Scholar236The Software Testing Help (STH) Blog (2019). Top 40 static code analysis tools (best source code analysis tools). URL https://www.softwaretestinghelp.com/tools/top-40-static-code-analysis-tools/.Google Scholar237Tolmeijer, S., Weiss, A., Hanheide, M., Lindner, F., Powers, T. M., Dixon, C., & Tielman, M. L. (2020). Taxonomy of trust-relevant failures and mitigation strategies. In Proceedings of the 2020 ACM/IEEE International Conference on Human-Robot Interaction (HRI) (pp. 3-12). Association for Computing Machinery.CrossrefGoogle Scholar238Tomayko, J. E. (2003). The story of self-repairing flight control systems. In C. Gelzer (Ed.), Dryden Historical Study No. 1. : NASA Dryden Flight Research Center.Google Scholar239Torens C, Adolf F, and Goormann L Certification and software verification considerations for autonomous unmanned aircraft Journal of Aerospace Information System. 2014 11 10 649-664CrossrefGoogle Scholar240Tuncali CE, Fainekos G, Prokhorov D, Ito H, and Kapinski J Requirements-driven test generation for autonomous vehicles with machine learning components IEEE Transactions on Intelligent Vehicles 2019 5 2 265-280CrossrefGoogle Scholar241U.S. Department of Transportation (2016). Federal automated vehicles policy. URL https://www.transportation.gov/AV/federal-automated-vehicles-policy-september-2016.Google Scholar242van der Aalst, W. M. P. (2002). Making work flow: On the application of petri nets to business process management. In J. Esparza, & C. Lakos (Eds.), Proceedings of 23rd International Conference on Applications and Theory of Petri Nets (ICATPN’02), volume 2360 of Lecture Notes in Computer Science (pp. 1–22). Springer.CrossrefGoogle Scholar243van der Aalst WMP Process Mining - Discovery, Conformance and Enhancement of Business Processes 2011 New york Springer ISBN 978-3-642-19344-6CrossrefGoogle Scholar244Visser W, Havelund K, Brat GP, Park S, and Lerda F Model checking programs Automated Software Engineering 2003 10 2 203-232CrossrefGoogle Scholar245Wada K, Shibata T, Asada T, and Musha T Robot therapy for prevention of dementia at home Journal of Robotics and Mechatronics 2007 19 6 691CrossrefGoogle Scholar246Webster M, Dixon C, Fisher M, Salem M, Saunders J, Koay K, Dautenhahn K, and Saez-Pons J Toward reliable autonomous robotic assistants through formal verification: A Case Study IEEE Transactions on Human-Machine Systems 2016 46 2 186-196 ISSN 2168-2291CrossrefGoogle Scholar247Webster MP, Cameron N, Fisher M, and Jump M Generating certification evidence for autonomous unmanned aircraft using model checking and simulation Journal of Aerospace Information System. 2014 11 5 258-279CrossrefGoogle Scholar248Whitehurst, R. A., & Lunt, T. F. (1989). The sea view verification. In Proceedings of 2nd IEEE Computer Security Foundations Workshop (CSFW’89) (pp. 125–132). IEEE Computer Society.CrossrefGoogle Scholar249Winfield AFT, Michael K, Pitt J, and Evers V Machine ethics: The design and governance of ethical AI and autonomous systems Proceedings of the IEEE 2019 107 3 509-517CrossrefGoogle Scholar250Winikoff M BDI agent testability revisited Journal of Autonomous Agents and Multi-Agent Systems (JAAMAS) 2017 31 5 1094-1132CrossrefGoogle Scholar251Winikoff M and Cranefield S On the testability of BDI agent systems Journal of Artificial Intelligence Research 2014 51 71-131CrossrefGoogle Scholar252Wohlin C and Runeson P Certification of software components IEEE Trans. Software Eng. 1994 20 6 494-499CrossrefGoogle Scholar253Woodman R, Winfield AFT, Harper CJ, and Fraser M Building safer robots: Safety driven control International Journal of Robotics Research 2012 31 13 1603-1626CrossrefGoogle Scholar254Wooldridge, M., & Jennings, N. R. (Eds.). (1995). Intelligent Agents, ECAI-94 Workshop on Agent Theories, Architectures, and Languages, Amsterdam, The Netherlands, August 8–9, 1994, Proceedings, volume LNCS 890. Springer.CrossrefGoogle Scholar255Wooldridge M and Jennings NR Intelligent agents: theory and practice Knowledge Eng. Review 1995 10 2 115-152CrossrefGoogle Scholar256Working Party on Automated/autonomous and Connected Vehicles, Economic Commission for Europe (2020). Proposal for a new UN regulation on uniform provisions concerning the approval of vehicles with regards to Automated Lane Keeping System. URL https://undocs.org/ECE/TRANS/WP.29/2020/81.Google Scholar257Xiao, L., Lewis, P. H., & Dasmahapatra, S. (2008). Secure Interaction Models for the HealthAgents System. In Proc. 27th International Conference on Computer Safety, Reliability, and Security (SAFECOMP), volume 5219 of LNCS (pp. 167–180). Springer. ISBN 978-3-540-87697-7.Google Scholar258Yang, M., & Chow, K.-P. (2015). An information extraction framework for digital forensic investigations. In IFIP International Conference on Digital Forensics, (pp. 61–76). Springer.Google Scholar259Yorke-Smith, N., Saadati, S., Myers, K. L., & Morley, D. N. (2009). Like an intuitive and courteous butler: A proactive personal agent for task management. In Proceedings of 8th International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS’09) (pp. 337–344).Google Scholar260Yu H, Lin C-W, and Kim B Automotive software certification: current status and challenges SAE International journal of passenger cars-electronic and electrical systems 2016 9 74-80CrossrefGoogle Scholar261Zhang, N., Wang, J., & Ma, Y. (2018). Mining domain knowledge on service goals from textual service descriptions. IEEE Transactions on Services Computing (pp. 1–1). ISSN 1939-1374.CrossrefGoogle Scholar262Zhao Y and Rozier KY Formal specification and verification of a coordination protocol for an automated air traffic control system Science of Computer Programming Journal 2014 96 3 337-353CrossrefGoogle Scholar263Zhao, Y., & Rozier, K. Y. (November 2014). Probabilistic model checking for comparative analysis of automated air traffic control systems. In Proceedings of the 33rd IEEE/ACM International Conference On Computer-Aided Design (ICCAD 2014) (pp. 690–695). San Jose, California, U.S.A. IEEE/ACM.Google Scholar View all259. Towards a framework for certification of reliable autonomous systems 260. Computer systems organization 261. General and reference 262. Cross-computing tools and techniques 263. Software and its engineering 264. Software creation and management 265. Software verification and validation 266. Software organization and properties 267. Software functional properties 268. Formal methods 269. Theory of computation 270. Semantics and reasoning 271. Program reasoning 272. Program verification

Formal methods for the certification of autonomous unmanned aircraft systems

SAFECOMP'11: Proceedings of the 30th international conference on Computer safety, reliability, and security In this paper we assess the feasibility of using formal methods, and model checking in particular, for the certification of Unmanned Aircraft Systems (UAS) within civil airspace. We begin by modelling a basic UAS control system in PROMELA, and verify it …

CCNP BCMSN Exam Certification Guide (3rd Edition) (Exam Certification Guide)

CCSP SNPA Official Exam Certification Guide (3rd Edition) (Exam Certification Guide)

Published In

cover image Autonomous Agents and Multi-Agent Systems Autonomous Agents and Multi-Agent Systems Volume 35, Issue 1Apr 2021604 pagesISSN:1387-2532Issue’s Table of Contents© The Author(s) 2020. Autonomous Agents and Multi-Agent Systems Volume 35, Issue 1Apr 2021604 pagesISSN:1387-2532Issue’s Table of Contents © The Author(s) 2020.

Publisher

Kluwer Academic Publishers

United States

Kluwer Academic Publishers

United States

Publication History

Published: 01 April 2021Accepted: 15 November 2020 Published: 01 April 2021 Accepted: 15 November 2020

Qualifiers

Research-article
Research-article

Funding Sources

Delft University of Technology
Delft University of Technology

Other Metrics

View Article Metrics View Article Metrics

Article Metrics

10Total CitationsView Citations
0Total Downloads
Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 13 Sep 2024- 10Total CitationsView Citations

0Total Downloads
Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 13 Sep 2024

Other Metrics

View Author Metrics View Author Metrics

Cited By

View all- Giachetti Gde la Vara JMarín B(2024)Model-driven gap analysis for the fulfillment of quality standards in software development processesSoftware Quality Journal10.1007/s11219-023-09649-x32:1(255-282)Online publication date: 1-Mar-2024https://dl.acm.org/doi/10.1007/s11219-023-09649-x

Aurandt AJones PRozier KWongpiromsarn T(2024)Multimodal Model Predictive Runtime Verification for Safety of Autonomous Cyber-Physical SystemsFormal Methods for Industrial Critical Systems10.1007/978-3-031-68150-9_13(220-244)Online publication date: 9-Sep-2024https://dl.acm.org/doi/10.1007/978-3-031-68150-9_13
Castellani ABenassi MBalboni G(2024)Ethical Principles in Artificial Intelligence for Children: A Protocol for a Scoping ReviewComputational Science and Its Applications – ICCSA 2024 Workshops10.1007/978-3-031-65282-0_8(124-137)Online publication date: 1-Jul-2024https://dl.acm.org/doi/10.1007/978-3-031-65282-0_8
Yang YAgmon NAn BRicci AYeoh W(2023)Verifiably Safe Decision-Making for Autonomous SystemsProceedings of the 2023 International Conference on Autonomous Agents and Multiagent Systems10.5555/3545946.3599142(2973-2975)Online publication date: 30-May-2023https://dl.acm.org/doi/10.5555/3545946.3599142
Abeywickrama DBennaceur AChance GDemiris YKordoni ALevine MMoffat LMoreau LMousavi MNuseibeh BRamamoorthy SRingert JWilson JWindsor SEder K(2023)On Specifying for TrustworthinessCommunications of the ACM10.1145/362469967:1(98-109)Online publication date: 21-Dec-2023https://dl.acm.org/doi/10.1145/3624699
Horne RLaw-Walsh CAssaad ZJoiner K(2023)Ten regulatory principles to scaffold the design, manufacture, and use of trustworthy autonomous systems, illustrated in a maritime contextProceedings of the First International Symposium on Trustworthy Autonomous Systems10.1145/3597512.3599701(1-12)Online publication date: 11-Jul-2023https://dl.acm.org/doi/10.1145/3597512.3599701
Zoor MApvrille LPacalet RCoudert S(2023)Execution trace analysis for a precise understanding of latency violationsSoftware and Systems Modeling (SoSyM)10.1007/s10270-022-01076-z22:5(1519-1541)Online publication date: 6-Jan-2023https://dl.acm.org/doi/10.1007/s10270-022-01076-z
Christie SChopra ASingh M(2022)Mandrake: multiagent systems as a basis for programming fault-tolerant decentralized applicationsAutonomous Agents and Multi-Agent Systems10.1007/s10458-021-09540-836:1Online publication date: 1-Apr-2022https://dl.acm.org/doi/10.1007/s10458-021-09540-8
de Silva LMycroft A(2022)Toward trustworthy programming for autonomous concurrent systemsAI & Society10.1007/s00146-022-01463-638:2(963-965)Online publication date: 8-Jun-2022https://dl.acm.org/doi/10.1007/s00146-022-01463-6
Peleska JHaxthausen ALecomte T(2022)Standardisation Considerations for Autonomous Train ControlLeveraging Applications of Formal Methods, Verification and Validation. Practice10.1007/978-3-031-19762-8_22(286-307)Online publication date: 22-Oct-2022https://dl.acm.org/doi/10.1007/978-3-031-19762-8_22

View all

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication Check if you have access through your login credentials or your institution to get full access on this article.

Copy LinkCopied!

Copying failed.

XLinkedInRedditFacebookemailCopy LinkCopied!

Copying failed.

XLinkedInRedditFacebookemailMichaelFisherUniversity of Manchester, Manchester, United KingdomView Profile VivianaMascardiUniversity of Genova, Genova, ItalyView Profile Kristin YvonneRozierIowa State University, Ames, IA, USAView Profile Bernd-HolgerSchlingloffHumboldt University and Fraunhofer FOKUS, Berlin, GermanyView Profile MichaelWinikoffVictoria University of Wellington, Wellington, New ZealandView Profile NeilYorke-SmithDelft University of Technology, Delft, The Netherlandshttps://orcid.org/0000-0002-1814-3515View Profile

Ce site ne collecte que des articles connexes. Pour voir l’original, veuillez copier et ouvrir le lien suivant :Towards a framework for certification of reliable autonomous systems Autonomous Agents and Multi-Agent Systems

New Citation Alert added!
New Citation Alert!
A computational system is called autonomous if it is able to make its own decisions, or take its own actions, without human supervision or control. The capability and spread of such systems have reached the point where they are beginning to touch much of everyday life. However, regulators grapple with how to deal with autonomous systems, for example how could we certify an Unmanned Aerial System for autonomous use in civilian airspace? We here analyse what is needed in order to provide verified reliable behaviour of an autonomous system, analyse what can be done as the state-of-the-art in automated verification, and propose a roadmap towards developing regulatory guidelines, including articulating challenges to researchers, to engineers, and to regulators. Case studies in seven distinct domains illustrate the article. 124me Company. 24me Smart Personal Assistant. URL https://www.twentyfour.me/.Google Scholar2Abate, A., Katoen, J.-P., & Mereacre, A. (2011). Quantitative automata model checking of autonomous stochastic hybrid systems. In Proceedings of the 14th ACM International Conference on Hybrid Systems: Computation and Control (HSCC) (pp. 83–92). ACM.Google Scholar3Adolf, F.-M., Faymonville, P., Finkbeiner, B., Schirmer, S., & Torens, C. (2017). Stream runtime monitoring on UAS. In Proceedings of International Conference on Runtime Verification (pp. 33–49).Google Scholar4Alexander, R., Hall-May, M., & Kelly, T. (2007). Certification of autonomous systems. In Proceedings of 2nd Systems Engineering for Autonomous Systems (SEAS) Defence Technology Centre (DTC) Annual Technical Conference.Google Scholar5Alur R, Henzinger TA, Lafferriere G, and Pappas GJ Discrete abstractions of hybrid systems Proceedings of the IEEE 2000 88 7 971-984CrossrefGoogle Scholar6Alves GV, Dennis L, Fernandes L, and Fisher M Leitner A, Watzenig D, and Ibanez-Guzman J Reliable Decision-Making in Autonomous Vehicles Validation and verification of automated systems: Results of the ENABLE-S3 Project 2020 Cham Springer, New york 105-117CrossrefGoogle Scholar7Amirabdollahian, F., Dautenhahn, K., Dixon, C., Eder, K., Fisher, M., Koay, K. L., Magid, E., Pipe, A., Salem, M., Saunders, J., & Webster, M. (2013). Can You Trust Your Robotic Assistant? In International Conference on Social Robotics, volume 8239 of LNCS (pp. 571–573). Springer.Google Scholar8Ancona, D., Ferrando, A., & Mascardi, V. (2016). Comparing trace expressions and Linear Temporal Logic for runtime verification. In Theory and Practice of Formal Methods, (pp. 47–64). Springer, New yorkGoogle Scholar9Ancona D, Ferrando A, and Mascardi V Parametric runtime verification of multiagent systems AAMAS 2017 17 1457-1459Google Scholar10Anderson, M., & Anderson, S. L. (2008). EthEl: Toward a principled ethical eldercare robot. In Proc. AAAI Fall Symposium on AI in Eldercare: New Solutions to Old Problems.Google Scholar11Anderson, M., & Anderson, S. L. (2011). Machine Ethics. : Cambridge University Press.Google Scholar12Appel, K., & Haken, W. (1989). Every Planar Map is Four-Colorable, volume 98 of Contemporary Mathematics. Providence, RI: American Mathematical Society. ISBN 0-8218-5103-9.CrossrefGoogle Scholar13Arcaini, P., Bonfanti, S., Gargantini, A., Mashkoor, A., & Riccobene, E. (2015). Formal validation and verification of a medical software critical component. In 13th ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2015, Austin, TX, USA, September 21-23, 2015 (pp. 80–89). IEEE.CrossrefGoogle Scholar14Areias, C., Cunha, J. C., Iacono, D., & Rossi, F. (2014). Towards certification of automotive software. In Proceedings of 25th IEEE International Symposium on Software Reliability Engineering Workshops ISSRE (pp. 491–496).CrossrefGoogle Scholar15Arkin, R. C. (2008). Governing lethal behavior: embedding ethics in a hybrid deliberative/reactive robot architecture. In Proceedings of 3rd ACM/IEEE international conference on Human Robot Interaction (HRI’08) (pp. 121–128).CrossrefGoogle Scholar16AV-TEST Institute. (2019). Robot vacuums undergo a security check: trustworthy helpers around the house or chatty cleaning appliances? URL https://www.av-test.org/en/news/robot-vacuums-undergo-a-security-check-trustworthy-helpers-around-the-house-or-chatty-cleaning-appli/. Archived from the original URL at: https://web.archive.org/web/20200613234231/https://www.av-test.org/en/news/robot-vacuums-undergo-a-security-check-trustworthy-helpers-around-the-house-or-chatty-cleaning-appli/.Google Scholar17Baier, C., & Katoen, J.-P. (2008). Principles of Model Checking. MIT Press. ISBN 026202649X.Google Scholar18Bao W, Yue J, and Rao Y A deep learning framework for financial time series using stacked autoencoders and long-short term memory PLOS One 2017 12 7 e0180944CrossrefGoogle Scholar19Bartocci E, Bortolussi L, Brázdil T, Milios D, and Sanguinetti G Policy learning in continuous-time markov decision processes using gaussian processes Perform. Eval. 2017 116 84-100CrossrefGoogle Scholar20Basin, D. A., Klaedtke, F., Müller, S., & Pfitzmann, B. (2008). Runtime monitoring of metric first-order temporal properties. In Proceedings of 28th IARCS Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS’08) (pp. 49–60).CrossrefGoogle Scholar21Bauer, B., Müller, J. P., & Odell, J. (2000). Agent UML: A formalism for specifying multiagent software systems. In P. Ciancarini, & M. J. Wooldridge (Eds.), Agent-Oriented Software Engineering, First International Workshop, AOSE 2000, Limerick, Ireland, June 10, 2000, Revised Papers, volume 1957 of Lecture Notes in Computer Science (pp. 91–104). Springer.CrossrefGoogle Scholar22Beck K Test-driven development: by example 2003 Boston Addison-Wesley ProfessionalGoogle Scholar23Beedle, M., van Bennekum, A., Cockburn, A., Cunningham, W., Fowler, M., Highsmith, J., Hunt, A., Jeffries, R., Kern, J., Marick, B., Martin, R. C., Schwaber, K., Sutherland, J., & Thomas, D. (2001). Manifesto for agile software development. URL http://agilemanifesto.org/.Google Scholar24Bensalem, S., Ganesh, V., Lakhnech, Y., Munoz, C., Owre, S., Rueß, H., Rushby, J., Rusu, V., Saıdi, H., Shankar, N., et al. (2000). An overview of SAL. In Proceedings of 5th NASA Langley Formal Methods Workshop. Williamsburg, VA.Google Scholar25Bentzen, M., Lindner, F., Dennis, L., & Fisher, M. (2018). Moral Permissibility of Actions in Smart Home Systems. In Proceedings of FLoC 2018 Workshop on Robots, Morality, and Trust through the Verification Lens.Google Scholar26Benzel, T. (1984). Analysis of a kernel verification. In Proceedings of 1984 IEEE Symposium on Security and Privacy (pp. 125–133).CrossrefGoogle Scholar27Bergenhem, C., Huang, Q., Benmimoun, A., & Robinson, T. (2010). Challenges of platooning on public motorways. In Proceedings of 17th World Congress on Intelligent Transport Systems (pp. 1–12).Google Scholar28Berry PM, Gervasio MT, Peintner B, and Yorke-Smith N PTIME: personalized assistance for calendaring ACM Trans. Intelligent Systems and Technology 2011 2 4 40:1-40:22CrossrefGoogle Scholar29Bertolino, A. (2007). Software testing research: Achievements, challenges, dreams. In L. C. Briand, & A. L. Wolf (Eds.), International Conference on Software Engineering, ISCE 2007, Workshop on the Future of Software Engineering, FOSE 2007, May 23-25, 2007, Minneapolis, MN, USA (pp. 85–103). IEEE Computer Society.CrossrefGoogle Scholar30Biere, A., Heljanko, K., & Wieringa, S. (2011). AIGER 1.9 and beyond. Available at fmv.jku.at/hwmcc11/beyond1.pdf.Google Scholar31Birnbacher D and Birnbacher W Fully autonomous driving: Where technology and ethics meet IEEE Intelligent Systems 2017 32 5 3-4CrossrefGoogle Scholar32Bloomfield R and Bishop P Dale C and Anderson T Safety and assurance cases: Past, present and possible future - an adelard perspective Making systems safer 2010 London, UK Springer 51-67CrossrefGoogle Scholar33Booch G, Rumbaugh J, and Jacobson I The unified modeling language user guide 1999 Redwood City, CA, USA Addison Wesley Longman Publishing Co. Inc. ISBN 0-201-57168-4Google Scholar34Bordini, R. H., Fisher, M., Pardavila, C., & Wooldridge, M. J. (2003). Model checking AgentSpeak. In The Second International Joint Conference on Autonomous Agents & Multiagent Systems, AAMAS 2003, July 14-18, 2003, Melbourne, Victoria, Australia, Proceedings (pp. 409–416). ACM.CrossrefGoogle Scholar35Bordini RH, Fisher M, Visser W, and Wooldridge MJ Model checking rational agents IEEE Intelligent Systems 2004 19 5 46-52CrossrefGoogle Scholar36Bordini RH, Fisher M, Visser W, and Wooldridge MJ Verifying multi-agent programs by model checking Autonomous Agents and Multi-Agent Systems 2006 12 2 239-256CrossrefGoogle Scholar37Bozzano, M., Cimatti, A., Pires, A. F., Jones, D., Kimberly, G., Petri, T., Robinson, R., Tonetta, S. (2015). Formal design and safety analysis of air6110 wheel brake system. In International Conference on Computer Aided Verification (pp. 518–535). Springer.Google Scholar38Brat, G., & Venet, A. (2005). Precise and scalable static program analysis of NASA flight software. In 2005 IEEE Aerospace Conference, (pp. 1–10). IEEE.Google Scholar39Brat, G., Navas, J. A., Shi, N., & Venet, A. (2014). IKOS: A framework for static analysis based on abstract interpretation. In International Conference on Software Engineering and Formal Methods (pp. 271–277). Springer.Google Scholar40Bremner P, Dennis LA, Fisher M, and Winfield AFT On Proactive, transparent, and verifiable ethical reasoning for robots Proceedings of the IEEE 2019 107 3 541-561CrossrefGoogle Scholar41Bringsjord S, Arkoudas K, and Bello P Toward a general logicist methodology for engineering ethically correct robots IEEE Intelligent Systems 2006 21 4 38-44CrossrefGoogle Scholar42British Standards Institution. BSI web site. URL https://www.bsigroup.com/.Google Scholar43British Standards Institution (BSI) (2016). BS 8611 – robots and robotic devices — guide to the ethical design and application. URL https://shop.bsigroup.com/ProductDetail/?pid=000000000030320089.Google Scholar44Brooks RA A robust layered control system for a mobile robot IEEE J. Robotics Autom. 1986 2 1 14-23CrossrefGoogle Scholar45Butler, R. (1996). An introduction to requirements capture using PVS: specification of a simple autopilot. Technical report, NASA Langley Technical Report Server.Google Scholar46Butler RW and Finelli GB The infeasibility of quantifying the reliability of life-critical real-time software IEEE Transactions on Software Engineering 1993 19 1 3-12CrossrefGoogle Scholar47Cambridge Academic Content Dictionary (2020). Definition of ‘certification’. URL https://dictionary.cambridge.org/dictionary/english/certification.Google Scholar48Cambridge English Dictionary (2020). Definition of ‘autopilot’. URL https://dictionary.cambridge.org/dictionary/english/autopilot.Google Scholar49Cambridge English Dictionary (2020). Definition of ‘regulation’. URL https://dictionary.cambridge.org/dictionary/english/regulation.Google Scholar50Cauwels, M., Hammer, A., Hertz, B., Jones, P., & Rozier, K. Y. (September 2020). Integrating runtime verification into an automated uas traffic management system. In Proceedings of DETECT: international workshop on moDeling, vErification and Testing of dEpendable CriTical systems, Communications in Computer and Information Science (CCIS), page TBD, L’Aquila, Italy. Springer.Google Scholar51CENELEC (2011). CENELEC - EN 50128 – railway applications - communication, signalling and processing systems - software for railway control and protection systems. URL https://standards.globalspec.com/std/1678027/EN%2050128Google Scholar52Chapman D Planning for conjunctive goals Artif. Intell. 1987 32 3 333-377CrossrefGoogle Scholar53Charisi, V., Dennis, L., Fisher, M., Lieck, R., Matthias, A., Slavkovik, M., Sombetzki, J., Winfield, A. F. T., & Yampolskiy, R. (Mar. 2017). Towards moral autonomous systems. ArXiv e-prints.Google Scholar54Cimatti, A., Gario, M., & Tonetta, S. (2016). A lazy approach to temporal epistemic logic model checking. In Proceedings of the 2016 International Conference on Autonomous Agents & Multiagent Systems (pp. 1218–1226).Google Scholar55Clarke EM and Schlingloff B-H Robinson A and Voronkov A Model Checking Handbook of Automated Reasoning 2001 Amesterdam Elsevier 1635-1790CrossrefGoogle Scholar56Clarke EM, Grumberg O, and Peled DA Model Checking 2000 London The MIT Press ISBN 0262032708Google Scholar57Cobleigh, J. M., Giannakopoulou, D., & Păsăreanu, C. S. (2003). Learning assumptions for compositional verification. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems (pp. 331–346). Springer, NewyorkGoogle Scholar58Cofer DD, Hatcliff J, Huhn M, and Lawford M Software certification: Methods and tools (Dagstuhl seminar 13051) Dagstuhl Reports 2013 3 1 111-148CrossrefGoogle Scholar59Cousot, P., Cousot, R., Feret, J., Miné, A., Rival, X., Blanchet, B., Monniaux, D., & Mauborgne, L. Astrée. URL http://www.astree.ens.fr/.Google Scholar60Currit PA, Dyer MG, and Mills HD Certifying the reliability of software IEEE Trans. Software Eng. 1986 12 1 3-11CrossrefGoogle Scholar61de Araújo, R. P., Mota, A. C., & Nogueira, S. d. C. (Aug 2017). Probabilistic analysis applied to cleaning robots. In 2017 IEEE International Conference on Information Reuse and Integration (IRI) (pp. 275–282).CrossrefGoogle Scholar62Dalpiaz F, Ferrari A, Franch X, and Palomares C Natural language processing for requirements engineering: The best is yet to come IEEE Software 2018 35 5 115-119CrossrefGoogle Scholar63Dastani M, Torroni P, and Yorke-Smith N Monitoring norms: A multi-disciplinary perspective Knowledge Eng. Review 2018 33 e25CrossrefGoogle Scholar64Dennett DC The Intentional Stance 1989 Cambridge, MA, USA MIT PressGoogle Scholar65Denney E and Pai G Tool support for assurance case development Autom. Softw. Eng. 2018 25 3 435-499CrossrefGoogle Scholar66Dennis, L. A. (2018). The MCAPL Framework including the Agent Infrastructure Layer and Agent Java Pathfinder. The Journal of Open Source Software, 3(24)Google Scholar67Dennis LA and Fisher M Verifiable self-aware agent-based autonomous systems Proceedings of the IEEE 2020 108 7 1011-1026CrossrefGoogle Scholar68Dennis LA, Fisher M, Webster M, and Bordini RH Model checking agent programming languages Automated Software Engineering 2012 19 1 5-63CrossrefGoogle Scholar69Dennis LA, Fisher M, Lincoln NK, Lisitsa A, and Veres SM Practical verification of decision-making in agent-based autonomous systems Automated Software Engineering 2016 23 3 305-359 ISSN 0928-8910CrossrefGoogle Scholar70Dennis LA, Fisher M, Slavkovik M, and Webster M Formal verification of ethical choices in autonomous systems Robotics and Autonomous Systems 2016 77 1-14CrossrefGoogle Scholar71Dixon, C., Webster, M., Saunders, J., Fisher, M., & Dautenhahn, K. (2014). The Fridge Door is Open — Temporal Verification of a Robotic Assistant’s Behaviours. In Advances in Autonomous Robotics Systems (TAROS),volume Lecture Notes in Computer Science (pp. 97–108). Springer. NewyorkGoogle Scholar72Dutilleul, S. C., Lecomte, T., & Romanovsky, A. B. (Eds.) (2019). Proceedings of 3rd International Conference on Reliability, Safety, and Security of Railway Systems (RSSRail’19), volume 11495 of Lecture Notes in Computer Science. Springer. ISBN 978-3-030-18743-9.CrossrefGoogle Scholar73Dutt ND, Regazzoni CS, Rinner B, and Yao X Self-awareness for autonomous systems Proceedings of the IEEE 2020 108 7 971-975CrossrefGoogle Scholar74Economic, U. N., & Council, S. (1968). Vienna Convention on Road Traffic. http://www.unece.org/trans/conventn/crt1968e.pdf.Google Scholar75Edelkamp S, Leue S, and Lluch-Lafuente A Directed explicit-state model checking in the validation of communication protocols International Journal on Software Tools For Technology Transfer 2004 5 2–3 247-267CrossrefGoogle Scholar76Emerson, E. A. (1990). Temporal and modal logic. In Formal Models and Semantics (pp. 995–1072). Elsevier, NewyorkGoogle Scholar77Espejo-García B, Martínez-Guanter J, Pérez-Ruiz M, López-Pellicer FJ, and Zarazaga-Soria FJ Machine learning for automatic rule classification of agricultural regulations: A case study in Spain Computers and Electronics in Agriculture 2018 150 343-352CrossrefGoogle Scholar78European Aviation Artificial Intelligence High Level Group (2020). The FLY AI report – demystifying and accelerating AI in aviation/ATM. URL https://www.eurocontrol.int/publication/fly-ai-report.Google Scholar79European Committee for Electrotechnical Standardisation. CENELEC web site. URL https://www.cenelec.eu/.Google Scholar80European Parliament (2016). Regulation (eu) 2016/679 of the european parliament and of the council of 27 april 2016 on the protection of natural persons with regard to the processing of personal data and on the free movement of such data, and repealing directive 95/46/ec (general data protection regulation). URL https://eur-lex.europa.eu/legal-content/EN/TXT/?uri=CELEX:32016R0679.Google Scholar81European Union Aviation Safety Agency. EASA web site. URL https://www.easa.europa.eu/.Google Scholar82FAA (November 2010). Qantas flight 32, airbus a380-842, vh-oqa. Online: https://lessonslearned.faa.gov/ll_main.cfm?TabID=1&LLID=83.Google Scholar83Falcone, Y., Krstic, S., Reger, G., & Traytel, D. (2018). A taxonomy for classifying runtime verification tools. In C. Colombo, & M. Leucker (Eds.), Runtime Verification - 18th International Conference, RV 2018, Limassol, Cyprus, November 10-13, 2018, Proceedings, volume 11237 of Lecture Notes in Computer Science (pp. 241–262). Springer.CrossrefGoogle Scholar84Farrell, M., Luckcuck, M., & Fisher, M. (2018). Robotics and Integrated Formal Methods: Necessity Meets Opportunity. In Proceedings of 14th International Conference on Integrated Formal Methods (IFM’18), volume LNCS 11023 (pp. 161–171). Springer.CrossrefGoogle Scholar85Federal Aviation Administration. FAA web site. URL https://www.faa.gov/.Google Scholar86Federal Aviation Administration (2004). Title 14 code of Federal Regulations Part 145 approved training program – research and recommendations. URL https://www.faa.gov/about/initiatives/maintenance_hf/library/documents/media/human_factors_maintenance/ar04-36.pdf.Google Scholar87Federal Aviation Administration (2016). Part 107: Operation and certification of small unmanned aircraft systems. URL https://www.faa.gov/uas/media/RIN_2120-AJ60_Clean_Signed.pdf.Google Scholar88Ferrando, A., Ancona, D., & Mascardi, V. (2017). Decentralizing MAS monitoring with DecAMon. In AAMAS (pp. 239–248). ACM.Google Scholar89Ferrando, A., Dennis, L. A., Ancona, D., Fisher, M., & Mascardi, V. (2018). Recognising Assumption Violations in Autonomous Systems Verification. In AAMAS (pp. 1933–1935). International Foundation for Autonomous Agents and Multiagent Systems Richland, SC, USA / ACM.Google Scholar90Ferrando, A., Dennis, L. A., Ancona, D., Fisher, M., & Mascardi, V. (2018). Verifying and Validating Autonomous Systems: Towards an Integrated Approach. In RV, volume 11237 of Lecture Notes in Computer Science (pp. 263–281). Springer.Google Scholar91FINRA. Algorithmic trading: Rules. https://www.finra.org/rules-guidance/key-topics/algorithmic-trading#rules. Accessed 2019-10-15.Google Scholar92Fisher M, Dennis LA, and Webster MP Verifying autonomous systems Communications of the ACM 2013 56 9 84-93CrossrefGoogle Scholar93Franchetti F, Low TM, Mitsch S, Mendoza JP, Gui L, Phaosawasdi A, Padua D, Kar S, Moura JM, Franusich M, et al. High-assurance spiral: End-to-end guarantees for robot and car control IEEE Control Systems Magazine 2017 37 2 82-103CrossrefGoogle Scholar94Frauenberger C and Purgathofer P Ways of thinking in informatics Communications of the ACM 2019 62 7 58-64CrossrefGoogle Scholar95FreeBSD. lint – a c program verifier. URL https://www.freebsd.org/cgi/man.cgi?query=lint&apropos=0&sektion=0&manpath=FreeBSD+11.1-RELEASE&arch=default&format=html.Google Scholar96Fulton, N., Ji, R., Platzer, A., et al. (2016). Proving autonomous vehicle and advanced driver assistance systems safety: final research report.Google Scholar97Galdino, A. L., Munoz, C., & Ayala-Rincón, M. (2007). Formal verification of an optimal air traffic conflict resolution and recovery algorithm. In International Workshop on Logic, Language, Information, and Computation (pp. 177–188). Springer, Berline, Heidelberg.Google Scholar98Gario, M., Cimatti, A., Mattarei, C., Tonetta, S., & Rozier, K. Y. (July 2016). Model checking at scale: Automated air traffic control design space exploration. In Proceedings of 28th International Conference on Computer Aided Verification (CAV 2016), volume 9780 of LNCS (pp. 3–22) Toronto, ON, Canada. Springer.CrossrefGoogle Scholar99Geist, J., Rozier, K. Y., & Schumann, J. (September 2014). Runtime observer pairs and bayesian network reasoners On-board FPGAs: Flight-certifiable system health management for embedded systems. In Proceedings of the 14th International Conference on Runtime Verification (RV14), volume 8734 (pp. 215–230). Springer-Verlag.Google Scholar100Ghosh, S., Elenius, D., Li, W., Lincoln, P., Shankar, N., & Steiner, W. (2016). ARSENAL: automatic requirements specification extraction from natural language. In S. Rayadurgam, & O. Tkachuk (eds.), NASA Formal Methods - 8th International Symposium, NFM 2016, Minneapolis, MN, USA, June 7-9, 2016, Proceedings, volume 9690 of Lecture Notes in Computer Science (pp. 41–46). Springer.CrossrefGoogle Scholar101Gunkel D and Bryson JJ Introduction to the special issue on machine morality: The machine as moral agent and patient Philosophy & Technology 2014 27 1 5-8CrossrefGoogle Scholar102Havelund, K., & Reger, G. (2017). Runtime verification logics a language design perspective. In Models, Algorithms, Logics and Tools - Essays Dedicated to Kim Guldstrand Larsen on the Occasion of His 60th Birthday, volume 10460 of Lecture Notes in Computer Science (pp. 310–338). Springer, New yorkGoogle Scholar103Heitmeyer CL On the role of formal methods in software certification: An experience report Electronic Notes on Theoretical Computer Science 2009 238 4 3-9CrossrefGoogle Scholar104Heitmeyer CL, Archer M, Leonard EI, and McLean J Applying formal methods to a certifiably secure software system IEEE Trans. Software Eng. 2008 34 1 82-98CrossrefGoogle Scholar105Helle, P., Schamai, W., & Strobel, C. (2016). Testing of autonomous systems – challenges and current state-of-the-art. In INCOSE International Symposium, volume 26-1 (pp. 571–584). Wiley Online Library.CrossrefGoogle Scholar106Henzinger TA, Ho P-H, and Wong-Toi H HYTECH: A model checker for hybrid systems International Journal on Software Tools for Technology Transfer 1997 1 1–2 110-122CrossrefGoogle Scholar107Hoare CAR An axiomatic basis for computer programming Commun. ACM 1969 12 10 576-580 ISSN 0001-0782CrossrefGoogle Scholar108Hodgkins, K. (5 Oct. 2011). Apple’s Knowledge Navigator, Siri and the iPhone 4S. Engadget.Google Scholar109Holzmann GJ The Spin Model Checker: Primer and Reference Manual 2003 Boston Addison-Wesley ISBN 0-321-22862-6Google Scholar110Huhns MN and Singh MP Agents on the web: Personal assistants IEEE Internet Computing 1998 2 5 90-92CrossrefGoogle Scholar111Industry Research (2019). Software testing services market by product, end-users, and geography – global forecast and analysis 2019-2023. URL https://www.industryresearch.co/software-testing-services-market-by-product-end-users-and-geography-global-forecast-and-analysis-2019-2023-14620379.Google Scholar112Institute of Electrical and Electronics Engineers. The IEEE global initiative on ethics of autonomous and intelligent systems, a. URL https://standards.ieee.org/industry-connections/ec/autonomous-systems.html.Google Scholar113Institute of Electrical and Electronics Engineers. IEEE web site, b. URL https://www.ieee.org/.Google Scholar114Institute of Electrical and Electronics Engineers (2006). IEEE 1512-2006 – standard for common incident management message sets for use by emergency management centers. URL https://standards.ieee.org/standard/1512-2006.html.Google Scholar115Institute of Electrical and Electronics Engineers (2015). IEEE standard ontologies for robotics and automation. URL https://ieeexplore.ieee.org/document/7084073.Google Scholar116Institute of Electrical and Electronics Engineers (2016). P2020 – standard for automotive system image quality. URL https://standards.ieee.org/project/2020.html.Google Scholar117Institute of Electrical and Electronics Engineers (2016). P7000 – model process for addressing ethical concerns during system design. URL https://standards.ieee.org/project/7000.html.Google Scholar118Institute of Electrical and Electronics Engineers (2016c). P7001 – transparency of autonomous systems. URL https://standards.ieee.org/project/7001.html.Google Scholar119Institute of Electrical and Electronics Engineers (2016d). P7002 – data privacy process. URL https://standards.ieee.org/project/7002.html.Google Scholar120Institute of Electrical and Electronics Engineers (2017). P7003 – algorithmic bias considerations. URL https://standards.ieee.org/project/7003.html.Google Scholar121Institute of Electrical and Electronics Engineers (2017). P7006 – standard for personal data artificial intelligence (AI) agent. URL https://standards.ieee.org/project/7006.html.Google Scholar122Institute of Electrical and Electronics Engineers (2017c). P7007 – ontological standard for ethically driven robotics and automation systems. URL https://standards.ieee.org/project/7007.html.Google Scholar123Institute of Electrical and Electronics Engineers (2017d). P7008 – standard for ethically driven nudging for robotic, intelligent and autonomous systems. URL https://standards.ieee.org/project/7008.html.Google Scholar124Institute of Electrical and Electronics Engineers (2017e). P7009 – standard for fail-safe design of autonomous and semi-autonomous systems. URL https://standards.ieee.org/project/7009.html.Google Scholar125Institute of Electrical and Electronics Engineers – Robotics and Automation Society (2019). IEEE-RAS technical committee for verification of autonomous systems. URL https://www.ieee-ras.org/verification-of-autonomous-systems.Google Scholar126International Association of Public Transport – L’Union internationale des transports publics. UITP web site. URL https://www.uitp.org/.Google Scholar127International Civil Aviation Organization (2001). Annex 11 to the convention on international civil aviation, thirteenth edition. URL https://store.icao.int/products/annex-11-air-traffic-services.Google Scholar128International Electrotechnical Commission. IEC TC 107 – process management for avionics, a. URL https://www.iec.ch/dyn/www/f?p=103:7:0::::FSP_ORG_ID:1304.Google Scholar129International Electrotechnical Commission. IEC TC 97 – electrical installations for lighting and beaconing of aerodromes, b. URL https://www.iec.ch/dyn/www/f?p=103:7:0::::FSP_ORG_ID:1294.Google Scholar130International Electrotechnical Commission. IEC web site, c. URL https://www.iec.ch/.Google Scholar131International Electrotechnical Commission (2002). IEC 62278 – railway applications - specification and demonstration of reliability, availability, maintainability and safety (RAMS). URL https://webstore.iec.ch/publication/6747.Google Scholar132International Electrotechnical Commission (2010). Functional safety and IEC 61508. URL https://www.iec.ch/functionalsafety/.Google Scholar133International Electrotechnical Commission (2010). IEC 62278-3 – railway applications - specification and demonstration of reliability, availability, maintainability and safety (RAMS) - Part 3: Guide to the application of IEC 62278 for rolling stock RAM. URL https://webstore.iec.ch/publication/6746.Google Scholar134International Electrotechnical Commission (2016). IEC 62278-4 – railway applications - specification and demonstration of reliability, availability, maintainability and safety (RAMS) - Part 4: RAM risk and RAM life cycle aspects. URL https://webstore.iec.ch/publication/29621.Google Scholar135International Electrotechnical Commission (2017). IEC TC 69 – electric road vehicles and electric industrial trucks. URL https://www.iec.ch/dyn/www/f?p=103:7:0::::FSP_ORG_ID:1255.Google Scholar136International Electrotechnical Commission (2017). IEC TC 9 – electrical equipment and systems for railways. URL https://www.iec.ch/dyn/www/f?p=103:7:0::::FSP_ORG_ID,FSP_LANG_ID:1248,25.Google Scholar137International Electrotechnical Commission (2017c). IEC TR 60601-4-1 – medical electrical equipment – part 4-1: Guidance and interpretation - medical electrical equipment and medical electrical systems employing a degree of autonomy. URL https://webstore.iec.ch/publication/29312.Google Scholar138International Electrotechnical Commission (2019). IEC 63243 ED1 – interoperability and safety of dynamic wireless power transfer (WPT) for electric vehicles. URL https://www.iec.ch/dyn/www/f?p=103:38:1864379252239.Google Scholar139International Organization for Standardization. ISO web site. URL https://www.iso.org/.Google Scholar140International Organization for Standardization (1947). ISO/TC 20 – Aircraft and space vehicles. URL https://www.iso.org/committee/46484.html.Google Scholar141International Organization for Standardization (1951). ISO/TC 76 – transfusion, infusion and injection, and blood processing equipment for medical and pharmaceutical use. URL https://www.iso.org/committee/50044.html.Google Scholar142International Organization for Standardization (1988). ISO/TC 194 – biological and clinical evaluation of medical devices. URL https://www.iso.org/committee/54508.html.Google Scholar143International Organization for Standardization (1994). ISO/TC 210 – quality management and corresponding general aspects for medical devices. URL https://www.iso.org/committee/54892.html.Google Scholar144International Organization for Standardization (1998). ISO/TC 215 – health informatics. URL https://www.iso.org/committee/54960.html.Google Scholar145International Organization for Standardization (2012). ISO 21500 – guidance on project management. URL https://www.iso.org/standard/50003.html.Google Scholar146International Organization for Standardization (2012). ISO/TC 269 – railway applications. URL https://www.iso.org/committee/661629.html.Google Scholar147International Organization for Standardization (2014). ISO 13482 – robots and robotic devices – safety requirements for personal care robots. URL https://www.iso.org/standard/53820.html.Google Scholar148International Organization for Standardization (2015). ISO/TC 299 – robotics. URL https://www.iso.org/committee/5915511.html.Google Scholar149International Organization for Standardization (2016). ISO and road vehicles. URL https://www.iso.org/publication/PUB100292.html.Google Scholar150International Organization for Standardization (2018). ISO 21245 – railway applications – railway project planning process – guidance on railway project planning. URL https://www.iso.org/standard/74012.html.Google Scholar151International Organization for Standardization (2018). ISO 26262-1 – road vehicles – functional safety. URL https://www.iso.org/standard/68383.html.Google Scholar152International Organization for Standardization (2019). ISO and health. URL https://www.iso.org/publication/PUB100343.html.Google Scholar153International Organization for Standardization (ISO) (2014). ISO 13482 – robots and robotic devices — safety requirements for personal care robots. URL https://www.iso.org/standard/53820.html.Google Scholar154International Organization for Standardization (ISO) (2016). ISO/TS 15066 – robots and robotic devices – collaborative robots. URL https://www.iso.org/standard/62996.html.Google Scholar155International Organization for Standardization (ISO) (2017). ISO/TR 20218-2 – robotics – safety design for industrial robot systems – part 2: Manual load/unload stations. URL https://www.iso.org/standard/70584.html.Google Scholar156International Organization for Standardization (ISO) (2017). ISO/TR 23482-2 – robotics – application of ISO 13482 – part 2: Application guidelines. URL https://www.iso.org/standard/71627.html.Google Scholar157International Organization for Standardization (ISO) (2018). ISO/TR 20218-1 – robotics – safety design for industrial robot systems – part 1: End-effectors. URL https://www.iso.org/standard/69488.html.Google Scholar158International union of railways – Union Internationale des Chemins de fer. UIC web site. URL https://uic.org/.Google Scholar159Jasim, O. A., & Veres, S. M. (Oct 2017). Towards formal proofs of feedback control theory. In Proc. 21st International Conference on System Theory, Control and Computing (ICSTCC) (pp. 43–48).CrossrefGoogle Scholar160Jennings NR, Sycara KP, and Wooldridge M A roadmap of agent research and development Autonomous Agents and Multi-Agent Systems 1998 1 1 7-38CrossrefGoogle Scholar161Jovinelly J and Netelkos J The crafts and culture of a medieval guild 2006 New York, NY Rosen PublishingGoogle Scholar162Julius A and Pappas G Approximations of stochastic hybrid systems IEEE Transactions on Automatic Control 2009 54 6 1193-1203CrossrefGoogle Scholar163Kempa, B., Zhang, P., Jones, P. H., Zambreno, J., & Rozier, K. Y. (September 2020). Embedding Online Runtime Verification for Fault Disambiguation on Robonaut2. In Proceedings of the 18th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS), volume TBD of Lecture Notes in Computer Science (LNCS), page TBD, Vienna, Austria: Springer. : TBD. URL http://research.temporallogic.org/papers/KZJZR20.pdf.Google Scholar164Kepuska, V., & Bohouta, G. (2018). Next-generation of virtual personal assistants (microsoft cortana, apple siri, amazon alexa and google home). In 2018 IEEE 8th Annual Computing and Communication Workshop and Conference (CCWC) (pp. 99–103). IEEE.Google Scholar165Khan SG, Herrmann G, Pipe AG, Melhuish C, and Spiers A Safe adaptive compliance control of a humanoid robotic arm with anti-windup compensation and posture Control Int. J. Social Robotics 2010 2 3 305-319CrossrefGoogle Scholar166Knight, J. C. (2002). Safety critical systems: challenges and directions. In W. Tracz, M. Young, & J. Magee (Eds.), Proceedings of the 24th International Conference on Software Engineering, ICSE 2002, 19-25 May 2002, Orlando, Florida, USA (pp. 547–550). ACM.CrossrefGoogle Scholar167Kohlberg, L. (1969). Stage and sequence: The cognitive-developmental approach to socialization. In D. Goslin (Ed.), Handbook of Socialization Theory and Research (pp. 347–480). Rand McNally.Google Scholar168Kohlberg L Essays on Moral Development. Volume I: The philosophy of moral development 1981 New York Harper & RowGoogle Scholar169Kohlberg L Essays on Moral Development. Volume II: The psychology of moral development: the nature and validity of moral stages 1984 NewYork Harper & RowGoogle Scholar170Kong, J., & Lomuscio, A. (2017). Symbolic model checking multi-agent systems against CTL*K specifications. In K. Larson, M. Winikoff, S. Das, & E. H. Durfee (Eds.), Proceedings of the 16th Conference on Autonomous Agents and MultiAgent Systems, AAMAS 2017, São Paulo, Brazil, May 8-12, 2017 (pp. 114–122). ACM. URL http://dl.acm.org/citation.cfm?id=3091147.Google Scholar171Kong, J., & Lomuscio, A. (2018). Model checking multi-agent systems against LDLK specifications on finite traces. In E. André, S. Koenig, M. Dastani, & G. Sukthankar (Eds.), Proceedings of the 17th International Conference on Autonomous Agents and MultiAgent Systems, AAMAS 2018, Stockholm, Sweden, July 10-15, 2018 (pp. 166–174). International Foundation for Autonomous Agents and Multiagent Systems Richland, SC, USA / ACM. URL http://dl.acm.org/citation.cfm?id=3237414.Google Scholar172Kowalski, R. A., & Sadri, F. (1996). Towards a unified agent architecture that combines rationality with reactivity. In D. Pedreschi, & C. Zaniolo (Eds.), Logic in Databases, International Workshop LID’96, San Miniato, Italy, July 1-2, 1996, Proceedings, volume 1154 of Lecture Notes in Computer Science (pp. 137–149). Springer.CrossrefGoogle Scholar173Leveson NG and Turner CS An investigation of the Therac-25 accidents Computer 1993 26 7 18-41 ISSN 1558-0814CrossrefGoogle Scholar174Levine, D. M. (23May 2013). A day in the quiet life of a NYSE floor trader. Fortune. URL https://fortune.com/2013/05/29/a-day-in-the-quiet-life-of-a-nyse-floor-trader/.Google Scholar175Li, J., & Rozier, K. Y. (November 2018). MLTL Benchmark Generation via Formula Progression. In Proceedings of the 18th International Conference on Runtime Verification (RV18), Limassol, Cyprus. Springer-Verlag.Google Scholar176Li, J., Vardi, M., & Rozier, K. Y. (July 2019). Satisfiability checking for mission-time LTL. In Proceedings of 31st International Conference on Computer Aided Verification (CAV’19), LNCS. Springer.CrossrefGoogle Scholar177Lomuscio, A., & Raimondi, F. (2006). Model checking knowledge, strategies, and games in multi-agent systems. In H. Nakashima, M. P. Wellman, G. Weiss, & P. Stone (Eds.), 5th International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS 2006), Hakodate, Japan, May 8-12, 2006 (pp. 161–168). ACM.CrossrefGoogle Scholar178Luckcuck M, Farrell M, Dennis L, Dixon C, and Fisher M Formal specification and verification of autonomous robotic systems: A survey ACM Computing Surveys 2019 52 5 100:1-100:41CrossrefGoogle Scholar179Luckow KS and Păsăreanu CS Symbolic pathfinder v7 ACM SIGSOFT Software Engineering Notes 2014 39 1 1-5CrossrefGoogle Scholar180Maggi, F. M., Montali, M., Westergaard, M., & van der Aalst, W. M. P. (2011). Monitoring business constraints with linear temporal logic: An approach based on colored automata. In S. Rinderle-Ma, F. Toumani, & K. Wolf (Eds.), Proceedings of 9th International Conference on Business Process Management (BPM’11), volume 6896 of LNCS (pp. 132–147). Springer.CrossrefGoogle Scholar181Marr, B. (2017). The biggest challenges facing artificial intelligence (AI) in business and society. Forbes. URL https://www.forbes.com/sites/bernardmarr/2017/07/13/the-biggest-challenges-facing-artificial-intelligence-ai-in-business-and-society/.Google Scholar182MathWorks. Polyspace bug finder. URL https://in.mathworks.com/products/polyspace-bug-finder.html.Google Scholar183Mattarei, C., Cimatti, A., Gario, M., Tonetta, S., Rozier, K. Y., & (September 2015). Comparing different functional allocations in automated air traffic control design. In Proceedings of Formal Methods in Computer-Aided Design (FMCAD,. (2015). Austin, Texas, U.S.A, IEEE/ACM.Google Scholar184Matthias A Robot lies in health care: when is deception morally permissible? Kennedy Institute of Ethics Journal 2011 25 2 279-301Google Scholar185McMillan, K. L. (1999). The SMV language. Cadence Berkeley Labs (pp. 1–49).Google Scholar186Merriam-Webster Dictionary (2020). Definition of ‘reliable’. URL https://www.merriam-webster.com/dictionary/reliable.Google Scholar187Moosbrugger, P., Rozier, K. Y., & Schumann, J. (April 2017). R2U2: Monitoring and Diagnosis of Security Threats for Unmanned Aerial Systems. In Formal Methods in System Design (FMSD) (pp. 1–31). Springer-Verlag.CrossrefGoogle Scholar188Munoz, C., Narkawicz, A., & Chamberlain, J. (2013). A TCAS-II resolution advisory detection algorithm. In AIAA Guidance, Navigation, and Control (GNC) Conference, page 4622.Google Scholar189Muñoz, C., Narkawicz, A., Hagen, G., Upchurch, J., Dutle, A., Consiglio, M., & Chamberlain, J. (2015). Daidalus: detect and avoid alerting logic for unmanned systems. In 2015 IEEE/AIAA 34th Digital Avionics Systems Conference (DASC) (pp. 5A1–1). IEEE.Google Scholar190Musuvathi M, Engler DR, et al. Model checking large network protocol implementations NSDI 2004 4 12-12Google Scholar191Negroponte N Being Digital 1996 New York, NY, USA Random House ISBN 0-679-43919-6Google Scholar192Nguyen, C. D., Perini, A., Bernon, C., Pavón, J., & Thangarajah, J. (2009). Testing in multi-agent systems. In M. P. Gleizes, & J. J. Gómez-Sanz (Eds.), Agent-Oriented Software Engineering X - 10th International Workshop, AOSE. (2009). Budapest, Hungary, May 11–12, 2009, Revised Selected Papers (Vol. 6038, pp. 180–190)., Lecture Notes in Computer Science New york: Springer.Google Scholar193Patchett C, Jump M, and Fisher M Institution of engineering and technology:in engineering and technology reference Safety and Certification of Unmanned Air Systems 2015CrossrefGoogle Scholar194Paulson LC A Generic Theorem Prover 1994 New york SpringerGoogle Scholar195Penczek, W., & Lomuscio, A. (2003). Verifying epistemic properties of multi-agent systems via bounded model checking. In The Second International Joint Conference on Autonomous Agents & Multiagent Systems, AAMAS 2003, July 14-18, 2003, Melbourne, Victoria, Australia, Proceedings (pp. 209–216). ACM.CrossrefGoogle Scholar196Perez, I., Dedden, F., & Goodloe, A. (2020). Copilot 3. Technical Report NASA/TM-2020-220587, National Aeronautics and Space Administration.Google Scholar197Pietrantuono, R., & Russo, S. (2018). Robotics software engineering and certification: Issues and challenges. In S. Ghosh, R. Natella, B. Cukic, R. Poston, & N. Laranjeiro (Eds.), 2018 IEEE International Symposium on Software Reliability Engineering Workshops, ISSRE Workshops, Memphis, TN, USA, October 15-18, 2018 (pp. 308–312). IEEE Computer Society.CrossrefGoogle Scholar198Pietronudo, E. (2018). ”Japanese women’s language” and artificial intelligence: Azuma Hikari, gender stereotypes and gender norms. http://hdl.handle.net/10579/12791.Google Scholar199Pike, L. (2007). Modeling time-triggered protocols and verifying their real-time schedules. In Formal Methods in Computer Aided Design (FMCAD’07) (pp. 231–238). IEEE.Google Scholar200platoon. Current State of EU Legislation- Cooperative Dynamic Formation of Platoons for Safe and Energy-optimized Goods Transportation. URL http://www.companion-project.eu/wp-content/uploads/COMPANION-D2.2-Current-state-of-the-EU-legislation.pdf.Google Scholar201Platzer A Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics 2010 Heidelberg Springer ISBN 978-3-642-14508-7CrossrefGoogle Scholar202Platzer, A., & Quesel, J.-D. (2008). KeyMaera: A Hybrid Theorem Prover for Hybrid Systems. In A. Armando, P. Baumgartner, & G. Dowek (Eds.), Proceedings of 4th International Joint Conference on Automated Reasoning (IJCAR), volume 5195 of LNCS (pp. 171–178). Springer.Google Scholar203Poore JH, Mills HD, and Mutchler D Planning and certifying software system reliability IEEE Software 1993 10 1 88-99CrossrefGoogle Scholar204Quirchmayr, T. (2018). Retrospective semi-automated software feature extraction from natural language user manuals. PhD thesis, University of Heidelberg, Germany. URL http://www.ub.uni-heidelberg.de/archiv/25322.Google Scholar205Radio Technical Commission for Aeronautics. RTCA web site. URL https://www.rtca.org/.Google Scholar206Radio Technical Commission for Aeronautics (1992). DO-178B – software considerations in airborne systems and equipment certification. URL https://www.rtca.org/content/standards-guidance-materials.Google Scholar207Radio Technical Commission for Aeronautics (1992). DO-278A – software integrity assurance considerations for communication, navigation, surveillance and air traffic management (CNS/ATM) systems. URL https://www.rtca.org/content/standards-guidance-materials.Google Scholar208Radio Technical Commission for Aeronautics (2000). DO-254 – design assurance guidance for airborne electronic hardware. URL https://www.rtca.org/content/standards-guidance-materials.Google Scholar209Radio Technical Commission for Aeronautics (2011). DO-333 – formal methods supplement to DO-178C and DO-278A. URL https://www.rtca.org/content/standards-guidance-materials.Google Scholar210Radio Technical Commission for Aeronautics (2012). DO-178C/ED-12C – software considerations in airborne systems and equipment certification. URL https://www.rtca.org/content/standards-guidance-materials.Google Scholar211Raman, V., Lignos, C., Finucane, C., Lee, K. C., Marcus, M. P., & Kress-Gazit, H. (2013). Sorry dave, i’m afraid i can’t do that: Explaining unachievable robot tasks using natural language. volume 2. Citeseer.Google Scholar212Ramesh B and Jarke M Toward reference models for requirements traceability IEEE Transactions on Software Engineering 2001 27 1 58-93CrossrefGoogle Scholar213Reinbacher, T., Rozier, K. Y., & Schumann, J. (2014). Temporal-logic based runtime observer pairs for system health management of real-time systems. In Proceedings of 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’14), volume LNCS 8413 (pp. 357–372). Springer.CrossrefGoogle Scholar214Rinehart, D. J., Knight, J. C., & Rowanhill, J. (2017). Understanding what it means for assurance cases to “work”. Technical report, NASA. NASA/CR–2017-219582.Google Scholar215Rosu G On safety properties and their monitoring Science Annals of Computer Science. 2012 22 2 327-365CrossrefGoogle Scholar216Rozier K and Vardi M LTL satisfiability checking International Journal on Software Tools for Technology Transfer (STTT) 2010 12 2 123-137CrossrefGoogle Scholar217Rozier KY Linear Temporal Logic Symbolic Model Checking Computer Science Review Journal 2011 5 2 163-203CrossrefGoogle Scholar218Rozier, K. Y. (2016). Specification: The biggest bottleneck in formal methods and autonomy. In Proceedings of 8th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE’16), volume LNCS 9971 (pp. 1–19). Springer.CrossrefGoogle Scholar219Rozier, K. Y. (April 2019). From simulation to runtime verification and back: Connecting single-run verification techniques. In Proceedings of the Spring Simulation Conference (SpringSim) (pp. 1–10), Tucson, AZ, USA. Society for Modeling & Simulation International. https://dl.acm.org/doi/10.5555/3338027.3338054.Google Scholar220Rozier, K. Y., & Schumann, J. (2017). R2U2: Tool overview. In Proceedings of International Workshop on Competitions, Usability, Benchmarks, Evaluation, and Standardisation for Runtime Verification Tools (RV-CUBES) (pp. 138–156).CrossrefGoogle Scholar221SAE International (2018). SAE J3016\_201806 – taxonomy and definitions for terms related to driving automation systems for on-road motor vehicles. URL https://www.sae.org/standards/content/j3016_201806/.Google Scholar222Salem, M., Lakatos, G., Amirabdollahian, F., & Dautenhahn, K. (2015). Would you trust a (faulty) robot?: Effects of error, task type and personality on human-robot cooperation and trust. In Proceedings of 10th ACM/IEEE International Conference on Human-Robot Interaction, HRI 2015, Portland, OR, USA, March 2-5, 2015, (pp. 141–148). ACM.Google Scholar223Salem, M., Lakatos, G., Amirabdollahian, F., & Dautenhahn, K. (2015). Towards Safe and Trustworthy Social Robots: Ethical Challenges and Practical Issues. In Proc. 7th International Conference on Social Robotics (ICSR), volume 9388 of LNCS (pp. 584–593). Springer.Google Scholar224Sartre. SARTRE project. URL https://cordis.europa.eu/project/rcn/92577/brief/en.Google Scholar225Schlatow, J., Möstl, M., Ernst, R., Nolte, M., Jatzkowski, I., Maurer, M., Herber, C., & Herkersdorf, A. (2017). Self-awareness in autonomous automotive systems. In D. Atienza, & G. D. Natale (Eds.), Design, Automation & Test in Europe Conference & Exhibition, DATE 2017, Lausanne, Switzerland, March 27-31, 2017 (pp. 1050–1055). IEEE.CrossrefGoogle Scholar226Schumann, J., Moosbrugger, P., & Rozier, K. Y. (September 2016). Runtime Analysis with R2U2: A Tool Exhibition Report. In Proceedings of the 16th International Conference on Runtime Verification (RV16). Madrid, Spain: Springer-Verlag.Google Scholar227Scrapper, C., Balakirsky, S., & Messina, E. (2006). MOAST and USARSim: a combined framework for the development and testing of autonomous systems. In Unmanned Systems Technology VIII, volume 6230, page 62301T. International Society for Optics and Photonics.Google Scholar228SCSC - The Safety-Critical Systems Club. SCSC – goal structuring notation community standard (version 2). URL https://scsc.uk/scsc-141B.Google Scholar229Shankar, N. (2008). Trust and automation in verification tools. In Automated Technology for Verification and Analysis, 6th International Symposium, ATVA 2008, Seoul, Korea, October 20-23, 2008. Proceedings (pp. 4–17).CrossrefGoogle Scholar230Sharkey, A., & Wood, N. (2014). The paro seal robot: demeaning or enabling. In Proceedings of AISB, volume 36.Google Scholar231Stout D Stone toolmaking and the evolution of human culture and cognition Philosophical Transactions of the Royal Society B: Biological Sciences 2011 366 1567 1050-1059CrossrefGoogle Scholar232Swaroop, D. (1997). String stability of interconnected systems: An application to platooning in automated highway systems. California Partners for Advanced Transit and Highways (PATH).Google Scholar233Tabakov D, Rozier KY, and Vardi MY Optimized temporal monitors for SystemC Formal Methods in System Design 2012 41 3 236-268CrossrefGoogle Scholar234The European Parliament (2018). Regulation (EU) 2018/1139 of the European Parliament and of the Council of 4 July 2018 on common rules in the field of civil aviation and establishing a European Union Aviation Safety Agency, and amending Regulations (EC) No 2111/2005, (EC) No 1008/2008, (EU) No 996/2010, (EU) No 376/2014 and Directives 2014/30/EU and 2014/53/EU of the European Parliament and of the Council, and repealing Regulations (EC) No 552/2004 and (EC) No 216/2008 of the European Parliament and of the Council and Council Regulation (EEC) No 3922/91 (Text with EEA relevance). URL https://eur-lex.europa.eu/legal-content/EN/TXT/?uri=CELEX:32018R1139.Google Scholar235The IEEE Global Initiative on Ethics of Autonomous and Intelligent Systems, (Ed.) (2019). Ethically Aligned Design: A Vision for Prioritizing Human Well-being with Autonomous and Intelligent Systems. IEEE. URL https://standards.ieee.org/content/ieee-standards/en/industry-connections/ec/ autonomous-systems.html.Google Scholar236The Software Testing Help (STH) Blog (2019). Top 40 static code analysis tools (best source code analysis tools). URL https://www.softwaretestinghelp.com/tools/top-40-static-code-analysis-tools/.Google Scholar237Tolmeijer, S., Weiss, A., Hanheide, M., Lindner, F., Powers, T. M., Dixon, C., & Tielman, M. L. (2020). Taxonomy of trust-relevant failures and mitigation strategies. In Proceedings of the 2020 ACM/IEEE International Conference on Human-Robot Interaction (HRI) (pp. 3-12). Association for Computing Machinery.CrossrefGoogle Scholar238Tomayko, J. E. (2003). The story of self-repairing flight control systems. In C. Gelzer (Ed.), Dryden Historical Study No. 1. : NASA Dryden Flight Research Center.Google Scholar239Torens C, Adolf F, and Goormann L Certification and software verification considerations for autonomous unmanned aircraft Journal of Aerospace Information System. 2014 11 10 649-664CrossrefGoogle Scholar240Tuncali CE, Fainekos G, Prokhorov D, Ito H, and Kapinski J Requirements-driven test generation for autonomous vehicles with machine learning components IEEE Transactions on Intelligent Vehicles 2019 5 2 265-280CrossrefGoogle Scholar241U.S. Department of Transportation (2016). Federal automated vehicles policy. URL https://www.transportation.gov/AV/federal-automated-vehicles-policy-september-2016.Google Scholar242van der Aalst, W. M. P. (2002). Making work flow: On the application of petri nets to business process management. In J. Esparza, & C. Lakos (Eds.), Proceedings of 23rd International Conference on Applications and Theory of Petri Nets (ICATPN’02), volume 2360 of Lecture Notes in Computer Science (pp. 1–22). Springer.CrossrefGoogle Scholar243van der Aalst WMP Process Mining - Discovery, Conformance and Enhancement of Business Processes 2011 New york Springer ISBN 978-3-642-19344-6CrossrefGoogle Scholar244Visser W, Havelund K, Brat GP, Park S, and Lerda F Model checking programs Automated Software Engineering 2003 10 2 203-232CrossrefGoogle Scholar245Wada K, Shibata T, Asada T, and Musha T Robot therapy for prevention of dementia at home Journal of Robotics and Mechatronics 2007 19 6 691CrossrefGoogle Scholar246Webster M, Dixon C, Fisher M, Salem M, Saunders J, Koay K, Dautenhahn K, and Saez-Pons J Toward reliable autonomous robotic assistants through formal verification: A Case Study IEEE Transactions on Human-Machine Systems 2016 46 2 186-196 ISSN 2168-2291CrossrefGoogle Scholar247Webster MP, Cameron N, Fisher M, and Jump M Generating certification evidence for autonomous unmanned aircraft using model checking and simulation Journal of Aerospace Information System. 2014 11 5 258-279CrossrefGoogle Scholar248Whitehurst, R. A., & Lunt, T. F. (1989). The sea view verification. In Proceedings of 2nd IEEE Computer Security Foundations Workshop (CSFW’89) (pp. 125–132). IEEE Computer Society.CrossrefGoogle Scholar249Winfield AFT, Michael K, Pitt J, and Evers V Machine ethics: The design and governance of ethical AI and autonomous systems Proceedings of the IEEE 2019 107 3 509-517CrossrefGoogle Scholar250Winikoff M BDI agent testability revisited Journal of Autonomous Agents and Multi-Agent Systems (JAAMAS) 2017 31 5 1094-1132CrossrefGoogle Scholar251Winikoff M and Cranefield S On the testability of BDI agent systems Journal of Artificial Intelligence Research 2014 51 71-131CrossrefGoogle Scholar252Wohlin C and Runeson P Certification of software components IEEE Trans. Software Eng. 1994 20 6 494-499CrossrefGoogle Scholar253Woodman R, Winfield AFT, Harper CJ, and Fraser M Building safer robots: Safety driven control International Journal of Robotics Research 2012 31 13 1603-1626CrossrefGoogle Scholar254Wooldridge, M., & Jennings, N. R. (Eds.). (1995). Intelligent Agents, ECAI-94 Workshop on Agent Theories, Architectures, and Languages, Amsterdam, The Netherlands, August 8–9, 1994, Proceedings, volume LNCS 890. Springer.CrossrefGoogle Scholar255Wooldridge M and Jennings NR Intelligent agents: theory and practice Knowledge Eng. Review 1995 10 2 115-152CrossrefGoogle Scholar256Working Party on Automated/autonomous and Connected Vehicles, Economic Commission for Europe (2020). Proposal for a new UN regulation on uniform provisions concerning the approval of vehicles with regards to Automated Lane Keeping System. URL https://undocs.org/ECE/TRANS/WP.29/2020/81.Google Scholar257Xiao, L., Lewis, P. H., & Dasmahapatra, S. (2008). Secure Interaction Models for the HealthAgents System. In Proc. 27th International Conference on Computer Safety, Reliability, and Security (SAFECOMP), volume 5219 of LNCS (pp. 167–180). Springer. ISBN 978-3-540-87697-7.Google Scholar258Yang, M., & Chow, K.-P. (2015). An information extraction framework for digital forensic investigations. In IFIP International Conference on Digital Forensics, (pp. 61–76). Springer.Google Scholar259Yorke-Smith, N., Saadati, S., Myers, K. L., & Morley, D. N. (2009). Like an intuitive and courteous butler: A proactive personal agent for task management. In Proceedings of 8th International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS’09) (pp. 337–344).Google Scholar260Yu H, Lin C-W, and Kim B Automotive software certification: current status and challenges SAE International journal of passenger cars-electronic and electrical systems 2016 9 74-80CrossrefGoogle Scholar261Zhang, N., Wang, J., & Ma, Y. (2018). Mining domain knowledge on service goals from textual service descriptions. IEEE Transactions on Services Computing (pp. 1–1). ISSN 1939-1374.CrossrefGoogle Scholar262Zhao Y and Rozier KY Formal specification and verification of a coordination protocol for an automated air traffic control system Science of Computer Programming Journal 2014 96 3 337-353CrossrefGoogle Scholar263Zhao, Y., & Rozier, K. Y. (November 2014). Probabilistic model checking for comparative analysis of automated air traffic control systems. In Proceedings of the 33rd IEEE/ACM International Conference On Computer-Aided Design (ICCAD 2014) (pp. 690–695). San Jose, California, U.S.A. IEEE/ACM.Google Scholar View all259. Towards a framework for certification of reliable autonomous systems 260. Computer systems organization 261. General and reference 262. Cross-computing tools and techniques 263. Software and its engineering 264. Software creation and management 265. Software verification and validation 266. Software organization and properties 267. Software functional properties 268. Formal methods 269. Theory of computation 270. Semantics and reasoning 271. Program reasoning 272. Program verification
- Formal methods for the certification of autonomous unmanned aircraft systems
Read More
- CCNP BCMSN Exam Certification Guide (3rd Edition) (Exam Certification Guide)
Read More
- CCSP SNPA Official Exam Certification Guide (3rd Edition) (Exam Certification Guide)
Cited By