La definizione e l’analisi di politiche di controllo d’accesso (access policy) sono elementi cardine su cui basare qualsiasi schema di protezione per sistemi industriali di controllo e di automazione distribuiti, contro attacchi informatici condotti sia a livello locale sia attraverso il cyberspazio. Quest’articolo mostra come l’uso di opportune tecniche di modellazione e di verifica, condotte con l’ausilio di strumenti software automatici, possa essere di aiuto nel raccordare le policy specificate a un alto livello di astrazione con i meccanismi elementari di sicurezza di basso livello, presenti nell’implementazione del sistema fisico reale. L’approccio utilizzato per raggiungere tale obiettivo è basato su un tipo di modello innovativo che integra due diverse viste dello stesso sistema, indicate nel seguito rispettivamente con i termini di specifica e implementazione. Le capacità descrittive del modello sono presentate tramite un semplice esempio derivato da un prototipo reale d’impianto progettato per la riparazione, lo smontaggio e il riciclaggio di circuiti stampati.