loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
17th IEEE International Workshop on Rapid System Prototyping (RSP'06)
Formalizing the Incremental Design and Verification Process of a Pipelined Protocol Converter
Chania, Crete
June 14-June 16
ISBN: 0-7695-2580-6
Cecile Braunstein, Universite Pierre et Marie Curie, France
Emmanuelle Encrenaz, ENS CACHAN, France
This work studies the relations between pipeline architectures and their specification expressed in CTL. We propose a method to build pipeline structures incrementally from a simple one (already verified) to a more complex one. Moreover, we show how each increment can be integrated in a CTL specification. We define increments to model treatment delay and treatment abortion of a pipeline flow, and we formalize the composition of the different increments. In order to represent the increments added to an architecture, we derive a set of CTL formulae transformations. Finally we model a control flow of a protocol converter by composition of these increments. We show how CTL properties of the complex architecture are built by applying automatic transformations on the set of CTL properties of the simplest architecture.
Citation:
Cecile Braunstein, Emmanuelle Encrenaz, "Formalizing the Incremental Design and Verification Process of a Pipelined Protocol Converter," rsp, pp.103-109, 17th IEEE International Workshop on Rapid System Prototyping (RSP'06), 2006
Usage of this product signifies your acceptance of the Terms of Use.