Per capire l’importanza di questo argomento pensiamo di avere un codice concorrente scritto in un certo linguaggio, con l’utilizzo dei thread, con un produttore, un consumatore e un buffer. I primi due estendono la classe thread mentre il buffer ha i metodi synchronized per il prelevamento e il deposito. Questo codice simula il modello produttore-consumatore già approfondito. Bisogna capire se questo programma funzioni correttamente ma non posso usare le tecniche viste precedentemente per valutare la correttezza di programmi (logica di Hoare, ecc…) in quanto abbiamo a che fare con un programma che non inizia, produce dati e finisce ma, generalmente, si ha a che fare con un programma senza stato finale, che esegue infinitamente le sue parti in modo concorrente. Per il modello appena ipotizzato possiamo dire che è corretto se, ad esempio:

• ogni oggetto prodotto venga prima o poi consumato
• nessun oggetto venga consumato più di una volta
• il sistema non vada in deadlock

Pensiamo ora ad una rete di Petri “complessa” con due processi che condividono in un mutua esclusione una certa risorsa. Si ha quindi una sezione critica dove un processo usa tale risorsa. Possiamo volere, per esempio, che i due processi non siano mai contemporaneamente nella sezione critica (userebbero insieme la risorsa) e che prima o poi un processo entri in zona critica. Un metodo è controllare l’intero spazio delle marcature raggiungibili e verificare che tutto vada come voluto, per la prima richiesta, ma ci sono tecniche migliori.

Un altro caso d’uso è quello dei circuiti asincroni. Volendo si può adattare la logica di Hoare a modelli concorrenti ma solo se si ha comunque un output finale e non un’evoluzione ciclica infinita.

Logica LTL (Linear Temporal Logic)

Fino ad ora ci si è basati sulla logica proposizionale ma tale logica ha dei limiti, si introduce quindi la logica LTL che introduce il concetto di tempo, in ottica lineare, nel processo logico.

La logica LTL viene usata per model checking. Lo scopo generale che ci si propone è quello di presentare un approccio formale alla progettazione e all’implementazione di sistemi basati su un linguaggio formale che permetta di specificarli e ragionare sulle loro proprietà. Si vogliono studiare già sistemi grandi, come software o addirittura sistemi operativi, che piccoli, come per esempio una coppia di semafori. Tutti questi sistemi hanno però la medesima caratteristica, ovvero assumono in ogni istante di tempo un determinato stato definito dalle variabili del sistema stesso. Si hanno quindi nel sistema, in ogni istante di tempo:

• uno stato, univocamente definito dai valori delle variabili
• una transizione che segnala un passaggio da uno stato ad un altro
• una computazione che rappresenta una sequenza di stati di cui ogni coppia forma una transizione. Si introduce quindi il concetto temporale.

Il tempo viene pensato come un oggetto discreto, cadenzato dalle transizioni, su cui può essere definita anche una relazione d’ordine (potrebbe servire che un processo termini prima, dopo o nello stesso tempo di un altro).

Sistema reattivo

Definizione: Si definisce sistema reattivo una componente:

• non terminante e interattivo
• che può leggere il proprio input non solo all’inizio della computazione è che può produrre output non solo alla fine della sua computazione (si possono quindi avere multipli input e multipli output)