This paper characterizes the workload seen at the storage subsystem of an e-commerce system. Measurements are conducted on multi-tiered systems running three different benchmarks,...
The UML profile for Modeling and Analysis of Real Time and Embedded systems (MARTE) provides a powerful, standardised framework for the specification of non-functional propertie...
We present a new version of PROBDIVINE – a parallel tool for verification of probabilistic systems against properties formulated in linear temporal logic. Unlike the previous r...
We tackle the problem of non robustness of simulation and bisimulation when dealing with probabilistic processes. It is important to ignore tiny deviations in probabilities becaus...
Abstract—We present an approach to support the debugging of stochastic system models using interactive visualization. The goal of this work is to facilitate the identification o...
We begin by observing that (discrete-time) QuasiBirth-Death Processes (QBDs) are equivalent, in a precise sense, to (discrete-time) probabilistic 1-Counter Automata (p1CAs), and b...
CaVi provides a uniform interface to state-of-the-art simulation methods and formal verification methods for wireless sensor network. Simulation is suitable to examine the behavi...