Towards automatic verification of autonomous systems
Conference Paper, Proceedings of (IROS) IEEE/RSJ International Conference on Intelligent Robots and Systems, Vol. 2, pp. 1410 - 1415, October, 2000
Abstract
While autonomous systems offer great promise in terms of capability and flexibility, their reliability is particularly hard to assess. This paper describes research to apply formal verification methods to languages used to develop autonomy software. In particular, we describe tools that automatically convert autonomy software into formal models that are then verified using model checking. This approach has been applied to MPL code for the Livingstone fault diagnosis system and to TDL task descriptions for mobile robot systems. Our long-term objective is to create tools that enable engineers and roboticists to use formal verification as part of the normal software development cycle.
BibTeX
@conference{Simmons-2000-122322,author = {R. Simmons and C. Pecheur and G. Srinivasan},
title = {Towards automatic verification of autonomous systems},
booktitle = {Proceedings of (IROS) IEEE/RSJ International Conference on Intelligent Robots and Systems},
year = {2000},
month = {October},
volume = {2},
pages = {1410 - 1415},
}
Copyright notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.