Sciweavers

QEST
2010
IEEE

Automatic Compositional Reasoning for Probabilistic Model Checking of Hardware Designs

13 years 1 months ago
Automatic Compositional Reasoning for Probabilistic Model Checking of Hardware Designs
Adaptive techniques like voltage and frequency scaling, process variations and the randomness of input data contribute signi cantly to the statistical aspect of contemporary hardware designs. Therefore, the performance metrics of such designs are also statistical in nature. In previous work, we have employed probabilistic model checking to rigorously evaluate the statistical performance of hardware designs. In this paper, we present an automatic compositional reasoning technique to improve the scalability of probabilistic model checking of hardware systems. We partition the set of system observables into disjoint subsets and use them to structurally decompose the system into smaller components. We employ an assume-guarantee form of reasoning and analyze the space of environmental constraints using a value-based case splitting approach. We split the space of values of all the observables of one component into separate value-based cases. We provide an argument for the correctness of our ...
Jayanand Asok Kumar, Shobha Vasudevan
Added 14 Feb 2011
Updated 14 Feb 2011
Type Journal
Year 2010
Where QEST
Authors Jayanand Asok Kumar, Shobha Vasudevan
Comments (0)