Alireza David Anisi

• Azaiez, Atef & Anisi, Alireza David (2026). Verified Design of Robotic Autonomous Systems using Probabilistic Model Checking. In Ciccozzi, Federico; Pires, Luís Ferreira & Bordeleau, Francis (Ed.), Proceedings of the 14th International Conference on Model-Based Software and Systems Engineering. SciTePress. ISSN 9789897587986. p. 85–96. doi: 10.5220/0014344800004058. Full text in Research Archive Show summary

  Safety and reliability play a crucial role when designing Robotic Autonomous Systems (RAS). Early consideration of hazards, risks and mitigation actions -- already in the concept study phase -- are important steps in building a solid foundations for the subsequent steps in the system engineering life cycle. The complex nature of RAS, as well as the uncertain and dynamic environments the robots operate within, do not merely effect fault management and operation robustness, but also makes the task of system design concept selection, a hard problem to address. Approaches to tackle the mentioned challenges and their implications on system design, range from ad-hoc concept development and design practices, to systematic, statistical and analytical techniques of Model Based Systems Engineering. In this paper, we propose a methodology to apply a formal method, namely Probabilistic Model Checking (PMC), to enable systematic evaluation and analysis of a given set of system design concepts, ultimately leading to a set of Verified Designs (VD). We illustrate the application of the suggested methodology -- using PRISM as probabilistic model checker -- to a practical RAS concept selection use-case from agriculture robotics. Along the way, we also develop and present a domain-specific Design Evaluation Criteria for agri-RAS.

• Azaiez, Atef; Anisi, David A.; Farrell, Marie & Luckcuck, Matt (2025). Revisiting Formal Methods for Autonomous Robots: A Structured Survey. In Cavalcanti, Ana; Foster, Simon & Richardson, Robert (Ed.), Proceedings of 26th Annual Conference Towards Autonomous Robotic Systems. Springer. ISSN 9783032014856. p. 338–352. doi: 10.1007/978-3-032-01486-3_26. Full text in Research Archive Show summary

  This paper presents the initial results from our structured literature review on applications of Formal Methods (FM) to Robotic Autonomous Systems (RAS). We describe our structured survey methodology; including database selection and associated search strings, search filters and collaborative review of identified papers. We categorise and enumerate the FM approaches and formalisms that have been used for specification and verification of RAS. We investigate FM in the context of sub-symbolic AI-enabled RAS and examine the evolution of how FM is used over time in this field. This work complements a pre-existing survey in this area and we examine how this research area has matured over time. Specifically, our survey demonstrates that some trends have persisted as observed in a previous survey. Additionally, it recognized new trends that were not considered previously including a noticeable increase in adopting Formal Synthesis approaches as well as Probabilistic Verification Techniques.

• Adam, Mustafa; Anisi, David A. & Ribeiro, Pedro (2025). A Verification Methodology for Safety Assurance of RAS. In Cavalcanti, Ana; Foster, Simon & Richardson, Robert (Ed.), Proceedings of 26th Annual Conference Towards Autonomous Robotic Systems. Springer. ISSN 9783032014856. p. 281–294. doi: 10.1007/978-3-032-01486-3_23. Full text in Research Archive Show summary

  Autonomous robots deployed in shared human environments, such as agricultural settings, require rigorous safety assurance to meet both functional reliability and regulatory compliance. These systems must operate in dynamic, unstructured environments, interact safely with humans, and respond effectively to a wide range of potential hazards. This paper presents a verification workflow for the safety assurance of an autonomous agricultural robot, covering the entire development life-cycle, from concept study and design to runtime verification. The outlined methodology begins with a systematic hazard analysis and risk assessment to identify potential risks and derive corresponding safety requirements. A formal model of the safety controller is then developed to capture its behaviour and verify that the controller satisfies the specified safety properties with respect to these requirements. The proposed approach is demonstrated on a field robot operating in an agricultural setting. The results show that the methodology can be effectively used to verify safety-critical properties and facilitate the early identification of design issues, contributing to the development of safer robots and autonomous systems.

