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. 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.