About OMNI
OMNI provides a new method for the accurate analysis of the quality-of-service (QoS) properties of component-based systems. Our method takes as input a QoS property of interest and a high-level continuous-time Markov chain (CTMC) model of the analysed system, and refines this CTMC based on observations of the execution times of the system components. The refined CTMC can then be analysed with existing probabilistic model checkers to accurately predict the value of the QoS property.
OMNI avoids the synthesis of unnecessarily large and inefficient-to-analyse models by generating a different refined CTMC for each QoS property of interest. This generation of property-specific CTMCs is fully automated and comprises two steps.
The first step, called component classification, determines the effect of every system component on the analysed QoS property. The second step, called selective refinement, produces the property-specific CTMC by using phase-type distributions to refine only those parts of the high-level CTMC that correspond to components which influence the QoS property being analysed. As such, OMNI refined CTMCs model component executions with much greater accuracy than traditional CTMC modelling, whose exponential distributions match only the first moment of the unknown distributions of the observed execution times.
The refined CTMC models generated by OMNI can be analysed with the established probabilistic model checker PRISM. As illustrated by the two case studies available on this website, these models support the accurate and efficient analysis of a broad spectrum of QoS properties specified in continuous stochastic logic. As such, OMNI’s observation-enhanced QoS analysis can prevent many invalid engineering and business decisions associated with traditional CTMC-based QoS analysis.
A preliminary version of OMNI was presented at the IEEE International Conference on Software Architecture (ICSA) in 2017 and the original OMNI Website is available at:
https://www-users.cs.york.ac.uk/~cap/OMNI/.
Downloading OMNI
OMNI is freely available under the GNU General Public Licence and may be downloaded from the getting started page.Contacting us
If you wish to contact the authors then please use the following email addresses:
Colin Paterson: cap508@york.ac.uk
Radu Calinescu: radu.calinescu@york.ac.uk
References
Colin Paterson and Radu Calinescu. Accurate Analysis of Quality Properties of Software with Observation-Based Markov Chain Refinement. IEEE International Conference on Software Architecture (ICSA), 2017