Tesis > Documento


Ver el documento (formato PDF)   Pavese, Esteban.  "Garantías cuantitativas para espacios de estados no tratables"  (2015-10-19)
Facultad de Ciencias Exactas y Naturales. Universidad de Buenos Aires
URL:
     
Resumen:
Los lenguajes basados en máquinas de estados finitos (también llamados automátas finitos) son usados de manera ubicua para la especificación de sistemas de software. La formalidad de estos modelos permite la aplicación de técnicas de validación tales como el model checking. De esta manera, pueden responder con seguridad si un sistema cumple o no las propiedades de interés. Al mismo tiempo, estás máquinas pueden ser utilizadas de manera composicional, especificando comportamientos aislados mediante varias máquinas, y estableciendo el comportamiento global mediante su composición en paralelo. Este enfoque reduce el esfuerzo de validación, ya que la validez de las propiedades en el sistema deberían ser dependientes de la validez de las propiedades en cada componente. Sin embargo, este enfoque es amenazado por la complejidad del sistema especificado, dando lugar al problema de la explosión de estados, que puede impedir la aplicación de estas técnicas. En esta tesis presentamos un enfoque que intenta paliar este problema, proveyendo información cuantitativa respecto de la propiedad que se intentó validar sin éxito. Nuestro enfoque se sostiene sobre dos contribuciones distintas, donde cada una de ellas puede, además, ser aplicada en el contexto de problemas relacionados. Esta tesis se inspira en el modelado y model checking probabilísticos, que pueden proveer información cuantitativa respecto de la validez de una propiedad. Esta cuantificación nos sirve de validación parcial en el contexto del problema que nos interesa. Sin embargo, un enfoque composicional tiene sus propios problemas en un contexto probabilístico. Las anotaciones probabilísticas asociadas a eventos independientes precisan ser contrastadas con estimaciones obtenidas de la observación del comportamiento a modelar. Al agregar estas anotaciones, es preciso distinguir las fuentes de estas probabilidades; en otras palabras, las probabilidades de eventos independientes deberían estar asociadas al comportamiento de los componentes que generan este comportamiento. A su vez, es preciso mantener la relación entre la validez de los componentes de manera aislada, y la validez de los comportamientos en el sistema compuesto. Los formalismos disponibles al momento, sin embargo, no proveen la seguridad de que estos resultados de validez sean preservados durante la composición. La primera contribución de esta tesis es, entonces, una extensión probabilística al formalismo de Interface Automata. Esta extensión asegura la preservación de comportamiento tal como es observado por la lógica probabilística pCTL. La segunda parte de esta tesis apunta al análisis de estos modelos, en particular cuando un análisis exhaustivo no es factible, teniendo en cuenta que la complejidad del model checking probabilístico es aún mayor que en el caso clásico. Nuestra hipótesis en este trabajo es que una exploración parcial, pero sistemáticamente controlada, puede proveer cotas a los valores de interés con un costo computacional reducido. Los experimentos realizados sugieren que un análisis mediante este enfoque puede ser más efectivo que tanto el model checking exhaustivo como así también enfoques estadísticos relacionados.

Abstract:
System specifications have long been expressed through automatabased languages, which enable automated validation techniques such as model checking. Automata-based validation has been extensively used in the analysis of systems, where they have been able to provide yes/no answers to queries regarding their temporal properties. Additionally, a compositional approach to construction of software specifications reduces the specification effort, allowing the engineer to focus on specifying individual component behaviour; and then analyse the composite system behaviour. This also reduces the validation effort, since the validity of the composite specification should be dependent on the validity of the components. However, even in a compositional approach, automatic validation techniques usually cannot cope with systems under analysis that grow complex enough. Problems such as state space explosion seriously hamper the applicability of these approaches. In this thesis, we present an approach that can help cope with these absence of results by providing quantitative validation information related to the property being validated, even when the model checking approach is unable to handle the whole system. Our proposed technique stands on two different approaches, with each of them being applicable on its own to related problems. The inspiration is that probabilistic modelling and checking can provide quantitative information, which can in turn serve as partial validation when full checking is infeasible. Compositional construction, however, poses additional challenges in a probabilistic setting. Numerical annotations of probabilistically independent events must be contrasted against estimations or measurements, taking care of not compounding this quantification with exogenous factors, in particular other system components’ behaviour. The validity of compositionally constructed specifications requires that the validated probabilistic behaviour of each component continues to be preserved in the composite system. However, existing probabilistic automata-based formalisms do not support behaviour preservation of non-deterministic and probabilistic components over their composition. The first contribution of this thesis is a probabilistic extension to Interface Automata which preserves pCTL properties. This extension not only supports probabilistic behaviour but also allows for weaker prerequisites to interfacing composition, allowing for specification refinement of internal behaviour. The second part of our approach aims at analysing these probabilistically enriched models, obtaining quantitative information that can be related to the validity of the property under analysis, even when a complete analysis is infeasible. Computational complexity of estimating these metrics can be prohibitive, even more so than classic model checking. Our hypothesis is that a (carefully crafted) partial systematic exploration of a system model can provide better bounds for these quantitative model metrics at lower computation cost than exhaustive exploration. Our technique combines simulation, invariant inference and probabilistic model checking to produce a probabilistically relevant portion of the model, which is then exhaustively analysed. We report on experiments that suggest that metric estimation using this technique (for both fully probabilistic models and those exhibiting non-determinism) can be more effective than (full model) probabilistic and statistical model checking.

* A este resumen le pueden faltar caracteres especiales. Consulte la versión completa en el documento en formato PDF

Registro:
Título : Garantías cuantitativas para espacios de estados no tratables     =    Quantitative guarantees for intractable state spaces
Autor : Pavese, Esteban
Director : Braberman, Víctor
Consejero : Uchitel, Sebastián
Jurados : Hermmans, Holger  ; Kofman, Ernesto  ; D´Argenio, Pedro
Año : 2015-10-19
Editor : Facultad de Ciencias Exactas y Naturales. Universidad de Buenos Aires
Filiación : Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales
Departamento de Computación
Grado obtenido : Doctor de la Universidad de Buenos Aires en el área de Ciencias de la Computación
Ubicación : Preservación - http://digital.bl.fcen.uba.ar/gsdl-282/cgi-bin/library.cgi?a=d&c=tesis&d=Tesis_5849_Pavese
Idioma : Español
Area Temática : Computación / Ingeniería del Software
Palabras claves : MODELADO PROBABILISTICO; VERIFICACION PROBABILISTICA; SIMULACIONES; VERIFICACION ESTADISTICA; EXPLORACION PARCIAL; PROBABILISTIC MODELLING; PROBABILISTIC VALIDATION; MODEL SIMULATION; STATISTICAL METHODS; PARTIAL EXPLORATIONS
URL al Documento : 
URL al Registro : 
hola chau _gs.DocumentHeader_ chau2 _documentheader_ chau3
Estadísticas:
     http://digital.bl.fcen.uba.ar
Biblioteca Central Dr. Luis Federico Leloir - Facultad de Ciencias Exactas y Naturales - Universidad de Buenos Aires
Intendente Güiraldes 2160 - Ciudad Universitaria - Pabellón II - C1428EGA - Tel. (54 11) 4789-9293 int 34