mdh.sePublications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Formal verification of an Autonomous Wheel Loader by model checking
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.ORCID iD: 0000-0002-7663-5497
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.ORCID iD: 0000-0003-2870-2680
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.ORCID iD: 0000-0003-0904-3712
2018 (English)In: Proceedings - International Conference on Software Engineering, IEEE Computer Society , 2018, p. 74-83Conference paper, Published paper (Refereed)
Abstract [en]

In an attempt to increase productivity and the workers' safety, the construction industry is moving towards autonomous construction sites, where various construction machines operate without human intervention. In order to perform their tasks autonomously, the machines are equipped with different features, such as position localization, human and obstacle detection, collision avoidance, etc. Such systems are safety critical, and should operate autonomously with very high dependability (e.g., by meeting task deadlines, avoiding (fatal) accidents at all costs, etc.). An Autonomous Wheel Loader is a machine that transports materials within the construction site without a human in the cab. To check the dependability of the loader, in this paper we provide a timed automata description of the vehicle's control system, including the abstracted path planning and collision avoidance algorithms used to navigate the loader, and we model check the encoding in UPPAAL, against various functional, timing and safety requirements. The complex nature of the navigation algorithms makes the loader's abstract modeling and the verification very challenging. Our work shows that exhaustive verification techniques can be applied early in the development of autonomous systems, to enable finding potential design errors that would incur increased costs if discovered later.

Place, publisher, year, edition, pages
IEEE Computer Society , 2018. p. 74-83
Keywords [en]
Autonomous Vehicle, Collision Avoidance, Formal Verification, Model Checking, Timed Automata, UPPAAL, Accident prevention, Automata theory, Construction equipment, Construction industry, Loaders, Mining machinery, Motion planning, Obstacle detectors, Wheels, Autonomous constructions, Autonomous Vehicles, Construction machines, Navigation algorithms, Safety requirements, Verification techniques
National Category
Electrical Engineering, Electronic Engineering, Information Engineering
Identifiers
URN: urn:nbn:se:mdh:diva-40747DOI: 10.1145/3193992.3193999Scopus ID: 2-s2.0-85052130860ISBN: 9781450357180 (print)OAI: oai:DiVA.org:mdh-40747DiVA, id: diva2:1246513
Conference
6th ACM/IEEE Conference on Formal Methods in Software Engineering, FormaliSE 2018, co-located with International Conference on Software Engineering, ICSE 2018, 2 June 2018
Available from: 2018-09-07 Created: 2018-09-07 Last updated: 2018-09-07Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Authority records BETA

Gu, RongMarinescu, RalucaSeceleanu, CristinaLundqvist, Kristina

Search in DiVA

By author/editor
Gu, RongMarinescu, RalucaSeceleanu, CristinaLundqvist, Kristina
By organisation
Embedded Systems
Electrical Engineering, Electronic Engineering, Information Engineering

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 60 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf