Towards the Verification of Safety-critical Autonomous Systems in Dynamic Environments
| Autor: | Falk Howar, Adina Aniculaesei, Andreas Rausch, Daniel Arnsberger |
|---|---|
| Jazyk: | angličtina |
| Rok vydání: | 2016 |
| Předmět: |
FOS: Computer and information sciences
Correctness Exploit computer.internet_protocol Computer science Distributed computing 0102 computer and information sciences 02 engineering and technology 01 natural sciences lcsh:QA75.5-76.95 Computer Science - Software Engineering Computer Science - Computers and Society Computer Science - Robotics Computers and Society (cs.CY) 0202 electrical engineering electronic engineering information engineering Collision avoidance lcsh:Mathematics Process (computing) Autonomous system (Internet) 020207 software engineering lcsh:QA1-939 Automaton Software Engineering (cs.SE) 010201 computation theory & mathematics Robot State (computer science) lcsh:Electronic computers. Computer science computer Robotics (cs.RO) |
| Zdroj: | Electronic Proceedings in Theoretical Computer Science, Vol 232, Iss Proc. V2CPS-16, Pp 79-90 (2016) V2CPS@IFM |
| ISSN: | 2075-2180 |
| Popis: | There is an increasing necessity to deploy autonomous systems in highly heterogeneous, dynamic environments, e.g. service robots in hospitals or autonomous cars on highways. Due to the uncertainty in these environments, the verification results obtained with respect to the system and environment models at design-time might not be transferable to the system behavior at run time. For autonomous systems operating in dynamic environments, safety of motion and collision avoidance are critical requirements. With regard to these requirements, Macek et al. [6] define the passive safety property, which requires that no collision can occur while the autonomous system is moving. To verify this property, we adopt a two phase process which combines static verification methods, used at design time, with dynamic ones, used at run time. In the design phase, we exploit UPPAAL to formalize the autonomous system and its environment as timed automata and the safety property as TCTL formula and to verify the correctness of these models with respect to this property. For the runtime phase, we build a monitor to check whether the assumptions made at design time are also correct at run time. If the current system observations of the environment do not correspond to the initial system assumptions, the monitor sends feedback to the system and the system enters a passive safe state. In Proceedings V2CPS-16, arXiv:1612.04023 |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|