About ePMC
ePMC is a parametric model checking (PMC) method for the efficient analysis of reliability, performance and other quality-of-service (QoS) properties of alternative software designs.
ePMC comprises two stages.
The first stage is domain specific and is performed only once for each domain (i.e. type of software system) that the method is applied to. This stage uses domain-expert input to identify domain-specific modelling patterns for components of systems from the considered domain, and precomputes closed-form expressions for key QoS properties of these patterns.
The second stage of the method is performed for each structurally different variant of a system and QoS property under analysis. The stage involves the PMC of a parametric Markov chain that models the interactions between the system components. This high-level Markov model can be provided by software engineers with PMC expertise, or can be generated from more general software models, such as annotated UML activity diagrams.
Downloading ePMC
ePMC is freely available under the GNU General Public Licence and may be downloaded from the getting started page.Contacting us
To contact the authors please use the following email addresses:
Radu Calinescu - radu.calinescu@york.ac.uk
Colin Paterson - colin.paterson@york.ac.uk
Kenneth Johnson - kenneth.johnson@aut.ac.nz
References
R. Calinescu, K. Johnson and C. Paterson. Efficient parametric model checking using domain-specific modelling patterns. 40th International Conference on Software Engineering: New Ideas and Emerging Results (ICSE:NIER), pp. 61-64, 2018.