Confidence Composition for Monitors of Verification Assumptions

• DOI: 10.48550/arxiv.2111.03782
• Publication Date: 2021-01-01
• Authors: Ivan Ruchkin; Matthew Cleaveland; Radoslav Ivanov; Pengyuan Lu; Taylor J. Carpenter; Oleg Sokolsky; Insup Lee
• Keywords: Software Engineering (cs.SE); FOS: Computer and information sciences; Computer Science - Logic in Computer Science; Computer Science - Software Engineering; Artificial Intelligence (cs.AI); Computer Science - Artificial Intelligence; 0202 electrical engineering, electronic engineering, information engineering; 02 engineering and technology; Logic in Computer Science (cs.LO)

Closed-loop verification of cyber-physical systems with neural network controllers offers strong safety guarantees under certain assumptions. It is, however, difficult to determine whether these apply at run time because assumptions may be violated. To predict violations in a verified system, we propose three-step confidence composition (CoCo) framework for monitoring First, represent the sufficient condition propositional logical formula over Second, build calibrated monitors that evaluate probability each assumption holds. Third, obtain by composing using function suitable formula. Our CoCo provides theoretical bounds on calibration and conservatism compositional monitors. Two case studies show are better than their constituents successfully violations.