• Adam, Mustafa; Hartmark, Elias Evjen; Andersen, Tage; Anisi, Alireza David & Cavalcanti, Ana (2024). Safety assurance of autonomous agricultural robots: from offline model-checking to runtime verification. IEEE International Conference on Automation Science and Engineering. ISSN 2161-8070. doi: 10.1109/CASE59546.2024.10711810. Full text in Research Archive Show summary

  The ongoing efforts to deploy safety-critical autonomous robots that operate in semi-structured, dynamic, and uncertain environments, reinforce the importance of supplementing traditional risk-management activities, input-based testing, and quality assurance procedures, with formal verification methods. With this approach, one may guarantee safe behavior in all relevant scenarios. In this paper, we propose a safety assurance framework enabling the integrated use of formal verification at all stages of the engineering life-cycle, beginning at the concept study, design, development, deployment, and operation. Along the way, a real use case from the agricultural industry, namely robotic ultra-violet (UVC) plant treatment, is used to demonstrate the proposed methodology. In particular, the transfer of offline model-checking artifacts to Runtime Verification elucidates how safety requirements can be conceptualized and subsequently translated into online monitors that are integrated seamlessly with the robot’s cont

• Murray, Yvonne; Nordlie, Henrik; Anisi, Alireza David; Ribeiro, Pedro & Cavalcanti, Ana (2024). Model Checking and Verification of Synchronisation Properties of Cobot Welding. Electronic Proceedings in Theoretical Computer Science (EPTCS). 411, p. 91–108. doi: 10.48550/arXiv.2411.14369. Full text in Research Archive Show summary

  This paper describes use of model checking to verify synchronisation properties of an industrial welding system consisting of a cobot arm and an external turntable. The robots must move synchronously, but sometimes get out of synchronisation, giving rise to unsatisfactory weld qualities in problem areas, such as around corners. These mistakes are costly, since time is lost both in the robotic welding and in manual repairs needed to improve the weld. Verification of the synchronisation properties has shown that they are fulfilled as long as assumptions of correctness made about parts outside the scope of the model hold, indicating limitations in the hardware. These results have indicated the source of the problem, and motivated a re-calibration of the real-life system. This has drastically improved the welding results, and is a demonstration of how formal methods can be useful in an industrial setting.

• Adam, Mustafa; Ye, Kangfeng; Anisi, Alireza David; Cavalcanti, Ana; Woodcock, Jim & Morris, Robert (2023). Probabilistic Modelling and Safety Assurance of an Agriculture Robot Providing Light-Treatment, Proceedings of the 2023 19th IEEE International Conference on Automation Science and Engineering (CASE). IEEE (Institute of Electrical and Electronics Engineers). ISSN 9798350320701. p. 1–7. doi: 10.1109/CASE56687.2023.10260395. Full text in Research Archive Show summary

  Continued adoption of agricultural robots postulates the farmer's trust in the reliability, robustness and safety of the new technology. This motivates our work on safety assurance of agricultural robots, particularly their ability to detect, track and avoid obstacles and humans. This paper considers a probabilistic modelling and risk analysis framework for use in the early development phases. Starting off with hazard identification and a risk assessment matrix, the behaviour of the mobile robot platform, sensor and perception system, and any humans present are captured using three state machines. An auto-generated probabilistic model is then solved and analysed using the probabilistic model checker PRISM. The result provides unique insight into fundamental development and engineering aspects by quantifying the effect of the risk mitigation actions and risk reduction associated with distinct design concepts. These include implications of adopting a higher performance and more expensive Object Detection System or opting for a more elaborate warning system to increase human awareness. Although this paper mainly focuses on the initial concept-development phase, the proposed safety-assurance framework can also be used during implementation, and subsequent deployment and operation phases.

