Sign in
Author

Conference

Journal

Organization

Year

DOI
Look for results that meet for the following criteria:
since
equal to
before
between
and
Search in all fields of study
Limit my searches in the following fields of study
Agriculture Science
Arts & Humanities
Biology
Chemistry
Computer Science
Economics & Business
Engineering
Environmental Sciences
Geosciences
Material Science
Mathematics
Medicine
Physics
Social Science
Multidisciplinary
Keywords
(7)
Functional Verification
Globally Asynchronous Locally Synchronous
Markov Process
Memory Access
Model Checking
Performance Prediction
Network On Chip
Subscribe
Academic
Publications
Towards Performance Prediction of Compositional Models in Industrial GALS Designs
Towards Performance Prediction of Compositional Models in Industrial GALS Designs,10.1007/9783642026584_18,Nicolas Coste,Holger Hermanns,Etienne L
Edit
Towards Performance Prediction of Compositional Models in Industrial GALS Designs
(
Citations: 5
)
BibTex

RIS

RefWorks
Download
Nicolas Coste
,
Holger Hermanns
,
Etienne Lantreibecq
,
Wendelin Serwe
Systems and Networks on Chips (NoCs) are a prime design focus of many hardware manufacturers. In addition to functional verification, which is a difficult necessity, the chip designers are facing extremely demanding
performance prediction
challenges, such as the need to estimate the latency of memory accesses over the NoC. This paper attacks this problem in the setting of designing globally asynchronous, locally synchronous systems (GALS). We describe foundations and applications of a combination of compositional modeling, model checking, and
Markov process
theory, to arrive at a viable approach to compute performance quantities directly on industrial, functionally verified GALS models.
Conference:
Computer Aided Verification  CAV
, pp. 204218, 2009
DOI:
10.1007/9783642026584_18
Cumulative
Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
(
www.springerlink.com
)
(
www.springerlink.com
)
(
www.informatik.unitrier.de
)
(
dx.doi.org
)
More »
Citation Context
(4)
...Since IMCs smoothly extend classical LTSs, the model has received attention in academic as well as in industrial settings [8,14,
15
]...
...Then we use interactive probabilistic chains (IPCs) [
15
] to define a discretization which reduces the time interval bounded reachability problem in IMCs to the problem of computing stepinterval bounded reachability probabilities in IPCs...
...Interactive probabilistic chains (IPCs) [
15
] are the discretetime analogon of IMCs:...
Lijun Zhang
,
et al.
Model Checking Interactive Markov Chains
...More recently, the Imc theory has been transposed into a discretetime setting, leading to the Ipc (Interactive Probabilistic Chain) theory [
4
]...
...An Ipc (Interactive Probabilistic Chain ) [
4
] can be seen as a transposition of the Imc approach to a discrete time setting...
...The Ipc Distribution tool takes as input a deterministic Ipc and two actions a and b and computes the longrun average probability distribution of the latency between a and b [
4
]...
...Our performance evaluation study [
4
] aimed at predicting throughput and latency of communication between xSTream queues...
Nicolas Coste
,
et al.
Ten Years of Performance Evaluation for Concurrent Systems Using CADP
...Interactive probabilistic chains (IPCs) are statebased models that combine discretetime Markov chains and labelled transition systems [
9
]...
Georgel Calin
,
et al.
TimeBounded Reachability in Distributed Input/Output Interactive Prob...
...applications of various domains, ranging from dynamic fault trees [11,10,12], architectural description languages such as AADL (Architectural Analysis and Design Language) [9,15,13,14], generalised stochastic Petri nets [40] and Statemate [8] to GALS (Globally Asynchronous Locally Synchronous) hardware design [22,19,
23
]...
...Definition 8 (Interactive probabilistic chain [
23
])...
Holger Hermanns
,
et al.
The How and Why of Interactive Markov Chains
References
(13)
Quantitative Evaluation in Embedded System Design: Validation of Multiprocessor Multithreaded Architectures
(
Citations: 9
)
Nicolas Coste
,
Hubert Garavel
,
Holger Hermanns
,
Richard Hersemeule
,
Yvain Thonnart
,
Meriem Zidouni
Conference:
Design, Automation, and Test in Europe  DATE
, pp. 8889, 2008
CADP 2006: A Toolbox for the Construction and Analysis of Distributed Processes
(
Citations: 64
)
Hubert Garavel
,
Radu Mateescu
,
Frédéric Lang
,
Wendelin Serwe
Conference:
Computer Aided Verification  CAV
, pp. 158163, 2007
Time and probability in formal design of distributed systems
(
Citations: 184
)
H. Hansson
Published in 1994.
Priority and Maximal Progress Are Completely Axioatisable (Extended Abstract)
(
Citations: 9
)
Holger Hermanns
,
Markus Lohrey
Conference:
International Conference on Concurrency Theory  CONCUR
, pp. 237252, 1998
A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour
(
Citations: 97
)
Iso. Lotos
Published in 1985.
Sort by:
Citations
(5)
Model Checking Interactive Markov Chains
(
Citations: 11
)
Lijun Zhang
,
Martin R. Neuhäußer
,
J. Esparza
,
R. Majumdar
Conference:
Tools and Algorithms for Construction and Analysis of Systems  TACAS
, pp. 5368, 2010
Ten Years of Performance Evaluation for Concurrent Systems Using CADP
(
Citations: 2
)
Nicolas Coste
,
Hubert Garavel
,
Holger Hermanns
,
Frédéric Lang
,
Radu Mateescu
,
Wendelin Serwe
Conference:
Leveraging Applications of Formal Methods  ISOLA
, pp. 128142, 2010
TimeBounded Reachability in Distributed Input/Output Interactive Probabilistic Chains
(
Citations: 1
)
Georgel Calin
,
Pepijn Crouzen
,
Pedro R. D'Argenio
,
Ernst Moritz Hahn
,
Lijun Zhang
Conference:
International Workshop on Model Checking of Software  SPIN
, pp. 193211, 2010
Efficient Approximation of Optimal Control for Markov Games
(
Citations: 1
)
Markus N. Rabe
,
Sven Schewe
,
Lijun Zhang
Journal:
Computing Research Repository  CORR
, vol. abs/1011.0, 2010
The How and Why of Interactive Markov Chains
(
Citations: 2
)
Holger Hermanns
,
JoostPieter Katoen
Conference:
Formal Methods for Components and Objects
, pp. 311337, 2009