Statistical Model Checking of Distributed Adaptive Real-Time Software

Abstract. The problem of estimating quantitative properties of distributed cyber-physical software that coordinate and adapt to uncertain environments is addressed. A domain-specific language, called dmpl, is developed to both describe such a system and a target property. Statistical model checking (SMC) is used to estimate the probability with which the property holds on the system. A distributed SMC tool is developed and described. Virtual machines are used to implement a realistic execution environment, and to isolate simulations from one another. Experimental results on a coordinated multi-robot example are presented.

• Type: Journal
• Year: 2015
• Where: RV
• Authors: David Kyle, Jeffery P. Hansen, Sagar Chaki
• Keywords: Hardware, RV 2015