Data abstraction method for model checking of real-time systems

Dursun, Mustafa
Model checking consists of automatic techniques for verifying whether a specified formal property holds for a specific state in a given finite-state model of a system. A major limitation of model checking arises in modeling infinite state systems. This limitation is the main obstacle for model checking of real time systems, due to the need for verifying real time constraints and the necessity of considering infinite data domains. Timed automata models are used to successfully cater for temporal behavior in modeling real time constraints. Abstracting infinite data sets with finite representations is mandatory for feasibility of model checking. In this study, we present an abstraction method for data which is collectively produced by a set of concurrent, asynchronous and periodic tasks in a real time system. The proposed method maps the infinite data domain to a finite one by taking temporal dependencies into account, and models the data with a finite state automaton. Proof of concept is provided with a case study that implements the proposed technique on a multi-sensor data aggregation problem.
Citation Formats
M. Dursun, “Data abstraction method for model checking of real-time systems,” Ph.D. - Doctoral Program, 2015.