Garantías cuantitativas para espacios de estados no tratables

Mostrar todas las versiones(3)

Los lenguajes basados en máquinas de estados finitos (también llamadosautomátas finitos) son usados de manera ubicua para la especificación desistemas de software. La formalidad de estos modelos permite la aplicación de técnicasde validación tales como el model checking. De esta manera, pueden respo...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autor principal: Pavese, Esteban
Formato: Tesis Doctoral
Lenguaje:Español
Publicado: 2015
Materias:
MODELADO PROBABILISTICO
VERIFICACION PROBABILISTICA
SIMULACIONES
VERIFICACION ESTADISTICA
EXPLORACION PARCIAL
PROBABILISTIC MODELLING
PROBABILISTIC VALIDATION
MODEL SIMULATION
STATISTICAL METHODS
PARTIAL EXPLORATIONS
Acceso en línea:https://hdl.handle.net/20.500.12110/tesis_n5849_Pavese
Aporte de:
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires
id todo:tesis_n5849_Pavese
record_format dspace
institution Universidad de Buenos Aires
institution_str I-28
repository_str R-134
collection Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA)
language Español
orig_language_str_mv Español
topic MODELADO PROBABILISTICO
VERIFICACION PROBABILISTICA
SIMULACIONES
VERIFICACION ESTADISTICA
EXPLORACION PARCIAL
PROBABILISTIC MODELLING
PROBABILISTIC VALIDATION
MODEL SIMULATION
STATISTICAL METHODS
PARTIAL EXPLORATIONS
spellingShingle MODELADO PROBABILISTICO
VERIFICACION PROBABILISTICA
SIMULACIONES
VERIFICACION ESTADISTICA
EXPLORACION PARCIAL
PROBABILISTIC MODELLING
PROBABILISTIC VALIDATION
MODEL SIMULATION
STATISTICAL METHODS
PARTIAL EXPLORATIONS
Pavese, Esteban
Garantías cuantitativas para espacios de estados no tratables
topic_facet MODELADO PROBABILISTICO
VERIFICACION PROBABILISTICA
SIMULACIONES
VERIFICACION ESTADISTICA
EXPLORACION PARCIAL
PROBABILISTIC MODELLING
PROBABILISTIC VALIDATION
MODEL SIMULATION
STATISTICAL METHODS
PARTIAL EXPLORATIONS
description Los lenguajes basados en máquinas de estados finitos (también llamadosautomátas finitos) son usados de manera ubicua para la especificación desistemas de software. La formalidad de estos modelos permite la aplicación de técnicasde validación tales como el model checking. De esta manera, pueden respondercon 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 comportamientosaislados mediante varias máquinas, y estableciendo el comportamientoglobal 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 dependientesde la validez de las propiedades en cada componente. Sin embargo, este enfoque esamenazado por la complejidad del sistema especificado, dando lugar al problema dela 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, proveyendoinformación cuantitativa respecto de la propiedad que se intentó validar sinéxito. Nuestro enfoque se sostiene sobre dos contribuciones distintas, donde cada unade ellas puede, además, ser aplicada en el contexto de problemas relacionados. Estatesis se inspira en el modelado y model checking probabilísticos, que pueden proveerinformación cuantitativa respecto de la validez de una propiedad. Esta cuantificaciónnos sirve de validación parcial en el contexto del problema que nos interesa. Sin embargo, un enfoque composicional tiene sus propios problemas en un contextoprobabilístico. Las anotaciones probabilísticas asociadas a eventos independientesprecisan ser contrastadas con estimaciones obtenidas de la observación del comportamientoa modelar. Al agregar estas anotaciones, es preciso distinguir las fuentes deestas probabilidades; en otras palabras, las probabilidades de eventos independientesdeberían estar asociadas al comportamiento de los componentes que generan estecomportamiento. A su vez, es preciso mantener la relación entre la validez de loscomponentes de manera aislada, y la validez de los comportamientos en el sistemacompuesto. Los formalismos disponibles al momento, sin embargo, no proveen la seguridadde 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 alformalismo de Interface Automata. Esta extensión asegura la preservación de comportamientotal como es observado por la lógica probabilística pCTL. La segunda parte de esta tesis apunta al análisis de estos modelos, en particularcuando un análisis exhaustivo no es factible, teniendo en cuenta que la complejidaddel model checking probabilístico es aún mayor que en el caso clásico. Nuestra hipótesisen 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 puedeser más efectivo que tanto el model checking exhaustivo como así también enfoquesestadísticos relacionados.
format Tesis Doctoral
author Pavese, Esteban
author_facet Pavese, Esteban
author_sort Pavese, Esteban
title Garantías cuantitativas para espacios de estados no tratables
title_short Garantías cuantitativas para espacios de estados no tratables
title_full Garantías cuantitativas para espacios de estados no tratables
title_fullStr Garantías cuantitativas para espacios de estados no tratables
title_full_unstemmed Garantías cuantitativas para espacios de estados no tratables
title_sort garantías cuantitativas para espacios de estados no tratables
publishDate 2015
url https://hdl.handle.net/20.500.12110/tesis_n5849_Pavese
work_keys_str_mv AT paveseesteban garantiascuantitativasparaespaciosdeestadosnotratables
AT paveseesteban quantitativeguaranteesforintractablestatespaces
_version_ 1807315774004527104
spelling todo:tesis_n5849_Pavese2023-10-03T13:01:57Z Garantías cuantitativas para espacios de estados no tratables Quantitative guarantees for intractable state spaces Pavese, Esteban MODELADO PROBABILISTICO VERIFICACION PROBABILISTICA SIMULACIONES VERIFICACION ESTADISTICA EXPLORACION PARCIAL PROBABILISTIC MODELLING PROBABILISTIC VALIDATION MODEL SIMULATION STATISTICAL METHODS PARTIAL EXPLORATIONS Los lenguajes basados en máquinas de estados finitos (también llamadosautomátas finitos) son usados de manera ubicua para la especificación desistemas de software. La formalidad de estos modelos permite la aplicación de técnicasde validación tales como el model checking. De esta manera, pueden respondercon 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 comportamientosaislados mediante varias máquinas, y estableciendo el comportamientoglobal 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 dependientesde la validez de las propiedades en cada componente. Sin embargo, este enfoque esamenazado por la complejidad del sistema especificado, dando lugar al problema dela 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, proveyendoinformación cuantitativa respecto de la propiedad que se intentó validar sinéxito. Nuestro enfoque se sostiene sobre dos contribuciones distintas, donde cada unade ellas puede, además, ser aplicada en el contexto de problemas relacionados. Estatesis se inspira en el modelado y model checking probabilísticos, que pueden proveerinformación cuantitativa respecto de la validez de una propiedad. Esta cuantificaciónnos sirve de validación parcial en el contexto del problema que nos interesa. Sin embargo, un enfoque composicional tiene sus propios problemas en un contextoprobabilístico. Las anotaciones probabilísticas asociadas a eventos independientesprecisan ser contrastadas con estimaciones obtenidas de la observación del comportamientoa modelar. Al agregar estas anotaciones, es preciso distinguir las fuentes deestas probabilidades; en otras palabras, las probabilidades de eventos independientesdeberían estar asociadas al comportamiento de los componentes que generan estecomportamiento. A su vez, es preciso mantener la relación entre la validez de loscomponentes de manera aislada, y la validez de los comportamientos en el sistemacompuesto. Los formalismos disponibles al momento, sin embargo, no proveen la seguridadde 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 alformalismo de Interface Automata. Esta extensión asegura la preservación de comportamientotal como es observado por la lógica probabilística pCTL. La segunda parte de esta tesis apunta al análisis de estos modelos, en particularcuando un análisis exhaustivo no es factible, teniendo en cuenta que la complejidaddel model checking probabilístico es aún mayor que en el caso clásico. Nuestra hipótesisen 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 puedeser más efectivo que tanto el model checking exhaustivo como así también enfoquesestadísticos relacionados. System specifications have long been expressed through automatabasedlanguages, 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 temporalproperties. Additionally, a compositional approach to construction of softwarespecifications reduces the specification effort, allowing the engineer to focus on specifyingindividual component behaviour; and then analyse the composite system behaviour. This also reduces the validation effort, since the validity of the compositespecification should be dependent on the validity of the components. However, evenin a compositional approach, automatic validation techniques usually cannot copewith systems under analysis that grow complex enough. Problems such as statespace explosion seriously hamper the applicability of these approaches. In this thesis, we present an approach that can help cope with these absenceof results by providing quantitative validation information related to the propertybeing validated, even when the model checking approach is unable to handle thewhole system. Our proposed technique stands on two different approaches, witheach of them being applicable on its own to related problems. The inspiration is thatprobabilistic modelling and checking can provide quantitative information, which canin turn serve as partial validation when full checking is infeasible. Compositional construction, however, poses additional challenges in a probabilisticsetting. Numerical annotations of probabilistically independent events must becontrasted against estimations or measurements, taking care of not compoundingthis quantification with exogenous factors, in particular other system components’behaviour. The validity of compositionally constructed specifications requires thatthe validated probabilistic behaviour of each component continues to be preserved inthe composite system. However, existing probabilistic automata-based formalismsdo not support behaviour preservation of non-deterministic and probabilistic componentsover their composition. The first contribution of this thesis is a probabilisticextension to Interface Automata which preserves pCTL properties. This extensionnot only supports probabilistic behaviour but also allows for weaker prerequisites tointerfacing composition, allowing for specification refinement of internal behaviour. The second part of our approach aims at analysing these probabilistically enrichedmodels, obtaining quantitative information that can be related to the validity of theproperty under analysis, even when a complete analysis is infeasible. Computationalcomplexity of estimating these metrics can be prohibitive, even more so than classicmodel checking. Our hypothesis is that a (carefully crafted) partial systematic explorationof a system model can provide better bounds for these quantitative modelmetrics at lower computation cost than exhaustive exploration. Our technique combinessimulation, invariant inference and probabilistic model checking to produce aprobabilistically 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 bemore effective than (full model) probabilistic and statistical model checking. Fil: Pavese, Esteban. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. 2015-10-19 Tesis Doctoral PDF Español info:eu-repo/semantics/openAccess https://creativecommons.org/licenses/by-nc-sa/2.5/ar https://hdl.handle.net/20.500.12110/tesis_n5849_Pavese

Ejemplares similares