@inproceedings{b9670cfe9a4f484b922e0523cd7baaa9,
title = "Verification-driven development of ICAROUS based on automatic reachability analysis: A preliminary case study",
abstract = "The Integrated and Configurable Algorithms for Reliable Operations of Unmanned Systems (ICAROUS) is a software architecture being developed for the robust integration of mission-specific software modules and highly assured core software modules. This paper reports on the use of automatic reachability analysis during the development of ICAROUS, as a first step towards a broader formal verification effort of the software architecture. It explains how simulation based on state-space exploration and LTL model checking has been performed on a formal executable specification of the system in rewriting logic. Overall, this effort has unveiled issues such as deadlocks and undesired behavior, and has helped improve the ICAROUS design and source code.",
keywords = "ICAROUS, Maude, Model checking, Reachability analysis, Software reliability, UAS",
author = "Feli{\'u}, {Marco A.} and Camilo Rocha and Swee Balachandran",
note = "Publisher Copyright: {\textcopyright} 2017 Copyright held by the owner/author(s).; 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software, SPIN 2017 ; Conference date: 13-07-2017 Through 14-07-2017",
year = "2017",
month = jul,
day = "13",
doi = "10.1145/3092282.3120995",
language = "English",
series = "SPIN 2017 - Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software",
publisher = "Association for Computing Machinery, Inc",
pages = "94--97",
editor = "Hakan Erdogmus and Klaus Havelund",
booktitle = "SPIN 2017 - Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software",
}