Publications

Formal Verification of Autonomy Models: From Livingstone to SMV

Authors
Charles Pecheur, Reid Simmons, Peter Engrand
Tags
, , , , , , ,

SMV, Translation, NASA

Title
Formal Verification of Autonomy Models: From Livingstone to SMV
Authors
Charles Pecheur, Reid Simmons, Peter Engrand
FM2018 Δ   0Kb   28 May 2020
Fmics2013 Δ   0Kb   28 May 2020
GandALF2017 Δ   0Kb   28 May 2020
HMI2011 Δ   0Kb   28 May 2020
LVLPrivate Δ   0Kb   28 May 2020
LVLPrivateNews Δ   0Kb   28 May 2020
Main Δ   0Kb   28 May 2020
Members Δ   0Kb   28 May 2020
Publications Δ   4Kb   28 May 2020
Site Δ   0Kb   28 May 2020
Talks Δ   4Kb   28 May 2020
Tools Δ   0Kb   28 May 2020
Type
In Collection
Book title
Agent Technology from a Formal Perspective
Series
NASA Monographs in Systems and Software Engineering
Publisher
Springer Verlag
Editor
Rouff, C. and Hinchey, M. and Rash, J. and Truszkowski, W. and Gordon-Spears, D.
Year
2006

Abstract

To fulfill the needs of its deep space exploration program, NASA is actively supporting research and development in autonomy software. However, the reliable and cost-effective development and validation of autonomy systems poses a tough challenge. Traditional scenario-based testing methods fall short because of the combinatorial explosion of possible situations to be analyzed, and formal verification techniques typically require a tedious, manual modelling by formal method experts. This paper presents the application of formal verification techniques in the development of autonomous controllers based on Livingstone, a model-based health-monitoring system that can detect and diagnose anomalies and suggest possible recovery actions. We present a translator that converts the models used by Livingstone into specifications that can be verified with the SMV model checker. The translation frees the Livingstone developer from the tedious conversion of his design to SMV, and isolates him from the technical details of the SMV program. We describe different aspects of the translation and briefly discuss its application to several NASA domains.

Tags Tags: , , , , , , ,

BibTeX Record
  @INCOLLECTION{lvl-2006-1,
    TITLE = {Formal Verification of Autonomy Models: From Livingstone to SMV},
    AUTHOR = {Charles Pecheur and Reid Simmons and Peter Engrand},
    YEAR = {2006},
    PUBLISHER = {Springer Verlag},
    EDITOR = {Rouff and C. and Hinchey and M. and Rash and J. and Truszkowski and W. and Gordon-Spears and D.},
    SERIES = {NASA Monographs in Systems and Software Engineering},
    URL = {https://lvl.info.ucl.ac.be/Publications/FormalVerificationOfAutonomyModelsFromLivingstoneToSMV},
  }