Data abstraction method for model checking of real-time systems

Download

index.pdf

Date

2015

Author

Dursun, Mustafa

Metadata

Show full item record

Item Usage Stats

179
views

67
downloads

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.

Subject Keywords

Real-time data processing., Real-time programming., Systems software., Computer algorithms.

URI

http://etd.lib.metu.edu.tr/upload/12618574/index.pdf
https://hdl.handle.net/11511/24486

Collections

Graduate School of Natural and Applied Sciences, Thesis

Suggestions

OpenMETU
Core

Time series classification with feature covariance matrices Ergezer, Hamza; Leblebicioğlu, Mehmet Kemal (2018-06-01) In this work, a novel approach utilizing feature covariance matrices is proposed for time series classification. In order to adapt the feature covariance matrices into time series classification problem, a feature vector is defined for each point in a time series. The feature vector comprises local and global information such as value, derivative, rank, deviation from the mean, the time index of the point and cumulative sum up to the point. Extracted feature vectors for the time instances are concatenated t...
On higher order approximations for hermite-gaussian functions and discrete fractional Fourier transforms Candan, Çağatay (Institute of Electrical and Electronics Engineers (IEEE), 2007-10-01) Discrete equivalents of Hermite-Gaussian functions play a critical role in the definition of a discrete fractional Fourier transform. The discrete equivalents are typically calculated through the eigendecomposition of a commutator matrix. In this letter, we first characterize the space of DFT-commuting matrices and then construct matrices approximating the Hermite-Gaussian generating differential equation and use the matrices to accurately generate the discrete equivalents of Hermite-Gaussians.
Analysis Window Length Selection For Linear Signal Models Yazar, Alper; Candan, Çağatay (2015-05-19) A method is presented for the selection of analysis window length, or the number of input samples, for linear signal modeling without compromising the model assumptions. It is assumed that the signal of interest lies in a known linear space and noisy samples of the signal is provided. The goal is to use as many signal samples as possible to mitigate the effect of noise without violating the assumptions on the model. An application example is provided to illustrate the suggested method.
Maximum likelihood estimation of transition probabilities of jump Markov linear systems Orguner, Umut (Institute of Electrical and Electronics Engineers (IEEE), 2008-10-01) This paper describes an online maximum likelihood estimator for the transition probabilities associated with a jump Markov linear system (JMLS). The maximum likelihood estimator is derived using the reference probability method, which exploits an hypothetical probability measure to find recursions for complex expectations. Expectation maximization (EM) procedure is utilized for maximizing the likelihood function. In order to avoid the exponential increase in the number of statistics of the optimal EM algori...
Model updating of nonlinear structures from measured FRFs Canbaloglu, Guvenc; Özgüven, Hasan Nevzat (Elsevier BV, 2016-12-01) There are always certain discrepancies between modal and response data of a structure obtained from its mathematical model and experimentally measured ones. Therefore it is a general practice to update the theoretical model by using experimental measurements in order to have a more accurate model. Most of the model updating methods used in structural dynamics are for linear systems. However, in real life applications most of the structures have nonlinearities, which restrict us applying model updating techn...

Citation Formats

M. Dursun, “Data abstraction method for model checking of real-time systems,” Ph.D. - Doctoral Program, Middle East Technical University, 2015.