• Serbezov, Atanas; Rhinehart, Russ; Goupil, Philippe & Anisi, Alireza David (2022). Academic-Practice Collaborations in Automation and Control: Keys for Success. IFAC-PapersOnLine. ISSN 2405-8971. 55(17), p. 308–313. doi: 10.1016/j.ifacol.2022.09.297. Full text in Research Archive Show summary

  This study identifies the keys for successful collaboration between the communities of academia and practice in the field of automation and control. The findings are based on the analysis of 85 different collaborations reported in a survey of the international control community conducted by the Industry and Education Committees at IFAC. Addressing a joint problem, understanding and respecting each other, frequent communication, and adequate funding are among the top attributes of successful collaboration. A complete list of the top 10 keys for success is provided in the conclusion section.

• Murray, Yvonne; Sirevåg, Martin; Ribeiro, Pedro; Anisi, Alireza David & Mossige, Morten (2022). Safety assurance of an industrial robotic control system using hardware/software co-verification. Science of Computer Programming. ISSN 0167-6423. 216. doi: 10.1016/j.scico.2021.102766. Full text in Research Archive Show summary

  As a general trend in industrial robotics, an increasing number of safety functions are being developed or re-engineered to be handled in software rather than by physical hardware such as safety relays or interlock circuits. This trend reinforces the importance of supplementing traditional, input-based testing and quality procedures which are widely used in industry today, with formal verification and model-checking methods. To this end, this paper focuses on a representative safety-critical system in an ABB industrial paint robot, namely the High-Voltage electrostatic Control system (HVC). The practical convergence of the high-voltage produced by the HVC, essential for safe operation, is formally verified using a novel and general co-verification framework where hardware and software models are related via platform mappings. This approach enables the pragmatic combination of highly diverse and specialised tools. The paper's main contribution includes details on how hardware abstraction and verification results can be transferred between tools in order to verify system-level safety properties. It is noteworthy that the HVC application considered in this paper has a rather generic form of a feedback controller. Hence, the co-verification framework and experiences reported here are also highly relevant for any cyber-physical system tracking a setpoint reference.

• Murray, Yvonne; David_Anisi, Alireza; Sirevåg, Martin; Ribeiro, Pedro & hagag, Rabah Saleh (2020). Safety Assurance of a High Voltage Controller for an Industrial Robotic System. In Carvalho, Gustavo & Stolz, Volker (Ed.), Formal Methods: Foundations and Applications. Springer. ISSN 9783030638825. p. 45–63. doi: 10.1007/978-3-030-63882-5_4. Full text in Research Archive Show summary

  Due to the risk of discharge sparks and ignition, there are strict rules concerning the safety of high voltage electrostatic systems used in industrial painting robots. In order to assure that the system fulfils its safety requirements, formal verification is an important tool to supplement traditional testing and quality assurance procedures. The work in this paper presents formal verification of the most important safety functions of a high voltage controller. The controller has been modelled as a finite state machine, which was formally verified using two different model checking software tools; Simulink Design Verifier and RoboTool. Five safety critical properties were specified and formally verified using the two tools. Simulink was chosen as a low-threshold entry point since MathWorks products are well known to most practitioners. RoboTool serves as a software tool targeted towards model checking, thus providing more advanced options for the more experienced user. The comparative study and results show that all properties were successfully verified. The verification times in both tools were in the order of a few minutes, which was within the acceptable time limit for this particular application.

