Paper Info
Title
Formal model of a protocol converter
Abstract
Reuse of components is a burgeoning field in chip design. Shorter time to market and assured quality are just two good reasons to reuse previously engineered components. Problems arise however when chip designers need to interface these components as they typically conform to different standards, or no standards at all. The popular model of interfacing components such as protocols is via a 'converter' that translates data between the components. We develop a theoretical model of a converter that will enable two given arbitrary protocols to communicate. This model includes buffers. We formally define correctness conditions, and guarantee that the resulting converter satisfies these conditions. We also allow the designer to define his own (CTL) conditions. As well, we allow protocols to be nondeterministic, and we ensure only valid data is sent to the converter. The verification of the conditions is carried out by a model checker (not reported in this work). We have implemented our theoretical model and we present experimental results.
Year
Venue
Keywords
2009
CATS
model checker,shorter time,popular model,valid data,chip design,theoretical model,formal model,chip designer,protocol converter,arbitrary protocol,translates data,resulting converter,formal verification
Field
DocType
Citations 
Model checking,Nondeterministic algorithm,Reuse,Computer science,Correctness,Interfacing,Protocol converter,Time to market,Formal verification,Embedded system
Conference
5
PageRank 
References 
Authors
0.51
12
2
Name
Order
Citations
PageRank
Jing Cao1202.99
Albert Nymeyer21069.98