|Table of Contents|

Formal Analysis and Verification of Energy Properties for Component-based Embedded Software Designs


Research Field:
Publishing date:


Formal Analysis and Verification of Energy Properties for Component-based Embedded Software Designs
CAO Dong1HU Jun23XU Bing-feng2
1.College of Automation,Nanjing University of Aeronautics and Astronautics,Nanjing 210016,China;2.College of Information Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 210016,China;3.State Key Laboratory for Novel Software Technology,Nanjing University,Nanjing 210093,China
embedded softwares component-based designs energy comsumption analysis software verification interface automata
The effective analysis and verification of system energy consumption properties of component-based embedded software in the stage of system design are studied.The real-time interface automata are extended with power semantics by assigning energy consumption rates in each system state,which is called energy interface automaton.The system compositional behaviors can be represented by an energy interface automaton network which consists of a set of energy interface automata synchronized by some shared actions.For the problems of minimal energy consumption calculation and maximal energy consumption verification,two algorithms are developed respectively based on analyzing the integral state space of the energy interface automaton network and its compatible reachability graph.


[ 1] H om J, K reme rU. Inter-program comp ilation fo r diskenergy reduction [ A ] . Powe r-Aw are Com pute r Systems, Third In ternationalW o rkshop PACS 2003[ C ].CA: San D iego, Springer-Ver lag, 2003. 13- 25.

[ 2] GuoY, Chheda S, Mo ritz A C. Runtim e b iased po in-ter reuse ana ly sis and its app lication to energy e fficiency[A]. Pow er-Aw are Computer System s, Third Inte rnationalW orkshop PACS2003 [ C ] . CA: San D iego,Springer-Verlag, 2003. 1- 12.
[ 3 ] 游静, 徐建, 赵学龙. 一种嵌套的软件抗衰策略及其模型[ J]. 南京理工大学学报( 自然科学版),2006, 30( 1): 43- 47.
[ 4] H u J, Yu X F, Zhang Y, e t a.l Checking com ponentbasedembedded so ftwa re designs for scenar io-basedtim ing spec ifica tions[ A]. The proceed ings o f the 2005IFIP Internationa l Conference on Embedded and Obiquitous computing [ C ]. Nagasak,i Japan: Spr ing er-V erlag, 2005. 395- 404.
[ 5] A lfa ro L, H enzinger T A. Interface autom ata[ J]. ESEC/S IGSOFT FSE, 2001, 26( 5): 109- 120.
[ 6] H u J, Yu X F, Zhang Y, et a .l Scena rio based ver-ifica tion for com ponen t-based em bedded so ftwa re designs[A ]. Proc of 34 th Interna tiona l Conference onPa ra lle l Process ingW o rkshops[ C]. W ashing ton D C,USA: IEEE CS, 2005. 240- 247.
[ 7] Farkas I K, Flinn J, Back G, e t a.l Quantify ing theenergy consumption o f a pocket computer and a java v irtualm achine[ A ]. Proceedings of Interna tiona l Con ferenceon Measurements andM odeling o f Computer Systems[ C]. New York, USA: ACM, 2000. 252- 263.
[ 8] Tan T K, Raghunathan A, Jha N K. Energy m acromodeling of em bedded operating system s [ J]. ACMTransactions on Em bedded Computing System s, 2005,4( 1): 231- 254.


Last Update: 2012-11-19