• Espeland, Elene Marie; Jung, Byung Kyu & Anisi, Alireza David (2019). A predictive learning approach to optimal load sharing in energy management systems. In Garofalo, Franco (Eds.), 2019 18th European Control Conference (ECC). IEEE (Institute of Electrical and Electronics Engineers). ISSN 9783907144008. p. 498–504. doi: 10.23919/ECC.2019.8796043. Full text in Research Archive
• Murray, Yvonne & Anisi, Alireza David (2019). Survey of Formal Verification Methods for Smart Contracts on Blockchain. IFIP International Conference on New Technologies, Mobility and Security (NTMS). ISSN 2157-4952. doi: 10.1109/NTMS.2019.8763832. Full text in Research Archive
• Anisi, Alireza David; Tveide, Svein Gjermund & Kongezos, Valentinos (2017). State classification for autonomous gas sample taking using deep convolutional neural networks. In Koutsoukos, Xenofon & Bugeja, Marvin (Ed.), 25th Mediterranean Conference on Control and Automation. IEEE (Institute of Electrical and Electronics Engineers). ISSN 9781509045334. p. 370–375. doi: 10.1109/med.2017.7984146. Full text in Research Archive
• Kaldestad, Knut Berg; Haddadin, Sami; Belder, Rico; Hovland, Geir & Anisi, Alireza David (2014). Collision Avoidance with Potential Fields Based on Parallel Processing of 3D-Point Cloud Data on the GPU, 2014 IEEE International Conference on Robotics and Automation (ICRA 2014). Curran Associates, Inc.. ISSN 9781479936861. p. 3250–3257. doi: 10.1109/icra.2014.6907326. Full text in Research Archive

View all works in NVA

• Adam, Mustafa & Anisi, Alireza David (2026). Roboter skal hjelpe bøndene, men først må de bli trygge nok. www.forskning.no. Full text in Research Archive
• Anisi, Alireza David (2026). Assured Human–Robot Interaction (HRI): Agriculture robot application and verification methodology. doi: https:/robostar.cs.york.ac.uk/robostar-summer-school/. Full text in Research Archive
• Hartmark, Elias Evjen; Anisi, Alireza David; Sauter, Alexander & Lund, Mass Soldal (2026). Towards Automated Runtime Verification: LLM-Assisted Synthesis of Temporal Logic from Safety Requirements. Full text in Research Archive
• Adam, Mustafa & Anisi, Alireza David (2026). How agricultural robots can revolutionise sustainable farming. doi: https:/www.sciencenorway.no/farming-opinion-researchers-zone/how-agricultural-robots-can-revolutionise-sustainable-farming/. Full text in Research Archive Show summary

  OPINION: Agriculture is under pressure from several directions at once. Autonomous robots are increasingly presented as part of the answer. But safety has to come first.

