ABSTRACT
CONTENTS 11.1 Introduction 273 11.2 Energy Bugs of Android Applications 274
11.2.1 Android Framework 274 11.2.1.1 Multilayered Architecture 274 11.2.1.2 Power Management 275 11.2.1.3 Activity Life Cycle 275
11.2.2 Detecting Energy Bugs 276 11.3 Energy Consumption Behavior 278
11.3.1 Energy Consumption Model 278 11.3.2 Linear Hybrid Automata 280 11.3.3 Power Consumption Automata 281
11.3.3.1 Formal Model of a PCA 281 11.3.3.2 Operational Semantics 282 11.3.3.3 Timed Words 283 11.3.3.4 Mealy Diagrams 284
11.4 Property Specications for Detecting Energy Bugs 284 11.4.1 Duration-Bounded Cost Constraints 284 11.4.2 Temporal Logic with Freeze Quantier 285
11.4.2.1 Temporal Logic-Based Approach 285 11.4.2.2 Formal Denitions of fWLTL 286
11.4.3 Model Checking Problem 287 11.4.3.1 Decidability and Undecidability 287 11.4.3.2 Approximation Methods 288 11.4.3.3 Monotonic Constraints 288 11.4.3.4 Property Patterns 289
11.5 Analysis Using Real-Time Maude 290 11.5.1 A Brief Introduction to Real-Time Maude 290
11.5.1.1 Real-Time Theory 290 11.5.1.2 Instantaneous Rewrite Rules 290 11.5.1.3 Tick Rewrite Rules 290 11.5.1.4 Sampling Abstraction Method 291
11.5.2 Time-Bounded Reachability Analysis 291 11.5.2.1 System State 291 11.5.2.2 State Transitions 292 11.5.2.3 Time-bounded Search 292
11.5.3 LTL Model Checking 293 11.5.3.1 LTL Model Checker in Real-Time Maude 293 11.5.3.2 Removing Freeze Quantiers 294 11.5.3.3 Model Checking Command 295 11.5.3.4 Correctness of Translation 295
11.6 SAT-Based Analysis Methods 296 11.6.1 Basic Concepts 297
11.6.1.1 Bounded Model Checking Problem 297 11.6.1.2 Fault Localization Problem 297 11.6.1.3 Minimal Unsatised Subset 297 11.6.1.4 Maximal Satisable Subset 297 11.6.1.5 Minimal Correction Subset 297 11.6.1.6 Hitting Set 297 11.6.1.7 Partial Maximum Satisability 298 11.6.1.8 Model-Based Diagnosis Framework 298
11.6.2 Boolean Encoding 298 11.6.2.1 Trace Formula 298 11.6.2.2 LTL-Bounded Model Checking 299
11.6.3 Fault Localization 300 11.6.3.1 Fault Localization Problem for a PCA 300 11.6.3.2 Failure Model 300 11.6.3.3 Nondeterministic Transitions 301 11.6.3.4 Trace Formula for Fault Localization 302 11.6.3.5 Sliced Transition Sequence 302 11.6.3.6 Fault Localization Method 302
11.7 Conclusion 303 Acknowledgments 304 References 304
Energy consumption is one of the primary nonfunctional concerns in systemsequipped with batteries. The capacity of batteries is limited and reducing the consumption of battery power is mandatory for the systems to be long-lived. The hardware components consume the battery power directly. However, application programs are responsible for energy consumption because they control the usage of the hardware
components. If the programs contain some hidden bugs, unexpectedly large amounts of energy may be consumed. These energy bugs must be eliminated in the early stages of the development of application programs. In this chapter we study a model-based analysis method of energy consumption behavior. Using a variant of linear hybrid automata as a rigorous model, we reduce the problem of detecting anomalies in the energy consumption behavior to logic model checking.
