Distributed lyapunov functions in analysis of graph models of software
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 a...
| Main Authors: | , , , |
|---|---|
| Other Authors: | |
| Format: | Article |
| Language: | en_US |
| Published: |
Spring Berlin/Heidelberg
2011
|
| Online Access: | http://hdl.handle.net/1721.1/67000 https://orcid.org/0000-0002-0505-1400 https://orcid.org/0000-0001-9088-0205 |
| _version_ | 1811090792226226176 |
|---|---|
| author | Roozbehani, Mardavij Megretski, Alexandre Frazzoli, Emilio Feron, Eric |
| author2 | Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science |
| author_facet | Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science Roozbehani, Mardavij Megretski, Alexandre Frazzoli, Emilio Feron, Eric |
| author_sort | Roozbehani, Mardavij |
| collection | MIT |
| description | 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. |
| first_indexed | 2024-09-23T14:52:01Z |
| format | Article |
| id | mit-1721.1/67000 |
| institution | Massachusetts Institute of Technology |
| language | en_US |
| last_indexed | 2024-09-23T14:52:01Z |
| publishDate | 2011 |
| publisher | Spring Berlin/Heidelberg |
| record_format | dspace |
| spelling | mit-1721.1/670002022-09-29T11:03:37Z Distributed lyapunov functions in analysis of graph models of software Roozbehani, Mardavij Megretski, Alexandre Frazzoli, Emilio Feron, Eric Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science Massachusetts Institute of Technology. Laboratory for Information and Decision Systems Roozbehani, Mardavij Roozbehani, Mardavij Megretski, Alexandre Frazzoli, Emilio 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. National Science Foundation (U.S.) (NSF-0715025) 2011-11-10T15:56:00Z 2011-11-10T15:56:00Z 2008-07 Article http://purl.org/eprint/type/ConferencePaper 978-3-540-78928-4 http://hdl.handle.net/1721.1/67000 Roozbehani, Mardavij et al. “Distributed Lyapunov Functions in Analysis of Graph Models of Software.” Hybrid Systems: Computation and Control. Ed. Magnus Egerstedt & Bud Mishra. Berlin, Heidelberg: Springer Berlin Heidelberg, 2008. 443-456. © 2008 Springer https://orcid.org/0000-0002-0505-1400 https://orcid.org/0000-0001-9088-0205 en_US http://dx.doi.org/10.1007/978-3-540-78929-1_32 Hybrid Systems: Computation and Control Article is made available in accordance with the publisher's policy and may be subject to US copyright law. Please refer to the publisher's site for terms of use. application/pdf Spring Berlin/Heidelberg Springer |
| spellingShingle | Roozbehani, Mardavij Megretski, Alexandre Frazzoli, Emilio Feron, Eric Distributed lyapunov functions in analysis of graph models of software |
| title | Distributed lyapunov functions in analysis of graph models of software |
| title_full | Distributed lyapunov functions in analysis of graph models of software |
| title_fullStr | Distributed lyapunov functions in analysis of graph models of software |
| title_full_unstemmed | Distributed lyapunov functions in analysis of graph models of software |
| title_short | Distributed lyapunov functions in analysis of graph models of software |
| title_sort | distributed lyapunov functions in analysis of graph models of software |
| url | http://hdl.handle.net/1721.1/67000 https://orcid.org/0000-0002-0505-1400 https://orcid.org/0000-0001-9088-0205 |
| work_keys_str_mv | AT roozbehanimardavij distributedlyapunovfunctionsinanalysisofgraphmodelsofsoftware AT megretskialexandre distributedlyapunovfunctionsinanalysisofgraphmodelsofsoftware AT frazzoliemilio distributedlyapunovfunctionsinanalysisofgraphmodelsofsoftware AT feroneric distributedlyapunovfunctionsinanalysisofgraphmodelsofsoftware |