Model checking controllers with predicate inputs

Santhosh Prabhu, M ; Dasgupta, Pallab (2013) Model checking controllers with predicate inputs In: 2013 26th International Conference on VLSI Design and 2013 12th International Conference on Embedded Systems (VLSID), 5-10 January 2013, Pune, India.

Full text not available from this repository.

Official URL:

Related URL:


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.

Item Type:Conference or Workshop Item (Paper)
Source:Copyright of this article belongs to Institute of Electrical and Electronics Engineers.
Keywords:Model Checking; Gears; Boilers; Reactive Power; Standards; Labeling
ID Code:101588
Deposited On:12 Dec 2016 11:20
Last Modified:12 Dec 2016 11:20

Repository Staff Only: item control page