dc.contributor.author |
Seotsanyana, M
|
|
dc.date.accessioned |
2010-09-28T13:49:04Z |
|
dc.date.available |
2010-09-28T13:49:04Z |
|
dc.date.issued |
2010-07 |
|
dc.identifier.citation |
Seotsanyana, 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 11 |
en |
dc.identifier.isbn |
978-0-620-46582-3 |
|
dc.identifier.uri |
http://hdl.handle.net/10204/4388
|
|
dc.description |
25th International Conference of CAD/CAM, Robotics and Factories of the Future Conference; Pretoria, 13-16 July 2010 |
en |
dc.description.abstract |
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 |
en |
dc.language.iso |
en |
en |
dc.subject |
Heorem proving |
en |
dc.subject |
Model checking |
en |
dc.subject |
Temporal logic |
en |
dc.subject |
Automaton |
en |
dc.subject |
Observer-pattern |
en |
dc.subject |
Robotics |
en |
dc.title |
Temporal logic runtime verification of dynamic systems |
en |
dc.type |
Conference Presentation |
en |
dc.identifier.apacitation |
Seotsanyana, M. (2010). Temporal logic runtime verification of dynamic systems. http://hdl.handle.net/10204/4388 |
en_ZA |
dc.identifier.chicagocitation |
Seotsanyana, M. "Temporal logic runtime verification of dynamic systems." (2010): http://hdl.handle.net/10204/4388 |
en_ZA |
dc.identifier.vancouvercitation |
Seotsanyana M, Temporal logic runtime verification of dynamic systems; 2010. http://hdl.handle.net/10204/4388 . |
en_ZA |
dc.identifier.ris |
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 -
|
en_ZA |