A Formal Approach for RT-DVS Algorithms Evaluation Based on Statistical Model Checking. (25th October 2015)

• Record Type: Journal Article
• Authors: Dai, Shengxin; Hong, Mei; Guo, Bing; He, Yang; Zhang, Qiongyu; Sun, Lin; Du, Yi
• Other Names: Song Xiaoyu Academic Editor.
• Is Part Of: Mathematical problems in engineering. Volume 2015(2015)
• Publication Date: 2015-10-25
• Subjects: Engineering mathematics -- Periodicals; 510.2462
• DOI: 10.1155/2015/815230
• Languages: English
• ISSNs: 1024-123X

Abstract

Abstract : Energy saving is a crucial concern in embedded real time systems. Many RT-DVS algorithms have been proposed to save energy while preserving deadline guarantees. This paper presents a novel approach to evaluate RT-DVS algorithms using statistical model checking. A scalable framework is proposed for RT-DVS algorithms evaluation, in which the relevant components are modeled as stochastic timed automata, and the evaluation metrics including utilization bound, energy efficiency, battery awareness, and temperature awareness are expressed as statistical queries. Evaluation of these metrics is performed by verifying the corresponding queries using UPPAAL-SMC and analyzing the statistical information provided by the tool. We demonstrate the applicability of our framework via a case study of five classical RT-DVS algorithms.