Using Ellipsoidal Domains to Analyze Control Systems Software - Computer Science > Programming LanguagesReportar como inadecuado




Using Ellipsoidal Domains to Analyze Control Systems Software - Computer Science > Programming Languages - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

Abstract: We propose a methodology for the automatic verification of safety propertiesof controllers based on dynamical systems, such as those typically used inavionics. In particular, our focus is on proving stability properties ofsoftware implementing linear and some non-linear controllers. We develop anabstract interpretation framework that follows closely the Lyapunov methodsused in proofs at the model level and describe the corresponding abstractdomains, which for linear systems consist of ellipsoidal constraints. Theseellipsoidal domains provide abstractions for the values of state variables andmust be combined with other domains that model the remaining variables in aprogram. Thus, the problem of automatically assigning the right type ofabstract domain to each variable arises. We provide an algorithm that solvesthis classification problem in many practical cases and suggest how it could begeneralized to more complicated cases. We then find a fixpoint by solving amatrix equation, which in the linear case is just the discrete Lyapunovequation. Contrary to most cases in software analysis, this fixpoint cannot bereached by the usual iterative method of propagating constraints untilsaturation and so numerical methods become essential. Finally, we illustrateour methodology with several examples.



Autor: Fernando Alegre, Eric Feron, Santosh Pande

Fuente: https://arxiv.org/







Documentos relacionados