Registro completo de metadatos
| Campo DC | Valor | Lengua/Idioma |
|---|---|---|
| dc.provenance | Facultad de Ciencias Exactas y Naturales de la UBA | - |
| dc.contributor | Braberman, Víctor | - |
| dc.contributor | Pavese, Esteban | - |
| dc.creator | Pavese, Esteban | - |
| dc.date.accessioned | 2018-05-04T22:02:49Z | - |
| dc.date.accessioned | 2018-05-28T16:57:33Z | - |
| dc.date.available | 2018-05-04T22:02:49Z | - |
| dc.date.available | 2018-05-28T16:57:33Z | - |
| dc.date.issued | 2015-10-19 | - |
| dc.identifier.uri | http://10.0.0.11:8080/jspui/handle/bnmm/75307 | - |
| dc.description | 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. | - |
| dc.description | 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. | - |
| dc.description | Fil:Pavese, Esteban. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. | - |
| dc.format | application/pdf | - |
| dc.language | spa | - |
| dc.publisher | Facultad de Ciencias Exactas y Naturales. Universidad de Buenos Aires | - |
| dc.rights | info:eu-repo/semantics/openAccess | - |
| dc.rights | http://creativecommons.org/licenses/by/2.5/ar | - |
| dc.source.uri | http://digital.bl.fcen.uba.ar/gsdl-282/cgi-bin/library.cgi?a=d&c=tesis&d=Tesis_5849_Pavese | - |
| dc.subject | PROBABILISTIC MODELLING | - |
| dc.subject | PROBABILISTIC VALIDATION | - |
| dc.subject | MODEL SIMULATION | - |
| dc.subject | STATISTICAL METHODS | - |
| dc.subject | PARTIAL EXPLORATIONS | - |
| dc.subject | MODELADO PROBABILISTICO | - |
| dc.subject | VERIFICACION PROBABILISTICA | - |
| dc.subject | SIMULACIONES | - |
| dc.subject | VERIFICACION ESTADISTICA | - |
| dc.subject | EXPLORACION PARCIAL | - |
| dc.title | Garantías cuantitativas para espacios de estados no tratables | - |
| dc.title | Quantitative guarantees for intractable state spaces | - |
| dc.type | info:eu-repo/semantics/doctoralThesis | - |
| dc.type | info:ar-repo/semantics/tesis doctoral | - |
| dc.type | info:eu-repo/semantics/publishedVersion | - |
| Aparece en las colecciones: | FCEN - Facultad de Ciencias Exactas y Naturales. UBA | |
Ficheros en este ítem:
No hay ficheros asociados a este ítem.