Uno dei problemi più spinosi nel campo della produzione di sistemi informatizzati − a livello sia di software (SW), di hardware (HW) o di entrambi − è quello di verificare efficacemente la totale correttezza del funzionamento dei sistemi progettati. Questo problema diventa addirittura vitale nel campo delle applicazioni "safety critical" (ad esempio nel mondo dei sistemi automobilistici, avionici, ferroviari o sanitari), in cui un errore di esecuzione di un sistema può causare la morte o il ferimento di decine di esseri umani, o in quelle "business critical" (come un sistema software bancario, o un microprocessore prodotto su larga scala) in cui un errore può causare la perdita di ingenti quantità di denaro.
La dimensione e la complessità dei sistemi software o hardware da verificare sono in continua crescita: basta considerare che su un’autovettura di medie dimensioni sono presenti più di 50 computer o centraline, e che su un aereo il software può arrivare a centinaia di milioni di linee. Pertanto, è necessario che la verifica avvenga a sua volta in modo automatizzato. In sintesi, si tratta di progettare sistemi informatizzati che verifichino la correttezza di altri sistemi informatizzati.
Il problema di verificare automaticamente la correttezza di un sistema software o hardware è concettualmente molto complesso. Un sistema è corretto se per ogni possibile sequenza di input produce sempre la corretta sequenza di output desiderata. Il problema è che le sequenze di input possibili sono un numero enorme, molto spesso infinito, per cui è praticamente impossibile verificarle tutte singolarmente.
Alla base della Computer-Aided Verification stanno i cosiddetti metodi formali, che consentono di descrivere il problema della correttezza − sia il progetto del sistema hardware o software, sia l'insieme di tutte le sequenze di input possibili, sia quello delle sequenze di output desiderate − tramite espressioni logiche, che possono essere generate automaticamente dalle specifiche di un progetto tramite opportuni compilatori. La verifica della correttezza viene quindi effettuata da algoritmi di deduzione logica automatica, una disciplina derivata dall'Intelligenza Artificiale, che "deducono" le sequenze di output desiderate come conseguenze logiche delle sequenze di input e del sistema da verificare. Quando questo non avviene, gli algoritmi individuano le sequenze di input e le parti del sistema che causano la deduzione di una sequenza in output errata, permettendo ai progettisti di individuare e correggere gli errori di progetto.
Inizialmente, i metodi formali si basavano su espressioni puramente logiche, e portarono significativi vantaggi applicativi nell’ambito della verifica di alcuni componenti hardware. La logica utilizzata, per altro, non era sufficientemente espressiva per rappresentare direttamente ed efficacemente molte operazioni fondamentali utilizzate nella rappresentazione dei sistemi software e hardware: in particolare le operazioni aritmetiche, ma anche operazioni specifiche quali l'accesso in memoria, la manipolazione di sequenze di simboli, o operazioni specifiche dei microprocessori.
Satisfiability Modulo Theories (SMT) nacque quindi dall'intuizione di integrare algoritmi per deduzione logica con altri algoritmi concepiti per risolvere problemi di natura molto diversa, quali la soluzione numerica di problemi matematici o la manipolazione di sequenze di caratteri o elementi. Questo ha permesso di costruire algoritmi di verifica "ibridi" basati su SMT molto più potenti e versatili, aumentando notevolmente l'espressività ed efficacia nella rappresentazione e verifica di sistemi complessi.
Per esempio, supponiamo si voglia verificare la correttezza del progetto di un sistema computerizzato che ordini di alzare o abbassare le sbarre di un gruppo di passaggi a livello, reagendo automaticamente ai sensori che segnalano l'arrivo dei treni. È necessario verificare che tutte le possibili sequenze di segnali dai sensori in input causino sempre in output sequenze corrette di ordini alle sbarre, per cui ogni sbarra sia sempre abbassata quando un treno è in arrivo. Contrariamente ai loro predecessori, gli algoritmi di verifica basati su Satisfiability Modulo Theories permettono di effettuare questo tipo di verifiche molto efficacemente, combinando la deduzione puramente logica, necessaria per analizzare tutte le combinazioni possibili di treni in arrivo e partenza, con il calcolo puramente matematico, necessario per prevederne i tempi di percorrenza.
Sistemi di verifica basati su Satisfiability Modulo Theories sono tuttora oggetto di intensa attività di ricerca, e al tempo stesso largamente utilizzati dai principali produttori di sistemi software (tra cui Microsoft, Apple, Amazon) e hardware (come Intel, AMD, Nvidia) e, in particolar modo, dalle compagnie che sviluppano sistemi informatizzati safety critical e business critical.
La conferenza internazionale CAV 2021 (Computer-Aided Verification 2021) che si è svolta online dal 18 al 24 luglio, ha assegnato ad Alessandro Cimatti e Roberto Sebastiani il Computer-Aided Verification Award 2021, come riconoscimento per la loro ricerca pionieristica sulla Satisfiability Modulo Theories (SMT). CAV è la più importante conferenza internazionale sulla verifica di correttezza di sistemi hardware e software e una delle più prestigiose in informatica. La cerimonia ufficiale di consegna del premio si terrà nell’edizione 2022 che si svolgerà in Israele.
La collaborazione tra Alessandro Cimatti e Roberto Sebastiani dura da oltre vent'anni: hanno scritto insieme quasi quaranta articoli scientifici, molti dei quali sono lavori fondazionali sul tema per i quali sono stati premiati; hanno dato vita al progetto MathSAT, e hanno supervisionato in modo congiunto numerosi studenti di dottorato.
Automatic verification of computerized systems
Alessandro Cimatti and Roberto Sebastiani won the Computer-Aided Verification Award 2021
by Alessandro Cimatti and Roberto Sebastiani
Alessandro Cimatti is director of the Digital Industry Center of Fondazione Bruno Kessler. Roberto Sebastiani is full professor at the Department of Information Engineering and Computer Science of UniTrento.
One of the thorniest issues in the field of the creation of computerized systems - at software (SW) or hardware (HW) level, or both - concerns the effective verification of the correctness of the functioning of the designed systems. This issue becomes vital in the area of "safety critical" applications (for example, in the fields of automotive, avionics, railways or healthcare systems), where an error in the execution of a system can cause the death or injury of dozens of human beings, or in the area of "business critical" applications (such as a banking software system, or in the large scale production of microprocessors), where an error can cause the loss of large amounts of money.
The size and complexity of the software or hardware systems that must be verified are constantly growing: consider, e.g., that a medium-sized car has more than 50 computers or control units, and that the software of an airplane can have hundreds of millions of code lines. Consequently, verification must be automated. In short, computer-aided verification means designing computerized systems that verify the correctness of other computerized systems.
The problem of automatically verifying the correctness of a software or hardware system is conceptually very complex. A system is correct if, for every possible input sequence, it always produces the correct desired output sequence. The problem is that, the number of possible input sequences is huge, most often even infinite, so it is practically impossible to verify all them one by one.
Computer-Aided Verification is based on the so-called formal methods, with which the problem of correctness - the hardware or software system design, the set of all possible input sequences, and that of the desired output sequences - can be described using logical expressions, which can be automatically generated from the specifications of a project by means of suitable compilers. Verification of correctness is then performed by automated logical deduction algorithms, a discipline derived from AI (artificial intelligence), which "deduce" the desired output sequences as logical consequences of the input sequences and of the system to be verified. When this is not the case, the algorithms identify the input sequences and the parts of the system that are responsible for the deduction of an incorrect output sequence, allowing designers to identify and correct design errors.
Formal methods were initially based on purely logical expressions, and brought significant application advantages in the verification of some hardware components. The logic used, however, was not sufficiently expressive to directly and effectively represent many fundamental operations used in the representation of software and hardware systems: in particular, arithmetic operations, but also specific operations to access memory and manipulate sequences of symbols, and specific microprocessor operations.
Satisfiability Modulo Theories (SMT) therefore came from the intuition of integrating algorithms for logical deduction with other algorithms designed to solve other types of problems, such as the numerical solution of mathematical problems or the manipulation of sequences of characters or elements. This made it possible to build much more powerful and versatile "hybrid" verification algorithms based on SMT, greatly increasing the expressiveness and effectiveness of the representation and verification of complex systems.
For example, suppose you want to verify the correctness of the design of a computerized system that commands the barriers to be lifted or lowered at a number of level crossings, automatically responding to sensors that detect the arrival of trains. It is necessary to verify that all possible signal sequences provided by the input sensors always generate correct output sequences to move the barriers, so that all barriers are always lowered when a train is incoming. Unlike previous algorithms, verification algorithms based on Satisfiability Modulo Theories make this type of verification very effective, by combining purely-logical deduction, which is necessary to analyze all the possible combinations of arriving and departing trains, with purely-mathematical calculation, which is necessary to predict travel times.
Verification systems based on Satisfiability Modulo Theories are still the subject of intense research activity and, at the same time, are widely used by the main producers of software (including Microsoft, Apple, Amazon) and hardware (such as Intel, AMD, Nvidia) systems and, in particular, by companies that develop safety-critical and business-critical computer systems.
[Traduzione Paola Bonadiman]
CAV 2021, the International Conference on Computer-Aided Verification, which took place online from 18 to 24 July, awarded Alessandro Cimatti and Roberto Sebastiani the Computer-Aided Verification Award 2021, for their pioneering contributions to the foundations of the theory and practice of Satisfiability Modulo Theories (SMT). CAV is the most important international conference on computer-aided formal analysis methods for hardware and software systems and one of the most prestigious in computer science. The official award ceremony will take place during the 2022 edition that will be held in Israel.
The collaboration between Alessandro Cimatti and Roberto Sebastiani has been going on for over twenty years: together they have written nearly forty scientific articles, many of which are foundational works for which they have received prizes; they have started the MathSAT project, and jointly supervised many PhD students.