Title :
Ranking structure in communication fabrics
Author :
Ray, Sambaran ; Brayton, Robert K.
Author_Institution :
Dept. of Electr. Eng. & Comput. Sci., Univ. of California, Berkeley, Berkeley, CA, USA
Abstract :
We present our experience and case studies for proving liveness of communication fabrics. A methodology is developed that reveals ranking structure underlying the state spaces of such fabrics. This enables an efficient proof of liveness using the k-LIVENESS algorithm leveraging this ranking structure. An open-source infrastructure for the k-LIVENESS algorithm has been implemented that has a provision for specifying and leveraging ranking structures in the form of stabilizing constraints. A significant speed-up was achieved with this modified k-LIVENESS framework when proving response property of communication fabrics.
Keywords :
formal verification; communication fabrics; k-LIVENESS algorithm; ranking structure; response property; stabilizing constraints; state spaces; Abstracts; Algorithm design and analysis; Benchmark testing; Fabrics; Monitoring; Safety; Semantics; communication fabrics; formal verification; liveness;
Conference_Titel :
Formal Methods and Models for Codesign (MEMOCODE), 2013 Eleventh IEEE/ACM International Conference on
Conference_Location :
Portland, OR
Print_ISBN :
978-1-4799-0903-2
