Métodos para la Verificación de Programas Concurrentes con aspectos Aleatorios y Temporizados
Introducción y Descripción
La interacción cotidiana con sistemas basados en computadoras es hoy un hecho inevitable. Podemos encontrar microprocesadores en electrónica de consumo (ej. TVs, reproductoras de video o CD), medios de transporte (ej. aviones, autos, controladores de diversos tipos de tráfico), sistemas de comunicación, plantas industriales, redes de computadoras, equipo médico, etc. El funcionamiento incorrecto de cualquiera de estos sistemas tiene una diversidad de consecuencias que varían desde una molestia en el usuario hasta situaciones que pueden poner en peligro la vida humana o inclusive generar serias catástrofes. Para la mayoría de tales sistemas, es crucial que ellos provean un servicio correcto y eficiente.
Los algoritmos aleatorios, en particular, presentan, en muchas ocasiones, soluciones más veloces que los algoritmos tradicionales y en otras, soluciones que no serían posibles dentro del dominio de lo algoritmos tradicionales [1,2]. De particular interés, son los algoritmos aleatorios concurrentes y/o distribuidos tales como los protocolos de elección de líder o los de acuerdo bizantino. Consideraremos también la posibilidad de que estos algoritmos deban incluir características temporales introducidas por el algoritmo mismo (como los timeouts) o por el contexto (ej. demora en transmisiones).
Model checking [3,4] es una técnica de verificación del tipo push-button, en el sentido de que dado el modelo del sistema bajo estudio, y la propiedad requerida sobre este, la técnica permite decidir automáticamente si la propiedad es satisfecha por este modelo o no.
Es nuestra intención el desarrollar técnicas y herramientas basadas en model checking para analizar la corrección de programas concurrentes temporizados con características aleatorias.
En particular, proponemos atacar el problema de la explosión de estados. Este problema, bien conocido y atacado en model checking, se magnifica en el ámbito de model checking cuantitativo (i.e. model checking de propiedades cuantificadas probabilísticamente). Los algoritmos de model checking cuantitativo, además de almacenar los estados en memoria deben resolver un sistema de optimización lineal donde cada variable esta asociada a un estado, y cada desigualdad a una transición probabilística. Asimismo planeamos implementar las técnicas estudiadas dentro en un model checker. Nos enfocaremos en extender el model checker Rapture [22,24].
Trabajos Relacionados y Metodología
Las primeras técnicas de model checking sobre programas probabilísticos concurrentes (o procesos de decisión de Markov [5]) sólo verificaban la validez de propiedades con probabilidad 1 (o no nula) [6,7,8]. Posteriormente se introdujo el model cecking cuantitativo en los cuales las propiedades incluían una construcción para cuantificar la probabilidad de su validez [9,10,11,12,13,14]. Basado en estas técnicas, se han desarrollado una diversidad de algoritmos y herramientas entre las que se incluyen [15,16,17,18,19,20,21,22,23,24,25,26].
Los BDDs (diagramas de decisión binaria) y en particular los MTBDDs (BDD con terminales múltiples) [27,28] son estructuras de datos que se han utilizado con éxito para la representación de grandes espacios de estados completos incluyendo el caso de model checking cuantitativo [18,23]. Sin embargo los MTBDDs no se comportan muy bien a la hora de solucionar sistemas de optimización lineal. Para atacar este problema, [19,20] presenta técnicas de abstracción que aproximan el resultado buscado mediante refinamientos sucesivos. Esta técnica, sin embargo, requiere la construcción del espacio de estados completo. Recientemente se introdujo una manera de generar directamente espacios de estados reducidos mediante la reducción de orden parcial [25,26], sólo que no utiliza abstracción. Para el caso de autómatas temporizados, la semántica de orden parcial a provisto el fundamento para algoritmos y estructuras de datos eficientes en la reducción de estados [30]. Otras técnicas que se pretende utilizar para atacar el problema de explosión de estado es la interpretación abstracta [29,31,32] y program slicing [33,34,35].
Tareas a Realizar y Resultados Esperados
La siguiente lista (no necesariamente exhaustiva) enumera las tareas a realizar.
- Aplicación de las técnicas presentadas en [19,20,25,26] para efectuar análisis de alcanzabilidad sobre autómatas temporizados con probabilidades.
- Extender las técnicas propuestas en [19,20,25,26] a propiedades de corrección expresadas en la lógica temporal LTL, y luego incluir el ingrediente temporal.
- Explorar la aplicabilidad de técnicas de program slicing e interpretación abstracta al model checking cuantitativo.
- Explorar la posibilidad de utilizar estas mismas técnicas para análisis de desempeño (performance analysis).
- Implementación de los resultados fundamentales.
- Análisis de casos de estudios que ayuden a evaluar el desempeño de la herramienta desarrollada.
Los resultados esperados de mínima incluyen la resolución de los puntos 1 y 2 (nótese que la técnica de reducción de orden parcial [25,26] es ortogonal a la de abstracción y refinamiento [19,20]). Además se espera la implementación de la reducción de orden parcial en RAPTURE [22,24] la cual ya implementa abstracción y refinamiento, y la implementación (parcial) de los resultados de 1 y 2.
Antecedentes en la Cooperación
Ver referencias [19,20,22,24,25]. Además, el Dr. D’Argenio trabajó en el LIF, CMI, Université de Provence dentro del proyecto Europeo AMETIST junto al Dr. Niebert entre Setiembre de 2003 y Agosto de 2004.
Referencias
[1] R. Gupta, S.A. Smolka, y S. Bhaskar. On
randomization in sequential and distributed algorithms. ACM
Comp. Surveys, 26(1):7--86, 1994.
[2] R. Motwani y P. Raghavan. Randomized Algorithms.
Cambridge University Press, 1995.
[3] E.M. Clarke, O. Grumberg, y D. Peled. Model Checking.
MIT Press, 1999.
[4] B. Berard, M. Bioit, A. Finkel, F. Laroussinie, A.
Petit, L. Petrucci, Ph. Schnoebelen, y P. McKenzie. Systems
and Software Verification: Model-Checking Techniques and
Tools. Springer-Verlag, 2001
[5] M.L. Puterman. Markov Decision Processes: Discrete
Stochastic Dynamic Programming. John Wiley & Sons,
1994.
[6] M.Y. Vardi. Automatic verification of probabilistic
concurrent finite state programs. En 26th FOCS, pp.
327--338. IEEE Press, 1985.
[7] C. Courcoubetis y M. Yannakakis. Verifying temporal
properties of finite-state probabilistic processes. En 29th
FOCS, pp. 338--345. IEEE Press, 1988.
[8] C. Courcoubetis y M. Yannakakis. The complexity of
probabilistic verification. J. of the ACM, 42(4):857--907,
1995.
[9] H.A. Hansson. Time and Probability in Formal Design of
Distributed Systems. Elsevier, 1994.
[10] A. Bianco y L. de Alfaro. Model checking of
probabilistic and nondeterministic systems. En P.S.
Thiagarajan, ed., Proc. of FST&TCS'95, LNCS 1026, pp.
499--513. Springer-Verlag, 1995.
[11] L. de Alfaro. Formal Verification of Probabilistic
Systems. Tesis Doctoral, Stanford University, 1997.
[12] L. de Alfaro Temporal logics for the specification of
performance and reliability. En R. Reischuk y M. Morvan,
eds., Proc. STACS'97, LNCS 1200, pp. 165--176, Lübeck,
Germany, 1997. Springer-Verlag.
[13] C. Baier y M. Kwiatkowska. Model checking for a
probabilistic branching time logic with fairness.
Distributed Computing, 11(3):125--155, 1998.
[14] C. Baier. On Algorithmic Verification Methods for
Probabilistic Systems. Habilitation thesis, University of
Mannheim, 1999.
[15] M. Huth y M. Kwiatkowska. Quantitative analysis and
model checking. En Proc. of the 12th LICS. IEEE Press,
1997.
[16] V. Hartonas-Garmhausen y S. Campos. ProbVerus:
Probabilistic symbolic model checking. En J.-P. Katoen,
ed., Proc. of the 5th ARTS, LNCS 1601. Springer-Verlag,
1999.
[17] M. Kwiatkowska, G. Norman, R. Segala, y J. Sproston.
Automatic Verification of Real-Time Systems with
Probability Distributions. En J.-P. Katoen, ed., Proc. of
the 5th ARTS, LNCS 1601, pp. 75--95. Springer-Verlag, 1999.
[18] L. de Alfaro, M. Kwiatkowska, G. Norman, D. Parker, y
R. Segala. Symbolic model checking of concurrent
probabilistic processes using MTBDDs and the Kronecker
representation. En S. Graf y M. Schwartzbach, eds., Proc.
of TACAS 2000, LNCS 1785. Springer-Verlag, 2000.
[19] P.R. D'Argenio, B. Jeannet, H.E. Jensen, y K.G.
Larsen. Reachability analysis of probabilistic systems by
successive refinements. En Proc. of PAPM/PROBMIV 2001, LNCS
2165, pp. 39--56. Springer-Verlag, 2001.
[20] P.R. D'Argenio, B. Jeannet, H.E. Jensen, y K.G.
Larsen. Reduction and refinement strategies for
probabilistic analysis. En H. Hermanns y R. Segala, eds.,
Proc. of PAPM/PROBMIV 2002, LNCS 2399. Springer-Verlag,
2002.
[21] M. Kwiatkowska, G. Norman, y D. Parker. PRISM:
Probabilistic symbolic model checker. En TOOLS'2002, LNCS
2324. Springer-Verlag, 2002.
[22] B. Jeannet, P.R. D'Argenio, y K.G. Larsen. Rapture: A
tool for verifying Markov decision processes. En I. Cerna,
ed., Proc. of the Special Tools Day at CONCUR 2002, Tech.
Rep. Fac. of Informatics, Masaryk University Brno, 2002.
[23] Prism web page. http://www.cs.bham.ac.uk/~dxp/prism/.
[24] Rapture web page. http://www.irisa.fr/prive/bjeannet/prob/prob.html.
[25] P.R. D'Argenio y P. Niebert. Partial order reduction
for concurrent probabilistic programs. En Proc of QEST04.
IEEE press, 2004. To appear.
[26] C. Baier, M. Größer, y F. Ciesinski. Partial order
reduction for probabilistic systems. En Proc of QEST04.
IEEE press, 2004. To appear.
[27] R.I. Bahar, E.A. Frohm, C.M. Gaona, G.D. Hachtel, E.
Macii, A. Pardo, y F. Somenzi. Algebraic decision diagrams
and their applications. Formal Methods in System Design,
10(2/3):171--206, 1997.
[28] M. Fujita, P.C. McGeer, y J.C.-Y. Yang. Multi-terminal
binary decision diagrams: An efficient data structure for
matrix representation. Formal Methods in System Design,
10(2/3):149--169, 1997.
[29] P. Cousot y R. Cousot. Abstract interpretations: A
unified lattice model for static analysis of programs by
construction or approximation of fixpoints. En Proc. of the
4th POPL, 1977.
[30] D. Lugiez, P. Niebert, y S. Zennou. A Partial Order
Semantics Approach to the Clock Explosion Problem of Timed
Automata. En Proc. of TACAS 2004. LNCS, Springer-Verlag.
[31] N.D. Jones y F. Nielson. Abstract interpretation:
Semantics-based tools for program analysis. En S. Abramsky,
D. Gabbay, y T. Maibaum, eds., Handbook of Logic in
Computer Science, Vol 4, pp. 527--636. Oxford Univ. Press,
1995.
[32] D. Schmidt y B. Steffen. Program analysis as model
checking of abstract interpretation. En Proc. SAS'98, LNCS
1503, pp. 351--380. Springer-Verlag, 1998.
[33] F. Tip. A survey of program slicing techniques.
Journal of Programming Languages, 3:121--189, 1995.
[34] L.I. Millet y T. Teitelbaum. Slicing Promela and its
application to model checking, simulation, and protocol
understanding. En Proc. of 4th SPIN Workshop, 1998.
[35] E.M. Clarke, M. Fujita, S.P. Rajan, T. Reps, S.
Shankar, y T. Teitelbaum. Program slicing of hardware
description languages. En Proc. of CHARME'99, LNCS 1703,
pp. 298--312. Springer-Verlag, 1999.