Model Analysis

As in any engineering discipline, complexity is mastered by using models. By analyzing these models insights can be obtained in the behavior of software, that might otherwise be detected in the hard way. Software produced using model analysis is in general of a considerable higher quality than software constructed in the traditional way.

With software modeling the essential communication structure of software components are described. Analysis techniques can typically determine whether there are no deadlocks, data is always delivered in time, alarm signals are always handled properly and dangerous situations are always avoided.

In general, software modeling and analysis also helps in obtaining a better understanding of the behavior of the system, which often leads to cleaner, more straightforward and more versatile designs, which helps in mastering the enormous complexity that we far too often see in the software business.

mCRL2 Toolset

The mCRL2 toolset allows users to model and analyze complex communication patterns in parallel and distributed software. Models can be specified in a process algebraic language that supports data and time, created using a graphical editor, or generated using conversion tools. Subsequently, these models can be analyzed by means of simulation, visualization, and automated testing and verification. Automated verification is supported by dedicated checks for deadlocks or occurrences of specific actions, by model equivalence checks, and by full model checking using properties expressed as temporal logic formulae.

A wide range of industrial case studies has been performed using the mCRL2 toolset, ranging from communication protocols such as sliding window protocols, hardware drivers for devices like pacemakers and I²C equipment, to control software for large systems such as networks of intelligent printers. So far, all case studies revealed errors, but also their causes and solutions.

The mCRL2 toolset is being developed at the Design and Analysis of Systems group of Eindhoven University of Technology, in collaboration with LaQuSo, Centrum Wiskunde & Informatica and University of Twente. The toolset is available under an open source license from mcrl2.org.

UNO

UNO is a tool for source code analysis. Besides the standard static analysis checks for Uninitialized variables, Null pointer references, and Out of bound array indices, UNO can also perform some advanced checking for user defined properties. UNO combines static analysis and model checking by capitalizing on the best features of both methods while avoiding their notorious pitfalls.

Compared to model checking tools, the advantage of UNO is that it works directly on the C source code and therefore it does not require a model of the program. Still, UNO retains the most important benefits of model checking. Most of the static analysis tools usually present only a predetermined repertoire of properties that can be checked. In contrast, UNO offers the flexibility to encode user defined properties. In the model checking style these properties are encoded as property automata. The property automaton monitors the traversal of the control flow graph of the C functions and in case a violation of the property is found, UNO produces an error trace which can significantly facilitate the location and correction of the defect.

Unlike typical static analysis tools, UNO usually produces only a small percentage of false positives. Since it works on the control flow graphs of the C functions, it does not suffer from the infamous state explosion problem, which is the main bottleneck in the applications of model checking tools. UNO has been successfully applied to various kinds of C programs, including kernel functions of the Linux operating system. In LaQuSo we have used the advanced analysis via user defined properties to find dynamic behavioral defects, like race conditions, deadlocks, and improper usage of interrupts in Linux device drivers. However, the flexibility of defining user customized properties does not limit UNO to only these kinds of errors. One can define automata for checking other relevant defects, like memory leaks and security flaws. Thus, we are looking forward for new challenges in that direction.