|
|
 |
|
NIA Formal Methods Seminar by Julien Schmaltz |
|
Date: November 21, 2006
Time: 10:30am
Location: NIA, Rm 137
Additional Information: Presentation (PDF)
Verisoft: Towards Verified Distributed Stacks
Julien Schmaltz, Saarland University, Germany
The Verisoft project aims at developing methods and tools for the pervasive verification - from abstract software down to gates - of computer systems.
Computer systems are often distributed and work under real-time constraints.
Our goal is the proof of a simulation theorem between application software and their distributed gate implementation. In particular, this includes the correctness proof of the communications between every layer of these distributed stacks. This talk presents two aspects around this verification effort.
On the one hand, we present a generic network model unifying communication architectures at a high-level of abstraction. This model embraces protocols, routing algorithms and switching techniques. It identifies the key constituents common to all communication architectures, and their essential properties
from which the correctness of the overall model is deduced. Thus, the verification of any particular design is reduced to the proof of the essential properties.
On the other hand, we formalize asynchronous communications at the bit level.
Our model considers precise timing parameters and metastability.
We prove the correctness of bit transmission between two independently clocked registers. We express this theorem in a digital context, defining digital conditions which guarantee correctness in the analog context.
Our formalism and the separation between analog and digital concerns allow the combination of classical automated tools and interactive theorem proving for the verification of time-triggered hardware interfaces.
We conclude with a hint on the integration of these results in our stack proof.
|
|
|
Home