Un esecutore di specifiche logiche in tempo reale

Capitolo 1
Introduzione
Come il linguaggio naturale traccia i confini della conoscenza comunicabile da uomo a uomo,
cos` ı i linguaggi formali delimitano i possibili contenuti della comunicazione tra uomo e macchina.
Solitamente, questa comunicazione ha come oggetto pi` u o meno esplicito un desiderio umano
che la macchina dovr` a soddisfare. Nonostante essa sia sempre fedele nella sua esecuzione, non
tutti i desideri si realizzano. Come in una famosa favola, il genio esegue alla lettera quanto
richiesto e quando il risultato non ` e quello gradito, al protagonista non resta che prendersela con
sestesso. A ben guardare egli potrebbe invocarenumeroseattenuanti, perch´ eper ogniformalismo
esistono problemi abbastanza complessi da non ammettere soluzioni la cui formulazione sia di per
s` e evidentemente corretta. La soglia di complessit` a sopra cui il semplice esame della soluzione
non ` e sufficiente a determinarne la correttezza pu` o invece variare notevolmente con il livello del
linguaggio in cui viene espressa. Tra i requisiti che ogni linguaggio formale dovrebbe soddisfare, i
seguenti sono indici di un livello elevato:
• Espressivit` a: deve essere possibile rappresentare i propri desideri
• Precisione: i desideri devono essere rappresentabili senza ambiguit` a
• Astrazione dal dettaglio: non deve essere necessario rappresentare dettagli ininfluenti
• Compattezza: la rappresentazione deve essere ragionevolmente breve
• Leggibilit` a: la rappresentazione deve essere comprensibile per altri lettori
Un modo abbastanza naturale di conseguire il risultato desiderato ` e quello di impartire alla
macchina una successione di comandi elementari riconosciuti che conduce all’obiettivo. Questa
` e l’essenza della programmazione imperativa ed i linguaggi formali attraverso cui si esprime, dal
codice macchina a quelli ad oggetti, sono detti semplicemente “di programmazione”. Al crescere
del loro livello si ` e per` o accompagnata una sempre maggiore rilevanza della sezione dichiarativa
del programma, quella cio` e in cui si descrivono gli enti coinvolti nell’esecuzione, rispetto a quel-
la imperativa. Nel frattempo, da istruzioni modellate sulla struttura dell’hardware ci si ` e pian
piano elevati verso una sintassi che ricalca le forme del pensiero, come avviene nei linguaggi di
programmazionelogicachesiispiranoalcalcolodeipredicatidelprimoordine. Questiultimisono
particolarmente importanti perch´ e ` e possibile utilizzarli per scrivere programmi che ammettono
una interpretazione completamente dichiarativa, cio` e che possono essere letti come la definizione
di un insieme di relazioni priva di qualunque comando esplicito. I linguaggi di programmazione
logica permettono quindi un diverso stile di scrittura, detto appunto dichiarativo, che conferisce
al programma propriet` a rilevanti quali la possibilit` a di essere fuso con un diverso programma
conservando la propria semantica.
Parallelamenteailinguaggidiprogrammazionesisviluppavaunadiversacategoriadilinguaggi
formali,detti“dispecifica”,ilcuiscopo` equellodiconsentireunadefinizionerigorosadell’obiettivo
da raggiungere, a prescindere dalla strada che verr` a in effetti seguita. Le specifiche scritte facendo
1
CAPITOLO 1. INTRODUZIONE
uso di questi linguaggi sono poi utilizzate per verificare la consistenza dei vincoli di progetto e la
loro successiva soddisfazione, possibilmente attraverso validatori automatici. In un certo senso,
un programma logico ` e un particolare tipo di specifica eseguibile ed ` e ragionevole chiedersi se
esistano algoritmi di esecuzione anche per altri linguaggi di specifica, con lo scopo di utilizzarli
come linguaggi di programmazione dichiarativa. Questo approccio garantirebbe automaticamente
la soddisfazione dei vincoli specificati, eliminando la fase di implementazione degli algoritmi in un
linguaggio convenzionale.
L’affidabilit` a del software, cio` e la garanzia del corretto funzionamento di un programma per
tutti i possibili ingressi, ` e uno dei problemi aperti dell’ingegneria. Nel controllo di sistemi com-
plessi, ad esempio, il punto debole solitamente non ` e costituito dall’hardware, per cui esistono
metodologie di verifica affermate, quanto dal software preposto alla sua gestione. Per contribuire
a risolvere questo problema si possono adottare linguaggi in cui i programmi fanno quello che
dicono di fare, cio` e il cui significato estensionale, l’insieme di tutte le possibili esecuzioni, ` e au-
toevidente dato il sorgente del programma stesso fino ad un grado ragionevole di complessit` a.
Un linguaggio di specifica potrebbe essere un ottimo candidato a questo ruolo in quanto mette
l’accentosull’obiettivoanzich´ esulmetodo, purdidisporredell’opportunoalgoritmodiesecuzione.
Un comune pregiudizio nei confronti della programmazione dichiarativa` e la sua presunta scar-
sa efficienza. In parte, questo ` e conseguenza di un suo uso troppo libero, oltre i limiti suggeriti
dall’implementazione. Inaltreparole,nontuttoci` ochesipu` oscrivereinunlinguaggiodispecifica
potr` a essere eseguito con ragionevole efficienza, ma di solito esiste un modo per scrivere quelle
stesse cose nel medesimo linguaggio tale da farle eseguire con elevata efficienza. Ad esempio, nella
programmazione logica le prestazioni dipendono dal grado di determinismo che viene specifica-
to durante la scrittura o semplicemente da un diverso ordinamento delle clausole. Non sfugge
comunque il vantaggio insito nel disporre di un linguaggio in cui si possono scrivere programmi
che fanno quello che dicono di fare, indipendentemente dall’efficienza con cui questo ` e in effetti
possibile. Un passo ulteriore pu` o essere infatti la riscrittura di un programma poco efficiente in
uno migliore nello stesso linguaggio, magari condotta con ottimizzatori automatici per garantirne
la correttezza.
Astrazioneeprestazioniinesecuzionesonofattorigeneralmentecostrastanti,esolounaccurato
bilanciamentotraquestiinvistadiuncertoambitodiapplicazionepu` oportarestrumentiutiliallo
sviluppo di software pi` u affidabile. In questa tesi si cercher` a di sfatare il pregiudizio che vorrebbe
i programmi dichiarativi poco prestanti scegliendo un ambito di applicazione particolarmente
ostile, ilcontrollodisistemiintemporeale. Alsoftwaredigestionediunmicrocontrollore` einfatti
richiesto di garantire:
• Produzione di uscite corrette per tutte le possibili storie degli ingressi
• Disponibilit` a delle uscite entro un tempo prefissato dall’istante di acquisizione degli ingressi
Inoltre, dato che tipicamente esso viene impiegato in apparecchiature di largo consumo e non
` e suscettibile di facile aggiornamento, ` e comprensibile che il mondo dell’industria non si accon-
tenti della soddisfazione pratica dei due requisiti precedenti ma sempre pi` u spesso ne richieda
la dimostrabilit` a. Un programmatore capace pu` o ottenere il risultato sperato anche attraverso
un linguaggio convenzionale, ma difficilmente il codice prodotto si prester` a ad alcuna forma di
dimostrazione rigorosa.
L’approcciotradizionaleallosviluppodiunsimilesoftware` eoperazionale,nelsensocherichiede
una modellazione esplicita della successione dei passi di esecuzione, e si basa su formalismi quali
macchine a stati, reti di Petri o loro varianti. Alternativamente sono utilizzati metodi descrittivi
basati su linguaggi di specifica quali lo Z o svariate logiche temporali, come la TILCO da cui
trae ispirazione la logica ridotta che verr` a impiegata nel seguito. Evidentemente questi ultimi
metodiconsentonounamaggioreastrazione,manonassicuranol’effettivaeseguibilit` adelrisultato.
D’altra parte, neppure impongono una particolare strategia di esecuzione e questo apre la strada
alla ricerca di algoritmi in grado di garantire il rispetto dei vincoli temporali assegnati.
L’obiettivo di questa tesi ` e appunto la realizzazione di uno strumento in grado di eseguire la
specifica logica di un sistema causale in tempo reale, cos` ı da garantirne l’applicabilit` a ingegneri-
2
CAPITOLO 1. INTRODUZIONE
stica. Eseguire la specifica di un sistema significa a tutti gli effetti riprodurne il comportamento a
partire dalla sua definizione in un certo linguaggio formale. Questo si realizza grazie ad un motore
d’inferenza che, in ogni istante di tempo, produce conseguenze logiche implicate dalla specifica,
assunta vera, data la conoscenza acquisita fino a quello stesso istante. Non tutte le specifiche
risulteranno per` o eseguibili. Assumendo la correttezza dell’algoritmo di esecuzione, le possibili
cause di ineseguibilit` a sono:
• Specifica del sistema non soddisfacibile
• Specifica del sistema incompleta
• Sistema specificato non causale
• Algoritmo di esecuzione incompleto
Agli errori di specifica si rimedia riscrivendo la stessa con maggiore attenzione, mentre la non
causalit` adelsistemarendevanoognitentativodiriprodurneilcomportamentointemporeale. Per
quanto riguarda l’algoritmo di esecuzione, la sua incompletezza` e solitamente il prezzo che si paga
all’efficienza dato che qualunque algoritmo completo in grado di risolvere un generico problema di
soddisfacibilit` a ha complessit` a esponenziale. Questo` e il limite pi` u evidente dei metodi descrittivi,
poich´ e rende incerta la produzione di un risultato desiderato anche quando ` e conseguenza logica
dellaspecificadaeseguire. Tuttavialaprogrammazionedichiarativa` eampiamenteutilizzatagrazie
ad un approccio misto che non perde di vista il significato operazionale che si nasconde dietro alla
descrizionedelsistemaspecificatoeconduceallasceltadiunaformaespressivaingradodigarantire
l’eseguibilit` a. Inquestocaso,l’algoritmodiesecuzionedeveesserestabilitoprecedentementeperch´ e
sia possibile aggirarne l’incompletezza durante la stesura della specifica. Nei comuni motori di
inferenza per la programmazione logica, ad esempio, la ricerca in profondit` a sull’albero delle
scelte costringe il programmatore ad assicurarsi che questo non contenga cammini infinitamente
lunghi, fruttodidefinizioniricorsivemagaricorrettemacertoeccessivamentecontorte. Perquesta
ragione, il motore di inferenza prescelto ` e abbastanza semplice da poterne simulare manualmente
il funzionamento nei casi di dubbia eseguibilit` a e consentire quindi una programmazione mirata.
In particolare si ` e preferito un tradizionale sistema di ragionamento in avanti, cio` e basato su
regoledeltipopremesse ‘conclusioni,aimetodidiricercalegatiall’obiettivo,accettandoilprezzo
di incompletezza derivante da questa scelta pur di poter enunciare una condizione che garantisse
il funzionamento dell’esecutore in tempo reale. Ci` o ` e reso possibile dalla strategia adottata per
selezionare le clausole su cui fare inferenza, che ` e invece del tutto originale e pu` o essere applicata
con identici risultati a qualunque sistema di ragionamento in avanti, purch´ e in ogni sua regola
le premesse descrivano istanti di tempo non successivi a quelli descritti dalle conclusioni. La
letteratura non presenta risultati simili e si ` e ritenuto opportuno formalizzarli, sviluppando una
teoria assai generale che combina inferenza ed acquisizione di ingressi che variano nel tempo.
Questa teoria prescinde dalla particolare modalit` a di rappresentazione della conoscenza e dalle
regole di inferenza implementate.
Successivamentesi` eintrodottounformalismoinnovativoperrappresentareivalorilogicidiun
insiemediclausoleattraversol’orientazionedegliarchidiunaspecialerete,abbastanzamaneggevo-
le da ammettere un utilizzo manuale ma anche adatta a costituire un formato di rappresentazione
della conoscenza per il motore di inferenza precedentemente proposto. Inizialmente a questa re-
te ` e associata una semantica puramente descrittiva, legata alla sintassi della specifica, ma una
volta fissate le regole di inferenza la sua interpretazione operazionale ` e immediata e ne consen-
te una pi` u libera e proficua manipolazione, agevolata dalla notazione grafica adottata. Questa
duplice natura la rende uno strumento particolarmente adatto ad un approccio misto durante la
stesura di specifiche eseguibili. Nonostante il formalismo adottato non presenti singoli aspetti in
grado di assicurargli un vantaggio decisivo rispetto ad altri formalismi in uso, l’insieme delle sue
caratteristiche pu` o farne un valido concorrente.
La realizzazione di un esecutore di specifiche conforme a quanto teorizzato ha infine fornito il
necessarioriscontrosperimentale. Ilminimopassodidiscretizzazionesopracui` edimostratoilsuo
funzionamento in tempo reale risulta lineare in alcuni dei parametri di interesse ed indipendente
3
CAPITOLO 1. INTRODUZIONE
dagli altri, superando cos` ı le aspettative pi` u favorevoli. Dato che al software di gestione di un
microcontrollore non ` e richiesta tanto la capacit` a di risolvere profondi problemi di ricerca, in cui
anche una marginale incompletezza pu` o essere inaccettabile, quanto quella di garantire risposte
pronte a stimoli elementari, lo scopo di questa tesi appare sostanzialmente raggiunto.
4