Lenguaje z

Testing Basado en Especificaciones Z
Maximiliano Cristi´ a Ingenier´ de Software ıa Facultad de Ciencias Exactas, Ingenier´ y Agrimensura ıa Universidad Nacional de Rosario 2010
Resumen En este apunte de clase se explica una t´cnica particular de testing basado en especificaciones e Z. Esta t´cnica permite efectuar un testing muy completo, riguroso y disciplinado de un sistema e del cual se poseeun modelo Z. No se incluyen ejercicios, para ello ver la pr´ctica correspondiente. a

´ Indice
1. Introducci´n o 1.1. Programas y especificaciones . . . . . . . . . 1.2. Casos de prueba exitosos, espacio v´lido de a abstracci´n . . . . . . . . . . . . . . . . . . o 1.3. El proceso de MBT . . . . . . . . . . . . . . 2. Generaci´n de casos de prueba abstractos o 3. T´cticas de MBT a 3.1. Elejemplo . . . . . . . . . . . . . . . . 3.2. IS y VIS de Extraer . . . . . . . . . . 3.3. Forma Normal Disyuntiva (FND) . . . 3.4. Particiones Est´ndar (PE) . . . . . . . a 3.5. Propagaci´n de Sub-Dominios (PSD) . o 3.6. Mutaci´n de Especificaciones (ME) . . o 3.7. Causa-efecto (CE) . . . . . . . . . . . 3.8. Otras t´cticas . . . . . . . . . . . . . . a 3.8.1. Tipos Libres (TL) . . . . . . . . 3.8.2. L´ımites de Implementaci´n (LI) o 4. El ´rbol de pruebas a 5. Selecci´n de casos de prueba abstractos o . . . . . entrada . . . . . . . . . . . y . . . . . . . . funciones . . . . . . . . . . . . . . . . . . . . . de refinamiento . . . . . . . . . . . . . . . . . . . . y . . . . 2 2 2 3 3 6 6 8 8 10 12 16 17 18 19 19 20 20

. . . . . . . . . .

. . . . . . . . . .

. . . . . . . . . .

. . .. . . . . . .

. . . . . . . . . .

. . . . . . . . . .

. . . . . . . . . .

. . . . . . . . . .

. . . . . . . . . .

. . . . . . . . . .

. . . . . . . . . .

. . . . . . . . . .

. . . . . . . . . .

. . . . . . . . . .

. . . . . . . . . .

. . . . . . . . . .

. . . . . . . . . .

. . . . . . . . . .

. . . . . . . . . .

. . . . . . . . . .

. . . . . . .. . .

. . . . . . . . . .

. . . . . . . . . .

. . . . . . . . . .

. . . . . . . . . .

. . . . . . . . . .

1

1.

Introducci´n o

En este cap´ ıtulo veremos con detalle una t´cnica especial de testing basado en modelos (MBT). e La t´cnica se denomina Test Template Framework (TTF) y fue propuesta por Phil Stocks y David e Carrington a mediados de los noventa, e implementadade forma autom´tica por primera vez reciena TM temente en Fastest por el autor, Pablo Rodr´ ıguez Monetti y Pablo Albertengo [CR09, CAR10]1 . El TTF se aplica especialmente a especificaciones Z, aunque puede utilizarse con otros formalismos. Luego de abordar los aspectos te´ricos de esta t´cnica los aplicaremos en la herramienta FastestTM o e la cual permite automatizar gran parte de la tarea.1.1.

Programas y especificaciones

Un programa es correcto si verifica su especificaci´n. Por ende, para poder efectuar un testing o significativo es necesario contar con alguna especificaci´n del programa que se quiere probar. De lo o contrario cualquier resultado que arroje el programa ante un caso de prueba no se sabr´ si es correcto a o no. La especificaci´n puede ser de cualquier tipo (formal,semi-formal o informal) e incluso puede o no estar escrita (la conoce el programador o el usuario). En algunos casos esta especificaci´n est´ tan o a ausente o mal documentada que se la suele llamar or´culo de decisi´n, en clara alusi´n a alg´n a o o u mecanismo m´gico que permite determinar si el programa es correcto o no. Este apunte, obviamente, a presupone la existencia de una especificaci´n omodelo formal Z del programa que se quiere testear. o En Z la especificaci´n de un programa es un esquema de operaci´n. o o

1.2.

Casos de prueba exitosos, espacio v´lido de entrada y funciones de a refinamiento y abstracci´n o

Diremos que un caso de prueba es exitoso si descubre un error en el programa. Pero para saber si es exitoso o no debemos recurrir a la especificaci´n que es una...