• Adam, Mustafa; Anisi, Alireza David; Cavalcanti, Ana & Hartmark, Elias Evjen (2026). Dual-future Predictive Runtime Verification of collaborative human-robot tasks. Full text in Research Archive
• Hartmark, Elias Evjen; Adam, Mustafa & Anisi, Alireza David (2025). Enhancing Safety for Autonomous Agricultural Robots using Generative Runtime Verification in ROS 2. Full text in Research Archive
• Adam, Mustafa & Anisi, Alireza David (2025). Verification Methodology for Robots and Autonomous Systems. Full text in Research Archive
• Adam, Mustafa & Anisi, Alireza David (2025). Ensuring Reliability in Agricultural Robotics: Verification Methodology. Full text in Research Archive
• Azaiez, Atef & Anisi, Alireza David (2025). Revisiting Formal Methods for Autonomous Robots: A Structured Survey. Full text in Research Archive
• Adam, Mustafa & Anisi, Alireza David (2025). Ensuring Reliability in Agricultural Robotics: An End-to-End Verification Methodology. Full text in Research Archive
• Adam, Mustafa; Anisi, Alireza David; Hartmark, Elias; Andersen, Tage & Cavalcanti, Ana (2024). Safety Assurance of Autonomous Agricultural Robots: Offline to Runtime Verification. Full text in Research Archive
• Anisi, Alireza David (2024). Applications of RoboStar technology to real-world robotics systems. Full text in Research Archive
• Anisi, Alireza David & Adam, Mustafa (2023). Reliability and safety assurance of adaptive robotic and autonomous systems. Full text in Research Archive
• Anisi, Alireza David (2023). Robotene skal gå tettere på plantene i landbruket. nationen.no. ISSN 1891-4659. Full text in Research Archive
• David_Anisi, Alireza; Kongezos, Valentinos; Krieger, Roland; Lillehagen, Tommy & Skourup, Charlotte (2013). Robot-human cooperation for error recovery in oil and gas robotic applications. Full text in Research Archive
• Adam, Mustafa; Anisi, Alireza David & Cavalcanti, Ana (2026). Reliability and safety of robotic autonomous systems from offline model checking to online verification. Norges miljø- og biovitenskapelige universitet (NMBU). ISSN 9788257523770. Full text in Research Archive Show summary

  Autonomous robots are increasingly needed in sectors where labour is physically demanding, repetitive, hazardous, or difficult to sustain. Agriculture is one such domain, where robots can support tasks such as crop monitoring, transport, harvesting, and plant treatment. As these systems become more autonomous and move from controlled demonstrations to real farms and shared workspaces, they must operate under uncertainty, timing constraints, imperfect perception, and possible interaction with people. These conditions make dependable operation difficult to assure. Testing remains necessary, but it cannot by itself provide a traceable link between hazards, safety requirements, verified control logic, and the behaviour of deployed systems. This thesis develops a lifecycle-oriented methodology that uses offline model checking and Runtime Verification (RV) to strengthen the reliability and safety of Robotic Autonomous System (RAS). The objective is to support safety and systems engineers in building trustworthy autonomous systems. The methodology produces verification artefacts that remain traceable across the engineering lifecycle and can support certification-oriented safety processes under deployment uncertainty. At the same time, it considers the practical need to keep runtime safety mechanisms lightweight, so that safety assurance does not unnecessarily degrade system performance or operational efficiency. The methodology was developed through four linked contributions. First, it introduces a standards-informed approach for reasoning about safety risks under uncertainty at the concept-study stage, before the complete robotic system has been designed or implemented. Second, it presents a workflow for transforming structured safety requirements into executable runtime monitors, thereby enabling the deployed systems to produce operational evidence. Third, it consolidates these activities into a lifecycle-oriented verification methodology. Fourth, it extends beyond classical RV through a Dual-Future Predictive Runtime Verification (DF-PRV) approach, which combines a conservative formal predictive branch with a short-horizon-learning predictor. This supports earlier and more proportionate mitigation while preserving formally justified safety authority. The proposed methods were demonstrated through two representative case studies: an agricultural robotic safety scenario involving Ultraviolet-C (UV-C) treatment and a collaborative robotic task involving Human–Robot Collaboration (HRC).

• Nordlie, Henrik; Anisi, Alireza David & Murray, Yvonne (2024). Formal verification of synchronization properties of a multi-robot welding system. Norges miljø- og biovitenskapelige universitet (NMBU). Full text in Research Archive Show summary

  Welding tasks are among the most prevalent use cases of robots. In this thesis, the synchronization properties of a welding system, the IntelliWelder M06, are formally verified. The welding system consists of a robotic arm (UR10e) and a welding table (Carpano FIVE MOT) external axis. This system allows the user to define a welding operation directly on a CAD model in simulation and consequently plans trajectories for the robotic arm and external axis so that the welding operation can be performed autonomously. The relevant sections of this system are modeled using RoboChart, a UML-based modeling language tailored to represent robotic applications accurately. This work is performed to verify properties critical to the synchronized operation of the system through model checking. Desired properties were defined as assertions through tock-CSP, a process algebra that includes the tock event representing the passage of discrete time. The assertions required the following properties: • Each time a movement request is received for the robotic arm or the external axis, a movement operation is called for the corresponding component. • The state machines corresponding to the system state tracker, the external axis, and the robotic arm do not terminate. The CSP refinement checker, FDR4, was used to verify the validity of these properties. The results showed that the system requirements were fulfilled for sets of inputs based on the assumption of correctness outside of the model. Also, they were not fulfilled if the components outside the model were not assumed to be ideal, which shows that the modeled part of the system is input-dependant.

