Model based verification and adaptation of software systems @runtime

The pervasiveness and flexibility of modern software systems and the uncertainty, unpredictability, and variability of their execution environments are strengthening the quest for systems that can self-adapt to their surrounding context. At run time, systems are required to monitor the environment, identify possible violations of the requirements, and plan a suitable reaction. Traditional techniques for automatic requirements verification are conceived for design time use and can hardly satisfy the time constraints imposed by run time analysis. Planning as well suffers from similar limitations, being most of the known approaches static and only effective in specific domains. In this thesis several results from stochastic processes analysis, semantic interpretation of formal languages, and control theory are used to ground the definition of novel verification and adaptation methodologies devised for run time use, with a particular focus on non functional requirements such as reliability, performance, or cost. Particular attention has been paid to the generality and the formal assessment of the effectiveness of these methodologies, which have proved to be efficient and dependable in a wide application scope. The contributions of this research can be summarized in the following list: - a methodology for run time efficient probabilistic model-checking, that define a design time partial evaluation procedure that significantly simplifies and speeds up the verification at run time. - an approach to bring sensitivity analysis at run time to estimate the impact of each monitored environmental condition online. - a methodology for syntactic-semantic incremental analysis, that can be used to define incremental verification procedures of both functional and non-functional requirements. - a methodology for software control through Markov models, providing for the automatic generation of broad-scope controllers able to adapt tunable software at run time in order to make it continuously satisfy its non functional requirements. - a reliability driven dynamic-binding strategy grounded on control theory that provides formal assurance of scalability, robustness, and efficiency.

Pervasività e flessibilità dei moderni sistemi software-intensive, assieme ad incertezza, non predicibilità e variabilità delle infrastrutture di calcolo, pongono l’accento sulla necessità di sistemi in grado di adattarsi autonomamente all’ambiente che li circonda. Durante la loro esecuzione, tali sistemi devono essere in grado di monitorare l’ambiente, identificare possibili violazioni dei loro requisiti e pianificare reazioni opportune. Le tecniche tradizionali per verificare il soddisfacimento dei requisiti sono tipicamente concepite per l’utilizzo in fase di progettazione e sviluppo e difficilmente riescono a soddisfare i vincoli temporali imposti dall’analisi a runtime. Gli algoritmi di planning soffrono spesso di limitazioni analoghe, essendo la maggior parte di essi pensati per contesti statici o per domini specifici. In questa tesi, concetti propri dell’analisi dei processi stocastici, dell’interpretazione semantica dei linguaggi formali e della teoria del controllo costituiscono il fondamento di alcune metodologie innovative per la verifica e l’adattamento di sistemi software a runtime. La ricerca si focalizza prevalentemente sui requisiti non funzionali quali, ad esempio, affidabilità, performance o costo. Un’attenzione particolare è stata rivolta alla generalità delle procedure proposte e alla valutazione formale della loro efficacia, dimostrandone anche sperimentalmente efficienza e affidabilità in un ampio spettro applicativo. I principali contributi di questa ricerca sono sintetizzabili nei seguenti punti: - una metodologia per model-checking probabilistico a runtime che, basata su una valutazione parziale del problema durante la fase di design, è in grado di semplificare drasticamente la verifica dei requisiti a seguito di cambiamenti nell’ambiente o nel sistema. - un approccio per effettuare un’analisi di sensitività a runtime allo scopo di stimare in tempo reale l’impatto di ciascuna delle condizioni ambientali monitorate durante l’esecuzione. - una metodologia per l’analisi sintattico-semantica incrementale di artefatti software utile a definire procedure di verifica sia di requisiti funzionali che non funzionali. - una metodologia per il controllo di sistemi software il cui control flow sia astraibile tramite processi Markoviani e che include la generazione automatica di controllori in grado di adattare il comportamento del sistema durante la sua esecuzione perché continui a soddisfare i suoi requisiti. - un meccanismo di dynamic-binding adattativo mirato a garantire la convergenza dell’affidabilità del sistema al suo valore obiettivo. Tale meccanismo è fondato su risultati di teoria del controllo che ne garantiscono formalmente scalabilità, robustezza ed efficienza.