Le smart cities sono ormai oggetto di tanti progetti di innovazione, e nell'agenda politica di molte amministrazioni. Spesso, nella progettazione di servizi smart e nelle discussioni al riguardo l'enfasi viene posta soprattutto sull'importanza della raccolta dei dati e delle comunicazioni, con particolare riguardo all'Internet delle cose. Minore attenzione viene invece rivolta alle interazioni necessarie fra le varie parti (umani, cose, programmi, sistemi di comunicazione, ecc.), e alla necessità di garantire che tali interazioni, indispensabili per una smart city, concorrano alla produzione di servizi ad alta qualità e affidabilità. Va sottolineato che si tratta di sistemi complessi, dove i servizi possono essere il risultato di comportamenti collettivi di agenti di varia natura; di sistemi con spiccate caratteristiche di adattabilità e dove, ad esempio, la qualità del servizio può essere il risultato di comportamenti emergenti. Pertanto, lo studio e la progettazione di questi sistemi devono essere essi stessi smart. QUANTICOL (www.quanticol.eu) è un progetto di ricerca EU 7FP FET-Proactive sui Fondamenti dei Collective Adaptive Systems (CAS), iniziato nel 2013. Esso mira a sviluppare nuove tecniche di modellizzazione e analisi formali quantitative per la progettazione e la gestione operativa di sistemi adattativi collettivi, con particolare attenzione alle necessità del contesto delle smart cities e delle loro infrastrutture ICT. Il fatto stesso che tali sistemi siano fortemente distribuiti e il loro comportamento adattativo si basi sul feedback stretto e continuo tra un gran numero di consumatori e produttori con controllo decentralizzato, rende tali sistemi tipici esempi di CAS. La natura pervasiva ma trasparente di questi sistemi, insieme con l'importanza degli obiettivi che ci si pone, implicano la necessità di avere strumenti adeguati anche per un'analisi a priori, in fase di progettazione, per potere indagare a fondo su tutti gli aspetti del loro comportamento, compresi quelli quantitativi ed emergenti. Vogliamo in sostanza potere essere sufficientemente fiduciosi che, una volta operativi, questi sistemi possono non solo fornire buoni servizi ``a regime'', ma siano anche in grado di adattarsi alle mutevoli esigenze, in modo autonomo e senza interruzioni operative.
La vision a lungo termine di QUANTICOL è lo sviluppo di una piattaforma concettuale basata su metodi formali, matematici e logici, di supporto alla progettazione e all'analisi qualitativa e quantitativa dei CAS per smart cities, corredata anche da una metodologia di software engineering adeguata e specializzata per tali sistemi. La strategia adottata dal progetto è quella della multidisciplinarietà. QUANTICOL, infatti, riunisce due comunità accademiche di ricerca distinte: quella dei Metodi Formali dell'Informatica, con particolare riferimento alle algebre di processi stocastiche, alle logiche e alle relative tecniche automatiche di verifica; e quella della Matematica Applicata con particolare riferimento alle tecniche di mean-field/fluid-flow approximation e control theory. I principali casi di studio che guidano l'attività di ricerca nel contesto di QUANTICOL sono due: il primo affronta problemi di scalabilità e pianificazione della capacità per sistemi di trasporto urbano smart, con particolare riferimento a sistemi di gestione di autobus e sistemi di bike sharing. Il secondo affronta invece i problemi di progettazione e modellizzazione di smart grid, nel campo dei sistemi di produzione e distribuzione di energia elettrica.
A un anno dal suo inizio, il progetto ha già dato dimostrazione della fattibilità degli approcci che si intendono seguire. Ad esempio, le tecniche di base, adottate in questa prima fase del progetto sono state applicate alla modellizzazione e all'analisi del sistema di trasporto pubblico nella città di Edimburgo, con un focus specifico sulla rete di autobus. Utilizzando dati di localizzazione automatica dei veicoli nella città, il progetto QUANTICOL è stato in grado di costruire modelli stocastici accurati del servizio di autobus di Edimburgo. Quindi, utilizzando strumenti software di analisi formale basata su logiche stocastiche, è stato possibile calcolare automaticamente misure quali la probabilità di completare un tragitto entro una data finestra di tolleranza per i tempi di arrivo e definire una tabella oraria ottimale realmente compatibile con i dati ottenuti dalle precedenti misure. Va sottolineato come le misure di probabilità non siano il risultato di operazioni ad hoc ma ottenute tramite una specifica di requisiti fatta usando formule di logica matematica, favorendo, così, la possibilità di analisi rigorosa della consistenza dei requisiti stessi e l'automazione del processo di valutazione.
Un'altra applicazione dei risultati preliminari del progetto consiste nella modellizzazione, usando tecniche di approssimazione mean-field, dei comportamenti probabili di un sistema di bike sharing e l'utilizzo combinato di sofisticate tecniche di model-checking, allo sviluppo delle quali l'ISTI ha dato un contributo sostanziale, per l'analisi di proprietà rilevanti di tali comportamenti. In particolare una domanda centrale per un sistema di bike sharing è quale sarebbe il numero di biciclette ottimale nel sistema in relazione al numero e alla capacità dei parking-slot, ad un dato tasso di richieste di bici per unità di tempo e per un dato tempo medio del loro uso. Un altro aspetto interessante da capire puo' essere l'effetto potenziale, positivo o negativo, di una strategia di incentivi per gli utenti e quindi capire se essa possa contribuire ad ottenere una distribuzione più equa delle bici nelle stazioni. Ovviamente, è importante capire i possibili effetti di una tale strategia prima di adottarla sul campo.
Quello che è importante mettere in evidenza è il fatto che l'approccio seguito consente di modificare facilmente i modelli e ripeterne le analisi con estrema semplicità e costo computazionale relativamente basso, il che li rende particolarmente utili per dare una prima risposta (approssimata) a domande del tipo "what if?".
Il Progetto EU QUANTICOL (http://www.quanticol.eu/) è coordinato dalla Prof.ssa J. Hillston, Direttrice del Laboratory for Foundations of Computer Science della School of Informatics dell'Universita' di Edimburgo. Gli altri partner del progetto sono il Consiglio Nazionale delle Ricerche, tramite il laboratorio di Formal Methods and Tools dell'ISTI, l'IMT Advanced Studies Lucca, l'INRIA di Grenoble e l'Università di Southampton.
Contatti: mieke.massink@isti.cnr.it
Immagini:
