www.prismmodelchecker.org
[PFF+19] Avi Pfeffer, Curt Wu, Gerald Fry, Kenny Lu, Steve Marotta, Mike Reposa, Yuan Shi, T. K. Satish Kumar, Craig A. Knoblock, David Parker, Irfan Muhammad and Chris Novakovic. Software Adaptation for an Unmanned Undersea Vehicle. IEEE Software, 36(2), pages 91-96, IEEE. March 2019. [pdf] [bib] [Summarises the PRINCESS project, which develops methods for adapting an optimising software at runtime, including mission verification using extensions of PRISM.]
Downloads:  pdf pdf (152 KB)  bib bib
Notes: The original version is available from ieeexplore.ieee.org.
Links: [Google] [Google Scholar]
Abstract. Most current software systems cannot adapt to changing hardware requirements or changing operational environments. This lack of adaptivity shortens the life of the software and makes it less capable of achieving its mission. We are developing Probabilistic Representation of Intent Commitments to Ensure Software Survival (PRINCESS) to enable software to adapt to both hardware changes and changing environments. We are developing methods to automatically optimize software for new environments, turning non-adaptive code into optimizable adaptive code. We are also developing sensor adapters that enable us to maintain software function despite changing or failing sensors. We are implementing PRINCESS on the navigation system of an unmanned undersea vehicle. An independent evaluation has demonstrated PRINCESS's ability to adapt to degraded sensors, changing environmental conditions, and loss of power.

Publications