Teoria di testing

Il comportamento esterno di programmi o processi, e più in generale di sistemi, può essere investigato tramite l'utilizzo di una serie di test. Risulta inoltre importante non soltanto sapere se, dato un particolare test, un processo risponde favorevolmente oppure no, ma anche se il processo risponde in maniera consistente ogni volta che il test viene eseguito.

Possiamo pensare, in generale, ad un insieme di processi e ad un insieme di test; due processi saranno equivalenti (rispetto a questo insieme di test) se superano esattamente gli stessi test. Questa naturale equivalenza può essere divisa in due preordini sui processi: il primo formulato in termini dell'abilità di rispondere positivamente ad un particolare test il secondo in termini dell'impossibilità di non rispondere positivamente ad un particolare test; nell'ultimo caso vedremo come un processo p sia meno di un processo q se, per ogni test a qui p risponde positivamente, anche q risponde positivamente. Attraverso la congiunzione di questi due preordini se ne otterrà un terzo, quello che caratterizza l'impianto teorico che stiamo discutendo.

Iniziamo dunque ad introdurre con maggior dettaglio quello di cui ci occuperemo:

Processi:

un insieme di termini chiusi sull'alfabeto ${Act}_{\tau}$. L'insieme viene indicato come $\mathcal{P}$;

Osservatori:

un insieme di termini chiusi sull'alfabeto ${Act}_{\tau} \cup \{ w \}$ con $w \: \not\in \: {Act}_{\tau}$ indicato con $\mathcal{O}$.

Stati:

sono coppie $<p,o>$ dove $p$ è lo stato di un processo e $o$ è lo stato di un osservatore. Uno stato si dice soddisfatto se $o$ può compiere un'azione $w$.

Computazione:

dato un processo $p \: \in \: \mathcal{P}$ ed un osservatore $o \: \in \: \mathcal{O}$ rispettivamente con stato iniziale $p$ ed $o$ si definisce una computazione da $<p,o>$ come una sequenza finita od infinita di stati $<p_n,o_n>$ dove:

1. $<p_0,o_0>$ corrisponde a $<p,o>$;

2. i) $<p_n,o_n> \stackrel{\tau}{\longrightarrow} <p_{n+1},o_{n+1}>$ se $p_n \stackrel{\tau}{\longrightarrow} p_{n+1}$ e $o_n = o_{n+1}$ oppure $o_n \stackrel{\tau}{\longrightarrow} o_{n+1}$ e $p_n = p_{n+1}$
   ii) $<p_n,o_n> \stackrel{\alpha}{\longrightarrow} <p_{n+1},o_{n+1}>$ se $p_n \stackrel{\alpha}{\longrightarrow} p_{n+1}$ e $o_n \stackrel{\alpha}{\longrightarrow} o_{n+1}$

3. Se la sequenza è finita allora l'ultimo elemento $<p_k,o_k> \stackrel{\mu}{\not\rightarrow}$ per ogni $\mu \in Act_{\tau}$.

Come detto, un osservatore è un processo che esegue test su altri processi comunicando con essi, in un certo senso guidandone l'esecuzione. Un test su un processo avrà esito positivo se il suo osservatore raggiunge uno stato in cui può eseguire l'azione $w$, che comunica il successo.

Definizione 7..1 (Osservazione)   Dato un processo P con alfabeto $Act_{\tau}$ e un osservatore O con alfabeto $Act_{\tau} \cup \{w\}$ un'osservazione è una sequenza del tipo:

$$P\vert O=P_{0}\vert O_{0} \stackrel{\tau}{\rightarrow}P_{1}\vert... ... \stackrel{\tau}{\rightarrow}P_{n}\vert O_{n}\stackrel{\tau}{\not\rightarrow}$$

cioè una sequenza di transizioni $\tau$ o $w$.

Un'osservazione si dice soddisfacente se $\exists i \: : \: O_i \stackrel{w}{\rightarrow}$, cioè se esiste uno stato in cui l'osservatore è soddisfatto; questa definizione non implica l'arresto dell'osservazione, ma richiede che si sia passati per uno stato che consentiva di eseguire un'azione $w$

Da quanto detto finora possiamo introdurre due concetti importanti per il proseguio:

Definizione 7..2   Siano $P$ e $O$ rispettivamente un processo ed un osservatore, allora:

i) P may satisfy O se esiste una sequenza $s \in {Act}^*$ tale che $p_0 \stackrel{s}{\Rightarrow}$, $o_0 \stackrel{s}{\Longrightarrow}o_n$ e $o_n\stackrel{w}{\rightarrow}$;

ii) P must satisfy O se per ogni computazione $<p_0,o_0> \stackrel{\mu_1}{\longrightarrow} <p_1,o_1> \stackrel{\mu_2}{\longrightarrow} \dots$ $\exists n \geq 0$ tale che $o_n\stackrel{w}{\rightarrow}$

La definizione sopra indica che un processo may satisfy un osservatore se esiste un'osservazione soddisfacente per $P\vert O$, mentre must satisfy un osservatore se tutte le osservazioni per $P\vert O$ sono soddisfacenti.

Con l'introduzione di may/must satisfy è possibile introdurre i tre preordini di questa teoria:

Definizione 7..3   Sia $\mathcal{O}$ l'insieme degli osservatori, allora si possono definire i seguenti preordini sui processi:

• $P \sqsubseteq_{may}Q$ sse $\forall O \in \mathcal{O} \quad$ P may satisfy O $\Rightarrow$ Q may satisfy O

• $P \sqsubseteq_{must}Q$ sse $\forall O \in \mathcal{O} \quad$ P must satisfy O $\Rightarrow$ Q must satisfy O

• $P \sqsubseteq_{test}Q$ sse $P \sqsubseteq_{may}Q \: \land \: P \sqsubseteq_{must} Q$

Definiti i preordini, prendendone il kernel, possiamo ottenere le relazioni di equivalenze corrispondenti:

Definizione 7..4   Le relazioni di equivalenza sono:

• $P \simeq_{may}Q$ sse $(P \sqsubseteq_{may}Q) \land (Q \sqsubseteq_{may}P)$

• $P \simeq_{must}Q$ sse $(P \sqsubseteq_{must}Q) \land (Q \sqsubseteq_{must}P)$

• $P \simeq_{test}Q$ sse $(P \simeq_{may}Q) \land (P \simeq_{must}Q)$