Testing and/or simulation are classical ways to look for design errors. However these approaches have two limitations:
The goal of Formal Methods is to complement testing and simulation by addressing those design areas for which testing or simulation are not suitable. Namely:
Formal methods can be broadly classified into automatic (e.g. Model Checking) and interactive (e.g. Proof Checking).
Automatic methods (model checking) can be easily introduced in the design cycle since they do not require a long training to be used. However, in general automatic methods can only be applied to Finite State Systems (FSSs). Fortunately many systems for which correctness is important are or can be approximated with FSSs. E.g. digital hardware, many reactive programs found in embedded control and/or telecommunication applications. Indeed automatic verification can often be done starting from the source code describing our systems (hardware or software). E.g. automatic verification can start from (possibly suitable fragments of) HDL, VHDL, SDL or Esterel code.
Interactive methods (proof checking) can be applied to any system in principle. However they require highly trained people to be used. Thus interactive methods are used only on projects that justify such an effort (e.g. new microprocessors, some military applications, etc).
Our research focuses on automatic methods for verification and, when possible, synthesis of finite state systems (hardware as well as software). Our main interests are in:
Using systems of equations on boolean functions we can define a Boolean Symbolic Programming (BSP) language based on BFOL (Boolean First Order Logic). This is done in [Tro 95a].
BSP is is a programming language designed to define explicit (i.e. using boolean operators or quantifiers) as well as implicit (i.e. using fixpoints) computations on boolean functions (boolean symbolic computations). For BSP we have implemented a BDD based interpreter as well as a BDD package tailored to it.
BSP can be downloaded from http://www.dsi.uniroma1.it/~tronci/bsp.html.
Automatic Verification of FSSs via Model Checking amounts to carry out computations on boolean functions [Tro 95a]. Thus BSP can be used as a Model Checker. However BSP has some advantages w.r.t. "traditional" model checkers.
For protocol verification or, more in general, for software like systems, Explicit Model Checking (i.e. State Space Exploration ) often outperforms Symbolic (i.e. OBDD based) Model Checking.
Our experimental results show ([TDIZ 01], [TDIZ 01a]) that protocols exhibit transition locality . That is, w.r.t. levels of a Breadth First (BF) visit, state transitions tend to be between states belonging to close levels of the transition graph.
This lead us to design a verification algorithm exploiting transition locality. We implemented such an algorithm within the Murphi verifier (http://sprout.stanford.edu/dill/murphi.html). We called our tool Cached Murphi and it is available on Murphi web site as well as in http://www.dsi.uniroma1.it/~tronci/cached.murphi.html
Our experimental results show that using our cached approach we can typically save more than 40% of RAM with an average time penalty of about 50%.
Transition locality can also be used to improve disk based state space exploration algorithms ([DITZ 02]). For example using our disk based Murphi we were able to complete verification of a protocol with about one billion of reachable states. This would require more than 5 gigabytes of RAM using RAM based Murphi.
The above results allowed us to automatically verify quite large systems ([DITZ 02]). Moreover our research results show that also Hybrid Systems can be effectively analyzed using cached murphi ([GHBTCM 02]).
A control system can often be partitioned into two main subsystems: a controller and a plant. The controller purpose is to restrict the plant behaviour so as to meet given closed loop system (plant + controller) specifications.
If plant and controller can be modeled as FSSs formal methods (namely: model checking) can be used to automatically check correctness of the designed controller w.r.t. given closed loop specifications. To this end we need to write formal specifications for the closed loop system, a finite state model of the plant, and a finite state model of the controller. E.g. this is possible when the plant is a finite state Discrete Event System (DES).
An alternative approach is to automatically synthesize the controller from the plant finite state model and the closed loop formal specifications. This yields a controller which is correct by construction, saves on the controller coding effort (thus saving on design time and cost) and allows us to focus on formal specifications (thus improving design quality).
The main obstruction to such approach is state explosion. As for automatic verification we can use symbolic (i.e. BDD based) algorithms to contrast state explosion. BSP can be used to define (and effectively run) symbolic controller synthesis algorithms. In general this cannot be done with any of the currently available BDD based tools (Model Checkers) without resorting to BDD primitives.
Optimal supervisors [Tro 96] as well as optimal controllers [Tro 97] for nontrivial plants can be automatically synthesized using our symbolic algorithms ([Tro 98], [Tro 99a], [Tro 99b]) E.g. we can automatically synthesize optimal controllers for plants with more than 10^9 states.
Many case studies have been carried out in collaboration with industry as well as research institutions. The goal of these case studies has been mainly that of testing effectiveness of our proposed approaches to automatic verification as well as to carry out technology transefer.
Here is a selected list of case studies.