Model-Aided Runtime Verification for Robotic Systems (MARVer)
The software of robotic systems is generally complex and safety-critical. Therefore, formal specification and verification is a rather challenging task. Widely used testing and simulation alone are insufficient to ensure the correctness and safety of the system [MBF1, MBF2]. However, an important part of the workload in the development of robotic systems is the test and simulations carried out to show that the system works in accordance with the safety requirements. If robotic system developers are provided with formal verification methods that they can use easily and effectively, an inclusive and reliable verification for the robotic systems will be achieved and the workload will be reduced. Although the software of robot systems is complex, fortunately, it can be designed as interacting but separate modules [MBF3]. Many people in the robotics research community use the robot operating system (ROS), which is a framework. Due to the modular structure of robot software, ROS allows the control of a robot to be carried out by functional modules operating as separate processes. The modular structure of robotic system software makes it possible to create behavioral models and verify based on the model.
In the formal verification of robotic systems with model checking methods, the widely preferred and suitable model is timed automata [MBF5, MBF6]. Model-checking tools can automatically perform system verification with a high coverage rate when the system behavior model and requirements are formally defined. However, it is needed to make model creation easier. On the other side, run-time verification methods are applied to robotics systems for the verification of the system during execution. Users provide formal safety and security specifications, and monitors are automatically generated and incorporated into the system to ensure the safety and security of robots [MBF7]. Runtime verification and implementation are important to help in the fight against security threats [MBF11]. Model-checking, when combined with runtime verification, will improve the verification coverage and assurance on the operation of robotic systems [MBF4]. Verification methods to be used to verify the safety of robotic systems must comply with standards such as ISO 12100, IEC 61508, ISO 13849, ISO 10218-1, ISO 10218-2, ISO TS 15066 [MBF9, MBF10].
The method is implemented in two stages. In the first stage, the system model is created and verified by model-checking, and thus the compliance of the system design with the safety requirements is verified, while in the second stage, the compliance of the system's software with the verified model and meeting the requirements during execution are verified by runtime verification. In the first stage, once the requirements are given, the formal model of the robotic system is created. To facilitate the modeling of robotic systems, the method proposes an approach named model patterns. Then, by using the model-checking technique, the model is verified whether it meets the requirements or not. If not, the model is recursively revised until it meets all the requirements. In the second stage, the software of the robotic system is developed accordingly with the verified model. Then, the system software is subjected to runtime verification during execution integrating with the real system or a simulated environment. Since the instrumentation and configuration of runtime verifiers, the method provides approaches to facilitate the instrumentation and configuration for runtime verification by utilizing a formal model and formally specified requirements of the system. In addition, the Runtime verification technique generally considers the internal states of the system for checking the compliance of the requirements. The method also proposes the integration of utilities which enables to checking of some requirements not verified just by monitoring the internal states of the system.
- Less time-consuming compared to simulation-based for limited state space.
- Once the system model and property specification are provided to the model checker, the verification process is fully automatic.
- Long simulation runs are not required to obtain good coverage
- Requires minimal human intervention for the verification process. So, human error is minimized.
- Although industrial systems achieve successful results against volumetric attacks from offline records, their detection and system verification on runtime for security is a separate challenge [MBF12, MBF13]. The size of the volumetric attack that can be made on the system should be verified as quickly as possible to detect.
- The system should be small in terms of the number of states to be processed by the model checker.
- Errors in specification: An implementation verification requires two versions of a design. Therefore, a bug in the specifications voids the reference model may escape implementation verification and may trickle down to implementations. A typical type of specification error is missing specifications[MBF8].
- User errors: Example user errors are an incorrect representation of specifications and over constraining the design.
- Formal specification languages need to be adopted for autonomous Industrial robots
- Identifying what is anomalous, without exhaustive knowledge of the concept of anomaly, requires the existence of an underlying concept of normality. For this reason, it may be difficult to detect attacks that can be made while recognizing normal data on the system side during the initial start-up phase of the system.
- [MBF1] Luckcuck, M., Farrell, M., Dennis, L., Dixon, C., Fisher, M. (2019), Formal Specification and Verification of Autonomous Robotic Systems: A Survey, ACM Computing Surveys, 52: 1-41.
- [MBF2] Ingrand, F., (2019), Recent Trends in Formal Validation and Verification of Autonomous Robots Software. 2019 Third IEEE International Conference on Robotic Computing (IRC).
- [MBF3] Siegwart, R. and Nourbakhsh, I, (2004), Introduction to Autonomous Mobile Robots, MIT Press.
- [MBF4] Desai, A., Dreossi, T., Seshia, S.A., (2017), Combining Model Checking and Runtime Verification for Safe Robotics, Runtime Verification RV 2017, LNCS 10548, pp. 172–189.
- [MBF5] Wang, R., Guan, Y., Song, H., Li, X., Li, X., Shi, Z., Song, X., (2018), A Formal Model-Based Design Method for Robotic Systems, IEEE Systems Journal, PP: 1-12.
- [MBF6] Halder, R., Proença, J., Macedo, N., Santos, A (2017), Formal Verification of ROS-Based Robotic Applications Using Timed-Automata, 2017 IEEE/ACM 5th International FME Workshop on Formal Methods in Software Engineering (FormaliSE).
- [MBF7] Huang, J., Erdogan, C., Zhang, Y., Moore, B., Luo, Q., Sundaresan, A., Rosu, G., (2014), ROSRV: Runtime Verification for Robots, International Conference on Runtime Verification, Springer. 8734: 247-254.
- [MBF8] W.K. Lam, Hardware Design Verification: Simulation and Formal Method-Based Approaches, Pearson Publishing, 2005.
- [MBF9] Villani, V. P., F. Leali, F. Secchi, C. (2018), Survey on human-robot collaboration in industrial settings: Safety, intuitive interfaces and applications, Mechatronics, 55: 248-266.
- [MBF10] Jérémie Guiochet, M. M., Hélène Waeselynck (2017). "Safety-critical advanced robots: A survey." Robotics and Autonomous Systems, 94: 43-52.
- [MBF11] Sánchez, C., Schneider, G., Ahrendt, W., Bartocci, E., Bianculli, D., Colombo, C., Lourenço, J. M. J. F. M. i. S. D. (2019). A survey of challenges for runtime verification from advanced application domains (beyond software). 54(3), 279-335
- [MBF12] Palmieri, F. J. J. o. N., & Applications, C. (2019). Network anomaly detection based on logistic regression of nonlinear chaotic invariants. 148, 102460.
- [MBF13] Tann, W. J.-W., Wei, J. T. J., Purba, J., & Chang, E.-C. J. a. p. a. (2020). Filtering DDoS Attacks from Unlabeled Network Traffic Data Using Online Deep Learning.