Paper Info
Title
Specification-guided Software Fault Localization for Autonomous Mobile Systems
Abstract
Verification and validation are vital steps in the development process of autonomous systems such as mobile robots and self-driving vehicles, as they allow reasoning about system safety. In the domain of cyber-physical systems, techniques using formal requirements have been show to enable rigorous mathematical reasoning about system safety through techniques for automatic test generation and performance analysis. In this paper, we show that system-level and subsystem-level requirements can also enable fault localization in autonomous systems that use heterogeneous functional components. However, writing correct formal requirements is challenging and requires a significant investment of time, effort and most importantly, expertise. To address this issue, we propose a specification library for autonomous mobile systems called TLAM (Temporal Logic for Autonomous Mobility). Our contributions are twofold: We provide a library of parametric formal specifications at both the system-level and subsystem-level for typical subsystems in autonomous systems such as those for perception, planning and decision-making. The specification parameters encode the design trade-offs for such components. Second, we introduce a new fault localization technique based on these parametric specifications that identifies the likeliest subsystem that has a fault.
Year
DOI
Venue
2020
10.1109/MEMOCODE51338.2020.9315067
2020 18th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE)
Keywords
DocType
ISBN
Formal specifications,Formal verification,Autonomous systems,Verification & Validation,Fault Localization
Conference
978-1-7281-9149-2
Citations 
PageRank 
References 
0
0.34
0
Authors
4
Name
Order
Citations
PageRank
Tomoya Yamaguchi111.75
Bardh Hoxha201.35
Danil V. Prokhorov300.34
Jyotirmoy V. Deshmukh431729.18