Abstract
In previous works, the authors introduced a framework for software analysis, which is based on optimization of Lyapunov invariants. These invariants prove critical software properties such as absence of overflow and termination in finite time. In this paper, graph models of software are introduced and the software analysis framework is further developed and extended on graph models. A distributed Lyapunov function is assigned to the software by assigning a Lyapunov function to every node on its graph model. The global decremental condition is then enforced by requiring that the Lyapunov functions on each node decrease as transitions take place along the arcs. The concept of graph reduction and optimality of graphs for Lyapunov analysis is briefly discussed.
This work was supported by the National Science Foundation (NSF-0715025). Any opinions, findings, conclusions or recommendations expressed in this paper are those of the authors and do not necessarily reflect the views of the supporting organization.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Boyd, S., Ghaoui, L.E., Feron, E., Balakrishnan, V.: Linear Matrix Inequalities in Systems and Control Theory. Society for Industrial and Applied Math. (1994)
Bemporad, A., Mignone, D., Morari, M.: Moving horizon estimation for hybrid systems and fault detection. In: Proc. American Control Conf., pp. 2471–2475 (1999)
Bertsimas, D., Tsitsikilis, J.: Introduction to Linear Optimization. Athena Scientific (1997)
Branicky, M.S., Borkar, V.S., Mitter, S.K.: A unified framework for hybrid control: Model and optimal control theory. IEEE Trans. Automatic Control 43(1), 31–45 (1998)
Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. on Programming Languages and Systems 8(2), 244–263 (1986)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)
Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proc. 4th Symposium on Principles of Programming Languages, pp. 238–252 (1977)
Prajna, S., Jadbabaie, A., Pappas, G.: A Framework for Worst-Case and Stochastic Safety Verification Using Barrier Certificates. IEEE Trans. on Automatic Control 52(8), 1415–1428 (2007)
Johansson, M., Rantzer, A.: Computation of piecewise quadratic Lyapunov functions for hybrid systems. IEEE Trans. on Automatic Control 43(4), 555–559 (1998)
Alur, R., Pappas, G.J. (eds.): HSCC 2004. LNCS, vol. 2993. Springer, Heidelberg (2004)
Lafferriere, G., Pappas, G.J., Sastry, S.: Hybrid systems with finite bisimulations. In: Antsaklis, P.J., Kohn, W., Lemmon, M.D., Nerode, A., Sastry, S.S. (eds.) HS 1997. LNCS, vol. 1567, Springer, Heidelberg (1999)
Lygeros, J., Tomlin, C., Sastry, S.: Controllers for reachability specifications for hybrid systems. Automatica 35(3), 349–370 (1999)
Peled, D.A.: Software Reliability Methods. Springer, New York (2001)
Parrilo, P.A.: Minimizing Polynomial Functions. In: Algorithmic and Quantitative Real Algebraic Geometry. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 60, pp. 83–99. AMS
Roozbehani, M., Feron, É., Megrestki, A.: Modeling, Optimization and Computation for Software Verification. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 606–622. Springer, Heidelberg (2005)
Roozbehani, M., Megretski, A., Feron, E.: Convex optimization proves software correctness. In: Proc. American Control Conf., pp. 1395–1400 (2005)
Roozbehani, M., Megretski, A., Feron, E.: Optimization of Lyapunov Invariants for Certification of Software Systems. IEEE Trans. Automatic Control (submitted, 2007)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Roozbehani, M., Megretski, A., Frazzoli, E., Feron, E. (2008). Distributed Lyapunov Functions in Analysis of Graph Models of Software. In: Egerstedt, M., Mishra, B. (eds) Hybrid Systems: Computation and Control. HSCC 2008. Lecture Notes in Computer Science, vol 4981. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-78929-1_32
Download citation
DOI: https://doi.org/10.1007/978-3-540-78929-1_32
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-78928-4
Online ISBN: 978-3-540-78929-1
eBook Packages: Computer ScienceComputer Science (R0)