Akademik Veri Yönetim Sistemi
Tezin Türü: Doktora
Tezin Yürütüldüğü Kurum: Orta Doğu Teknik Üniversitesi, Mühendislik Fakültesi, Elektrik ve Elektronik Mühendisliği Bölümü, Türkiye
Tezin Onay Tarihi: 2015
Tezin Dili: İngilizce
Öğrenci: Mustafa Dursun
Danışman: SEMİH BİLGEN
Özet: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.