Abstract
The paper describes a formal approach for designing and reasoning about power-constrained, timed systems. The framework is based on process algebra, a formalism that has been developed to describe and analyze communicating concurrent systems. The proposed extension allows the modeling of probabilistic resource failures, priorities of resource usages, and power consumption by resources within the same formalism. Thus, it is possible to model alternative power-consumption behaviors and analyze tradeoffs in their timing and other characteristics. This paper describes the modeling and analysis techniques, and illustrates them with examples, including a dynamic voltage-scaling algorithm.
This research was supported in part by NSF CCR-9988409, NSF CCR-0086147, NSF CCR-0209024, ARO DAAD19-01-1-0473, and by the EU Future and Emerging Technologies programme IST-1999-14186 (ALCOM-FT).
Chapter PDF
References
C. Baier, B.R. Haverkort, H. Hermanns, and J.-P. Katoen. On the logical characterisation of performability properties. In Proceedings of ICALP 00, volume 1853 of LNCS, pages 780–792, 2000.
M. Bernardo. An algebra-based method to associate rewards with empa terms. In Proceedings of ICALP 97, volume 1256 of LNCS, pages 358–368, July 1997.
T. D. Burd and R. W. Brodersen. Energy efficient CMOS microprocessor design. In Proceedings of IEEE Hawaii International Conference on System Sciences. Volume 1: Architecture, pages 288–297, 1995.
J-Y. Choi, I. Lee, and H.-L. Xie. The specification and schedulability analysis of real-time systems using ACSR. In Proceedings of Real-Time Systems Symposium, December 1995.
E. Clarke, E. Emerson, and A. Prasad Sistla. Automatic verification of finite state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2), 1986.
L. de Alfaro. How to specify and verify the long-run average behavior of probabilistic systems. In Proceedings of IEEE Symposium on Logic in Computer Science, pages 454–465, 1998.
R. De Nicola and F. W. Vaandrager. Three logics for branching bisimulation. In Proceedings of LICS’ 90, 1990.
H. Hansson. Time and probability in formal design of distributed systems. In Real-Time Safety Critical Systems, volume 1. Elsevier, 1994.
H. Karlo. Linear Programming. Progress in Theoretical Computer Science. Birkhauser, 1991.
I. Lee, P. Brémond-Grégoire, and R. Gerber. A process algebraic approach to the specification and analysis of resource-bound real-time systems. Proceedings of the IEEE, pages 158–171, Jan 1994.
I. Lee, A. Philippou, and O. Sokolsky. Formal modeling and analysis of power-aware real-time systems. Technical Report MIS-CIS-02-12, Department of Computer and Information Science, University of Pennsylvania, 2002.
C. L. Liu and J. W. Layland. Scheduling algorithms for multiprogramming in a hard real-time environment. Journal of the ACM 20, 1:46–61, 1973.
A. Philippou, O. Sokolsky, R. Cleaveland, I. Lee, and S. Smolka. Probabilistic resource failure in real-time process algebra. In Proceedings of CONCUR 98, pages 389–404, 1998.
P. Pillai and K. G. Shin. Real-time dynamic voltage scaling for low-power embedded operating systems. In Proceedings of ACM Symposium on Operating Systems Principles, 2001.
R. Segala and N. Lynch. Probabilistic simulations for probabilistic processes. In Proceedings CONCUR 94, Uppsala, Sweden, volume 836 of LNCS, pages 481–496, 1994.
O. Sokolsky, I. Lee, and H. Ben-Abdallah. Specification and analysis of real-time systems with PARAGON. Annals of Software Engineering, 7:211–234, 1999.
M. Vardi. Automatic verification of probabilistic concurrent finite-state programs. In Proceedings of the Symposium on Foundations of Computer Science, pages 327–338, 1985.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Sokolsky, O., Philippou, A., Lee, I., Christou, K. (2003). Modeling and Analysis of Power-Aware Systems. In: Garavel, H., Hatcliff, J. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2003. Lecture Notes in Computer Science, vol 2619. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36577-X_29
Download citation
DOI: https://doi.org/10.1007/3-540-36577-X_29
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00898-9
Online ISBN: 978-3-540-36577-8
eBook Packages: Springer Book Archive