Formal Methods for Design & Verification

We study the use of formal methods for the design and verification of systems. Such systems may consist of hardware, software, or both, as in the case of Embedded Systems or Systems on Chip.

We are part of the Secure and Correct Systems (SCoS) Group at IAIK.

In the context of model checking, we look at the connections between temporal logics such as PSL and finite automata on infinite words. We also study the question of requirements analysis, i.e., of making sure that a specification is correct. One way to do this is to automatically generate and explain scenarios that satisfy (or violate) a given specification. We are also looking at alternative specification methods for properties that are hard to formulate.

When a system has a fault, we want to help the user to fix it. Thus, we consider the questions of automatic fault localization and automatic repair. For the former we employ model-based diagnosis, the latter problem is solved using game theory.

Finally, we think that it should be enough to specify a system. The implementation can be derived automatically using property synthesis. We study how to make synthesis efficient and how to assist the user to design a system by specification.

People

• Roderick Bloem
• Karin Greimel
• Georg Hofferek
• Robert Könighofer

Former Members:

• Andreas Griesmayer (UNU-ist)
• Barbara Jobstmann (VERIMAG)
• Ingo Pill (TU Graz)
• Stefan Staber (Onespin Solutions)

Projects

We are involved in the following projects.

DIAMOND

Increasing design costs are the main challenge facing the semiconductor community. Assuring the correctness of the design contributes to the major part of the problem. While diagnosis and correction of errors are more time-consuming compared to error detection, they have received far less attention, both, in terms of research works and industrial tools introduced.

Another, orthogonal, threat to the development is the rapidly growing rate of soft errors in the emerging nanometer technologies. According to roadmaps, soft errors in sequential logic are becoming a more severe issue than in memories. However, the design community is not ready for this challenge because existing soft error escape identification methods for sequential logic are inadequate.

The DIAMOND project contends the above-mentioned challenges by providing a systematic methodology and an integrated environment for the diagnosis and correction of errors on different abstraction levels and from different sources.

DIAMOND is funded by the European Commission as an FP7 STReP.

Coconut

Design and verification of modern embedded platforms are two highly related problems which are still mainly addressed by using unrelated methodologies. This effectively reduces development productivity and complicates achieving predictable system properties.

The COCONUT project thus focuses on the definition of a formal framework based on a tight integration of design and verification through all refinement steps of an embedded platform design flow, from specifications to logic synthesis and software compilation. In particular, it is intended to propose a modelling and verification flow to enhance and speed-up embedded platform design and configuration with particular regard to application fields related to mixed continuous/discrete models, like for example networked multimedia and sensor network managing.

Coconut is funded by the European Commission as an FP7 STReP.

Prosyd

The goal of the PROSYD project is to significantly increase the competitiveness and efficiency of the European IT industry through the establishment of a standard, integrated property-based paradigm for the design of electronic systems. This paradigm will integrate and unify the many phases of system development, including requirement definition, design, implementation, and verification, into one coherent design flow, building on the emerging standard property specification language PSL/Sugar, which has been recently selected as a basis for an IEEE standard. The new paradigm will enable the development of electronic systems of higher quality within shorter design cycles and with lower costs.

The prime deliverable of the PROSYD project will be a reference methodology and a set of coherent PSL/Sugar-based tools for property-based system design. Using these tools, we aim to demonstrate an improvement of at least 30% in design productivity. In addition, we expect to see an increase in the quality of the finished product, resulting in a significant decrease in the number of design flaws that make it through the verification phase.

Prosyd was funded by the European Commission as an FP6 STReP.