FMPAer is a formal models based performance analyzer, which is developed as an eclipse plugin. The tool can be used to create MARTE models and to evaluate the reliability, the throughput and response time of the models. A MARTE model we consider includes a use case diagram, a deployment diagram and a set of activity diagrams.
Figure 1 is the framework of FMPAer. Analysis process in FMPAer includes three steps.
Step 1: create a MARTE model of the systems under analysis.
Step 2: Transform the MARTE model to Timed Automata or extended Markov Decision Processes.
Step 3: Analyze above formal models by UPPAAL or PRISM.
Figure 1 : FMPAer Framework
Publications
1. Xue-Yang Zhu. An overview of FMPA and the design of FMPAer. Technical report, ISCAS-SKLCS-13-16, 2013.(in Chinese with English abstract)(pdf)
2. Gaogao Yan, Xue-Yang Zhu, Rongjie Yan, and Guanyuan Li. Formal Throughput and Response Time Analysis of MARTE models. 16th International Conference on Formal Engineering Methods(ICFEM 2014), accepted.(pdf)