Sagar Chaki

David Kyle, Jeffery Hansen, Sagar Chaki, Proceedings of the 15th International Conference on Runtime Verification (RV), September 22-25, 2015.

Software: Tools and benchmarks for experiments reported in the paper are here. Read LICENSE.txt for the license, and README.txt for usage.

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.