Model Checking Controllers with Predicate Inputs

Digital controllers sitting at the digital-analog boundary often react to specific analog events that can be modeled in terms of predicates over real variables. The specifications for such controllers are also naturally described in terms of similar events, and can be formally expressed with simple extensions of assertion languages. This paper studies the model checking problem for such controllers, where the inputs represent predicates over real variables. We show that this is a novel problem which is distinct from both model checking hybrid systems and model checking purely digital systems. This paper presents a methodology which enables us to solve this problem using a combination of SMT solvers and existing industrial model checking tools. We establish the theoretical correctness of the approach and present two case studies to demonstrate the proposed tool flow.