• Lambda Calcolo
• History Expression
• Model Checking

Viene presentato il prototipo di un Model Checker per la verifica statica di proprietá di sicurezza, in un contesto di servizi distribuiti descritti tramite espressioni lambda-req. Queste sono un'estensione del lambda-calcolo per rappresentare reti di servizi. In questo modello, sia i servizi che i loro client possono proteggersi imponendo dei vincoli di sicurezza sul comportamento delle altre entitá tramite un meccanismo di invocazione per proprietá.

L'approccio utilizzato permette di comporre i vari servizi, garantendo che la loro esecuzione sia sicura, senza dover ricorrere a verifiche dinamiche. Questo è realizzabile in quanto, a partire dalle espressioni lambda-req, si possono inferire a priori le possibili sequenze di eventi critici per la sicurezza, descritte tramite History Expression.

Le proprietá di sicurezza vengono rappresentate come automi di Büchi, in accordo alle piú diffuse tecniche di Model Checking, le quali vengono prese in esame in conclusione del lavoro.

Lo strumento è stato realizzato principalmente in Ocaml, con un'interfaccia grafica Java per la definizione degli automi.