Seotsanyana, M2010-09-282010-09-282010-07Seotsanyana, M. Temporal logic runtime verification of dynamic systems. 25th International Conference of CAD/CAM, Robotics and Factories of the Future Conference; Pretoria, 13-16 July 2010, pp 11978-0-620-46582-3http://hdl.handle.net/10204/438825th International Conference of CAD/CAM, Robotics and Factories of the Future Conference; Pretoria, 13-16 July 2010Robotic computer systems are increasingly ubiquitous in everyday life and this has led to a need to develop safe and reliable systems. To ensure safety and reliability of these systems, the following three main verification techniques are usually considered: (1) theorem proving, (2) model checking, and (3) testing. However, the behaviour of robotic systems depends heavily on the environment and changes over time, which makes it hard to predict and analyse prior to their execution. Therefore, this paper provides a novel framework that automatically and verifiably monitors these systems at runtime. The main aim of the framework is to assist the operator through witnesses and counterexamples that are generated during the execution of the system. The framework is suitable for manufacturing and mine operations. In addition, the framework can explicitly capture sensor specifications of the environment and react to the changes accordingly to ensure safe and reliable operation during runtime of the system. The framework first constructs a region automaton of the environment and then represents operation rules in a formal specification language called universal computation tree logic (ACTL). This formal specification language allows the expression of complex desired behaviours, such as collision avoidance in the case of haul truck operationsenHeorem provingModel checkingTemporal logicAutomatonObserver-patternRoboticsConference PresentationSeotsanyana, M. (2010). Temporal logic runtime verification of dynamic systems. http://hdl.handle.net/10204/4388Seotsanyana, M. "Temporal logic runtime verification of dynamic systems." (2010): http://hdl.handle.net/10204/4388Seotsanyana M, Temporal logic runtime verification of dynamic systems; 2010. http://hdl.handle.net/10204/4388 .TY - Conference Presentation AU - Seotsanyana, M AB - Robotic computer systems are increasingly ubiquitous in everyday life and this has led to a need to develop safe and reliable systems. To ensure safety and reliability of these systems, the following three main verification techniques are usually considered: (1) theorem proving, (2) model checking, and (3) testing. However, the behaviour of robotic systems depends heavily on the environment and changes over time, which makes it hard to predict and analyse prior to their execution. Therefore, this paper provides a novel framework that automatically and verifiably monitors these systems at runtime. The main aim of the framework is to assist the operator through witnesses and counterexamples that are generated during the execution of the system. The framework is suitable for manufacturing and mine operations. In addition, the framework can explicitly capture sensor specifications of the environment and react to the changes accordingly to ensure safe and reliable operation during runtime of the system. The framework first constructs a region automaton of the environment and then represents operation rules in a formal specification language called universal computation tree logic (ACTL). This formal specification language allows the expression of complex desired behaviours, such as collision avoidance in the case of haul truck operations DA - 2010-07 DB - ResearchSpace DP - CSIR KW - Heorem proving KW - Model checking KW - Temporal logic KW - Automaton KW - Observer-pattern KW - Robotics LK - https://researchspace.csir.co.za PY - 2010 SM - 978-0-620-46582-3 T1 - Temporal logic runtime verification of dynamic systems TI - Temporal logic runtime verification of dynamic systems UR - http://hdl.handle.net/10204/4388 ER -