A Symbolic Approach to the Analysis of Multi-Formalism Markov Reward Models

When modelling large systems, modularity is an important concept, as it aids modellers to master the complexity of their model. Moreover, employing different modelling formalisms within the same modelling project has the potential to ease the description of various parts or aspects of the overall system. In the area of performability modelling, formalisms such as stochastic reward nets, stochastic process algebras, stochastic automata, or stochastic UML state charts are often used, and several of these may be employed within one modelling project. This chapter presents an approach for efficiently constructing a symbolic representation in the form of a zero-suppressed Binary Decision Diagram (BDD), which represents the Markov Reward Model underlying a multi-formalism high-level model. In this approach, the interaction between the submodels may be established either by the sharing of state variables or by the synchronisation of common activities. It is shown that the Decision Diagram data structure and the associated algorithms enable highly efficient state space generation and different forms of analysis of the underlying Markov Reward Model (e.g. calculation of reward measures or asserting non-functional system properties by means of model checking techniques).

GPA

This chapter discusses the latest trends and developments in performance analysis research of large population models. In particular, it reviews GPA, a state-of-the-art Multiformalism, Multisolution (MFMS) tool that provides a framework for the implementation of various population modelling formalisms and solution methods.

Towards a Multi-Formalism Multi-Solution Framework for Model-Driven Performance Engineering

Model-Driven Performance Engineering (MDPE) uses performance model interchange formats among multiple formalisms and tools to automate performance analysis. Model-to-Model (M2M) transformations convert system specifications into performance specifications and performance specifications to multiple performance model formalisms. Since a single tool is not good for everything, tools for different formalisms provide multiple solutions for evaluation and comparison. This chapter demonstrates transformations from the Performance Model Interchange Format (PMIF) into multiple formalisms: Queueing Network models solved with Java Modeling Tools (JMT), QNAP, and SPE·ED, and Petri Nets solved with PIPE2.

Combining Heterogeneity, Compositionality, and Automatic Generation in Formal Modelling

Critical computer-based systems have an increasing complexity due to the number of components, to their heterogeneity, and to the relationships among them. Such systems must meet strict non-functional requirements and should be able to cope with competitive market needs. The adoption of formal methods is often advocated in order to provide formal proof, but their application does not scale with the growing size of systems. The aim of this chapter is to introduce a modelling and analysis methodology that allows the combination of three proven research trends in formal modelling of large systems: formal model generation (by means of model-driven techniques), multiformalism, and compositional approaches. In this chapter there is also a discussion about enabling techniques. The proposed approach has been applied to the performability modelling and evaluation of flexible manufacturing systems.

Multiformalism Modeling Compositionality in SIMTHESys

Multiformalism has emerged as a sound technique to define a complex system as the composition of a set of sub-components, each one modeled according to the best-suited formalism. Existing literature offers a wide choice of frameworks and tools that exploit model composition following different approaches. This chapter provides an insight into the composition approach used by SIMTHESys (a framework for the development of modeling languages and the solution of multiformalism models) in order to compose easily and consistently primitives belonging to different (custom) modeling languages. A case study is presented to illustrate the effectiveness of the proposed composition formalism.