Exploiting multiformalism models for testing and performance evaluation in SIMTHESys

ABSTRACT

SIMTHESys is a framework for the design of multiformalism performance evaluation models. The modeler can create new formalisms by specifying both the syntax and the dynamic behavior of their atomic elements. Even if other approaches address the same issue, the proposed methodology relies on fewer assumptions, opening new possibilities that allow to consider new types of composition and interaction between formalisms.

In this direction, this paper shows how four formalisms belonging to three different classes can interact together in a single environment. The multiformalism proposed is composed of two standard performance evaluation formalisms, a reliability formalism and a verification formalism. The potential of this approach is demonstrated by analyzing a model of an e-government process.

References

1. Christel Baier, Lucia Cloth, Boudewijn Haverkort, Matthias Kuntz, and Markus Siegle. Model checking action- and state-labelled markov chains. In Proceedings of the 2004 International Conference on Dependable Systems and Networks, pages 701--, Washington, DC, USA, 2004. IEEE Computer Society.
2. Christel Baier, Lucia Cloth, Boudewijn R. Haverkort, Matthias Kuntz, and Markus Siegle. Model checking markov chains with actions and state labels. IEEE Trans. Softw. Eng., 33:209--224, April 2007.
3. Falko Bause, Peter Buchholz, and Peter Kemper. A toolbox for functional and quantitative analysis of deds. In Proceedings of the 10th International Conference on Computer Performance Evaluation: Modelling Techniques and Tools, TOOLS '98, pages 356--359, London, UK, 1998. Springer-Verlag.
4. D. Bjørner, C. W. George, A. E. Haxthausen, C. K. Madsen, S. Holmslykke, and M. Penicka. "uml-ising" formal techniques. In Proceedings of INT'2004 - Integration of Software Specification Techniques for Applications in Engineering, Lecture Notes in Computer Science, pages 423--450. Springer, 2004. Invited paper.
5. G. Ciardo, R. L. Jones, III, A. S. Miner, and R. I. Siminiceanu. Logic and stochastic modeling with smart. Perform. Eval., 63:578--608, June 2006.
6. Graham Clark, Tod Courtney, David Daly, Dan Deavours, Salem Derisavi, Jay M. Doyle, William H. Sanders, and Patrick Webster. The mobius modeling tool. In Proceedings of the 9th international Workshop on Petri Nets and Performance Models (PNPM'01), pages 241--, Washington, DC, USA, 2001. IEEE Computer Society.
7. Tod Courtney, Salem Derisavi, Shravan Gaonkar, Mark Griffith, Vinh Lam, Michael McQuinn, Eric Rozier, and William H. Sanders. The mobius modeling environment: Recent extensions - 2005. Quantitative Evaluation of Systems, International Conference on, 0:259--260, 2005.
8. Tod Courtney, Shravan Gaonkar, Ken Keefe, Eric Rozier, and William H. Sanders. Mobius 2.3: An extensible tool for dependability, security, and performance evaluation of large and complex system models. In DSN, pages 353--358. IEEE, 2009.
9. Daniel D. Deavours, Graham Clark, Tod Courtney, David Daly, Salem Derisavi, Jay M. Doyle, William H. Sanders, and Patrick G. Webster. The mobius framework and its implementation.
10. Clemens Fischer. Csp-oz: a combination of object-z and csp. In Proceedings of the IFIP TC6 WG6.1 international workshop on Formal methods for open object-based distributed systems, pages 423--438, London, UK, UK, 1997. Chapman & Hall, Ltd.
11. F. Franceschinis, M. Gribaudo, M. Iacono, N. Mazzocca, and V. Vittorini. Towards an object based multi-formalism multi-solution modeling approach. In Proc. of the Second International Workshop on Modelling of Objects, Components, and Agents (MOCA'02), Aarhus, Denmark, August 26--27, 2002/Daniel Moldt (Ed.), pages 47--66. Technical Report DAIMI PB-561, August 2002.
12. G. Franceschinis, M. Gribaudo, M. Iacono, S. Marrone, F. Moscato, and V. Vittorini. Interfaces and binding in component based development of formal models. In Proceedings of the Fourth International ICST Conference on Performance Evaluation Methodologies and Tools, VALUETOOLS '09, pages 44:1--44:10, ICST, Brussels, Belgium, Belgium, 2009. ICST (Institute for Computer Sciences, Social-Informatics and Telecommunications Engineering).
13. Marco Gribaudo and Matteo Sereno. Gspn semantics for queueing networks with blocking. In Proceedings of the 6th International Workshop on Petri Nets and Performance Models, pages 26--, Washington, DC, USA, 1997. IEEE Computer Society.
14. Jochen Hoenicke and Ernst-Rüdiger Olderog. Csp-oz-dc: a combination of specification techniques for processes, data and time. Nordic J. of Computing, 9:301--334, December 2002.
15. Mauro Iacono and Marco Gribaudo. Element based semantics in multi formalism performance models. In MASCOTS, pages 413--416. IEEE, 2010.
16. D. Kartson, G. Balbo, S. Donatelli, G. Franceschinis, and Giuseppe Conte. Modelling with Generalized Stochastic Petri Nets. John Wiley & Sons, Inc., New York, NY, USA, 1994.
17. Brendan Mahony and Jin Song Dong. Blending object-z and timed csp: an introduction to tcoz. In Proceedings of the 20th international conference on Software engineering, ICSE '98, pages 95--104, Washington, DC, USA, 1998. IEEE Computer Society.
18. F. Moscato, F. Flammini, G. Di Lorenzo, V. Vittorini, S. Marrone, and M. Iacono. The software architecture of the osmosys multisolution framework. In ValueTools '07: Proceedings of the 2nd international conference on Performance evaluation methodologies and tools, pages 1--10, 2007.
19. Alexandre Mota and Augusto Sampaio. Model-checking csp-z: strategy, tool support and industrial application. Sci. Comput. Program., 40:59--96, May 2001.
20. Richard F. Paige. Heterogeneous notations for pure formal method integration. Formal Asp. Comput., 10(3):233--242, 1998.
21. Daniele Codetta Raiteri, Mauro Iacono, Giuliana Franceschinis, and Valeria Vittorini. Repairable fault tree for the automatic evaluation of repair policies. In DSN, pages 659--668. IEEE Computer Society, 2004.
22. R. A. Sahner, K. S. Trivedi, and A. Puliafito. Performance and Reliability Analysis of Computer Systems; An Example-based Approach Using the SHARPE Software Package. Kluwer Academic Publisher, 1996.
23. William H. Sanders, Tod Courtney, Daniel Deavours, David Daly, Salem Derisavi, and Vinh Lam. Multi-formalism and multi-solution-method modeling frameworks: The mobius approach.
24. Kishor S. Trivedi. Sharpe 2002: Symbolic hierarchical automated reliability and performance evaluator. In DSN '02: Proceedings of the 2002 International Conference on Dependable Systems and Networks, page 544, Washington, DC, USA, 2002. IEEE Computer Society.
25. V. Vittorini, G. Franceschinis, M. Gribaudo, M. Iacono, and N. Mazzocca. Drawnet++: Model objects to support performance analysis and simulation of complex systems. In Proc. of the 12th Int. Conference on Modelling Tools and Techniques for Computer and Communication System Performance Evaluation (TOOLS 2002), London, UK, April 2002.
26. Valeria Vittorini, Mauro Iacono, Nicola Mazzocca, and Giuliana Franceschinis. The osmosys approach to multi-formalism modeling of systems. Software and System Modeling, 3(1):68--81, 2004.