JCSE, vol. 5, no. 1, pp.85-110, 2011

DOI: 10.5626/JCSE.2011.5.1.085/

Applying Formal Methods to Modeling and Analysis of Real-time Data Streams

Krasimira Kapitanova, Yuan Wei, Woochul Kang, Sang H. Son
University of Virginia, Charlottesville, VA, USA Zeno Software Inc., San Francisco, CA, USA Electronics and Telecommunication Research Institute, Daejeon, Korea University of Virginia, Charlottesville, VA, USA

Abstract: Achieving situation awareness is especially challenging for real-time data stream applications because they i) operate on continuous unbounded streams of data, and ii) have inherent realtime requirements. In this paper we showed how formal data stream modeling and analysis can be used to better understand stream behavior, evaluate query costs, and improve application performance. We used MEDAL, a formal specification language based on Petri nets, to model the data stream queries and the quality-of-service management mechanisms of RT-STREAM, a prototype system for data stream management. MEDAL’s ability to combine query logic and data admission control in one model allows us to design a single comprehensive model of the system. This model can be used to perform a large set of analyses to help improve the

Keyword: Real-time and Embedded Systems, Knowledge Representation Formalisms and Methods, Data Stream Analysis; Petri Nets; Operator Selectivity Estimation; Stream Query Modeling; Quality-of-Service Management

Full Paper:   176 Downloads, 2330 View