• Andersen, Tage; Hartmark, Elias Evjen; Anisi, Alireza David & Adam, Mustafa (2024). Kjøretidsverifisering av autonome robotsystemer i ROS 2. Norges miljø- og biovitenskapelige universitet (NMBU). Full text in Research Archive Show summary

  Den økte bruken av autonome robotsystemer har nødvendiggjort fremskritt i sikkerhetstiltak på grunn av de potensielle farene disse systemene kan utgjøre. Dette økte fokuset på automatisering og robotsystemer stiller spørsmål om hvordan sikkerhet og samsvar vil opprettholdes i et stadig mer automatisert samfunn. Med økende kompleksitet har det blitt tydelig at grundig offline testing ikke kan ta høyde for alle farer forbundet med uendelige tilstandssystemer, da sikkerheten er begrenset av de definerte testtilfellene. For å opprettholde sikkerhet og pålitelighet under drift, er det ofte nødvendig å sette inn flere verktøy. Et slikt verktøy kalles Kjøretidsverifisering (Runtime Verification, RV). Kjøretidsverifisering, et begrep som har blitt stadig mer populært, refererer til lette formelle metoder for å observere, analysere og noen ganger avbryte prosessene til systemprogramvare eller Cyber-Physical Systems (CPS). Et av de mest brukte språkene for CPS-robotikk er Robot Operating System (ROS). Selv om ROS har mange tilgjengelige kjøretidsverifiseringsverktøy, har den nylige utgivelsen av ROS 2 skapt et kunnskapsgap angående kompatible verktøy og deres bruk, spesielt med overgangen fra en sentralisert til en distribuert oppdagelsesinfrastruktur. Ved feil eller svikt i en sikkerhetskontroller spiller kjøretidsverifisering en avgjørende rolle i å oppdage hva som gikk galt, når og hvor det skjedde, og hvordan man kan administrere avbøtende tiltak. Hovedmålet med denne avhandlingen er å lage en pipeline for automatisk generering av RV-overvåkere for ROS 2 fra krav i naturlig språk til formelt verifiserte temporale logiske ligninger. For å oppnå dette, benytter pipelinen NASAs Copilot, OGMA og FRET-verktøy for å konvertere sikkerhetskrav i naturlig språk til formelt verifiserte temporale logiske overvåkere. Denne studien tar også for seg gapet i RV-verktøy for ROS 2, og gir en omfattende oversikt over eksisterende verktøy, implementeringsstrategier og fordelene med RV i CPS. Rammeverkets ytelse evalueres gjennom simulering og felttesting ved bruk av landbruksroboten Thorvald-005 og D435 RealSense-kameraet, med fokus på systembelastning, hendelse-til-strøm-basert kommunikasjon og effektivitet i bruddrapportering. Viktige funn viser at RV-rammeverket effektivt forbedrer sikkerhet og pålitelighet, med overvåkeren som opprettholder akseptabel systemytelse selv under høye meldingshastigheter. Forskningen understreker også viktigheten av å erkjenne maskinvarebegrensninger og forbedre prediktive evner for ytterligere å øke systemets robusthet. Funnene beviser at automatisk generering av formelt verifiserte RV-overvåkere for ROS 2 er mulig med dagens programvare og er raskt å implementere eller endre, noe som gjør det mulig å teste flere spesifikasjonsmodeller på samme system uten å endre kildekoden. Fremtidig arbeid innebærer å forbedre det generative RV-rammeverket, forbedre maskinvareintegrasjon og utvide kompatibilitet til andre ROS-distribusjoner. Resultatene har bidratt til den pågående utviklingen av NASAs RV-verktøy, og fremmer sikrere utplassering av autonome systemer i landbruk og andre domener. Denne avhandlingen er i seg selv et bidrag til metodikken og kunnskapen som er oppnådd for å riktig forstå og bruke Linear Temporal Logic (LTL)-overvåkere.

• Anisi, Alireza David; Adam, Mustafa; Hartmark, Elias Evjen & Andersen, Tage (2024). Runtime Verification of Autonomous Robotic Systems in ROS 2. Norges miljø- og biovitenskapelige universitet (NMBU). Full text in Research Archive

View all works in NVA