Formal modeling and quantitative analysis of KLAIM-based mobile systems

ABSTRACT

KLAIM is an experimental language designed for modeling and programming distributed systems composed of mobile components where distribution awareness and dynamic system architecture configuration are key issues. In this paper we propose STOCKLAIM, a STOchastic extension of cKLAIM, the core subset of KLAIM. cKLAIM includes process distribution, process mobility, and asynchronous communication. The extension makes it possible to integrate the modeling of quantitative aspects of mobile systems--- e.g. performance---with the functional specification of such systems. We present a formal operational semantics of STOcKLAIM, which associates a labeled transition system to each STOcKLAIM network and a translation to Continuous Time Markov Chains for quantitative analysis. We also show how STOcKLAIM can be used by means of a simple example, i.e. the modeling of the spreading of a virus.

REFERENCES

• 1: Christel Baier , Boudewijn R. Haverkort , Holger Hermanns , Joost-Pieter Katoen, Automated Performance and Dependability Evaluation Using Model Checking, Performance Evaluation of Complex Systems: Techniques and Tools, Performance 2002, Tutorial Lectures, p.261-289, January 2002
• 2: Christel Baier , Joost-Pieter Katoen , Holger Hermanns, Approximate Symbolic Model Checking of Continuous-Time Markov Chains, Proceedings of the 10th International Conference on Concurrency Theory, p.146-161, August 24-27, 1999
• 3: L. Bettini, R. De Nicola, and M. Loreti. Formulae meet Programs over the Net: a Framework for Reliable Network Aware Programming, 2003. (submitted for publication. Available at: http: //music. dsi.unif.it).
• 4: L. Bettini, V. Non, R. De Nicola, G. Ferrari, D. Gorla, M. Loreti, E. Moggi, R. Pugliese, E. Tuosto, and B. Venneri. The Klaim Project: Theory and Practice. In C. Priami, editor, Global Computing: Programming Environments, Languages, Security and Analysis of Systems, volume 2874 of LNCS, pages 88--150. Springer-Verlag, 2003.
• 5: J. Bradley and N. Davies. Reliable Performance Modeling with Approximate Synchronisations. In J. Hillston and M. Silva, editors, Proceedings of the 7th workshop on process algebras and performance modeling, pages 99--118. Prensas Universitarias de Zaragoza, September 1999.
• 6: P. Buchholz, J.-P Katoen, P. Kemper, and C. Tepper. Model-checking Large Structured Markov Chains. The Journal of Logic and Algebraic Programming. Elsevier, 56(1--2):69--96, 2003.
• 7: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 8: C. Courcoubetis and M. Yannakakis. Verifying Temporal Properties of Finite State Probabilistic Programs. In 29th Annual Symposium on Foundations of Computer Science, pages 338--345. IEEE Computer Society Press, 1988.
• 9: Rocco de Nicola , Gian Luigi Ferrari , Rosario Pugliese, KLAIM: A Kernel Language for Agents Interaction and Mobility, IEEE Transactions on Software Engineering, v.24 n.5, p.315-330, May 1998 [doi>10.1109/32.685256]
• 10: R. De Nicola, D. Latella, and M. Massink. Formal modeling and quantitative analysis of KLAIM-based mobile systems. FULL VERSION. Technical Report 2004-TR-25, Consiglio Nazionale delle Ricerche, Istituto di Scienza e Tecnologie deirinformazione 'A. Faedo', 2004.
• 11: A. Di Pierro, C. Hankin, and H. Wiklicky. Probabilistic KLAIM. In R. De Nicola, G. Ferrari, and G. Meredith, editors, Coordination Models and Languages, volume 2949 of LNCS. Springer-Verlag, 2004.
• 12: Alessandro Fantechi , Stefania Gnesi , Gianluca Mazzarini, How Expressive Are LOTOS Behaviour Expressions?, Proceedings of the IFIP TC6/WG6.1 Third International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols: Formal Description Techniques, III, p.17-32, November 05-08, 1990
• 13: David Gelernter, Generative communication in Linda, ACM Transactions on Programming Languages and Systems (TOPLAS), v.7 n.1, p.80-112, Jan. 1985 [doi>10.1145/2363.2433]
• 14: Stephen Gilmore , Jane Hillston , Leila Kloul , Marina Ribaudo, PEPA nets: a structured performance modelling formalism, Performance Evaluation, v.54 n.2, p.79-104, 1 October 2003 [doi>10.1016/S0166-5316(03)00069-5]
• 15: D. Gorla and R. Pugliese. A Semantic Theory for Global Computing Systems, 2004. (Submitted for publication. Available at http://www.dsi.uniromal.it/~gorla/papers/bis4k-full.pdf).
• 16: Sergiu Hart , Micha Sharir(, Probabilistic temporal logics for finite and bounded models, Proceedings of the sixteenth annual ACM symposium on Theory of computing, p.1-13, December 1984 [doi>10.1145/800057.808660]
• 17: Boudewijn R. Haverkort, Markovian models for performance and dependability evaluation, Lectures on formal methods and performance analysis: first EEF/Euro summer school on trends in computer science, Springer-Verlag New York, Inc., New York, NY, 2002
• 18: Oltea Mihaela Herescu , Catuscia Palamidessi, Probabilistic Asynchronous pi-Calculus, Proceedings of the Third International Conference on Foundations of Software Science and Computation Structures: Held as Part of the Joint European Conferences on Theory and Practice of Software,ETAPS 2000, p.146-160, March 25-April 02, 2000
• 19: Holger Hermanns , Joost-Pieter Katoen , Joachim Meyer-Kayser , Markus Siegle, Towards Model Checking Stochastic Process Algebra, Proceedings of the Second International Conference on Integrated Formal Methods, p.420-439, November 01-03, 2000
• 20: Udo Feldkamp , Hilmar Rauhe , Wolfgang Banzhaf, Software Tools for DNA Sequence Design, Genetic Programming and Evolvable Machines, v.4 n.2, p.153-171, June 2003 [doi>10.1023/A:1023985029398]
• 21: Vidyadhar G. Kulkarni, Modeling and analysis of stochastic systems, Chapman & Hall, Ltd., London, UK, 1995
• 22: Marta Z. Kwiatkowska , Gethin Norman , David Parker, Probabilistic Symbolic Model Checking with PRISM: A Hybrid Approach, Proceedings of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, p.52-66, April 08-12, 2002
• 23: C. Priami. Stochastic π-Calculus. The Computer Journal. Oxford University Press., 38(7):578--589, 1995.
• 24: Håkan L. S. Younes , Reid G. Simmons, Probabilistic Verification of Discrete Event Systems Using Acceptance Sampling, Proceedings of the 14th International Conference on Computer Aided Verification, p.223-235, July 27-31, 2002

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Formal methods

General Terms:
Languages, Performance, Verification

Keywords:
coordination languages, formal modeling and validation, mobile systems, stochastic behavior