[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ Skip to main content
Springer Nature Link
Log in

Behavioural models for distributed Fractal components

  • Published:
annals of telecommunications - annales des télécommunications Aims and scope Submit manuscript

Abstract

This paper presents a formal behavioural specification framework for specifying and verifying the correct behaviour of distributed Fractal components. The first contribution is a parameterised and hierarchical behavioural model called pNets that serves as a low-level semantic framework for expressing the behaviour of various classes of distributed languages and as a common internal format for our tools. Then, we use this model to define the generation of behavioural models for applications ranging from sequential Fractal components, to distributed objects, and finally to distributed components. Our models are able to characterise both functional and non-functional behaviours and the interaction between the two concerns. Finally, this work has resulted in the development of tools allowing the non-expert programmer to specify the behaviour of his components and (semi)automatically verify properties of his application.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
£29.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (United Kingdom)

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7
Fig. 8
Fig. 9
Fig. 10
Fig. 11
Fig. 12
Fig. 13
Fig. 14

Similar content being viewed by others

Notes

  1. Cleaveland and Riely [25] was using a slightly relaxed condition called “galois insertions”.

  2. http://www-sop.inria.fr/oasis/Vercors.

References

  1. Bruneton E, Coupaye T, Leclercp M, Quema V, Stefani J (2004) An open component model and its support in java. In: 7th int symp on component-based software engineering (CBSE-7), LNCS, vol 3054. Springer

  2. CoreGRID, Programming Model Institute (2006) Basic features of the grid component model (assessed). Technical report, Deliverable D.PM.04. http://www.coregrid.net/mambo/images/stories/Deliverables/d.pm.04.pdf

  3. Milner R (1989) Communication and concurrency. Prentice Hall, Englewood Cliffs ISBN 0-13-114984-9

  4. Bergstra J, Pose A, Smolka S (2001) Handbook of process algebra. North-Holland, Amsterdam

    MATH  Google Scholar 

  5. Arnold A (1994) Finite transition systems. Semantics of communicating sytems. Prentice-Hall, Englewood Cliffs

    Google Scholar 

  6. Milner R, Parrow J, Walker D (1992) A calculus of mobile processes. Inf Comput 100(1):1–77

    Article  MATH  MathSciNet  Google Scholar 

  7. Garavel H, Lang F, Mateescu R, Serve W (2007) CADP 2006: a toolbox for the construction and analysis of distrbuted processes. In: CAV 2007 conference. Berlin, Germany

  8. Garavel H, Lang F (2002) NTIF: a general symbolic model for communicating sequential processes with data. In: Proceedings of FORTE’02 (Houston), LNCS, vol 2529. Springer

  9. Roscoe A (1994) Model-checking CSP. In: A classical mind, essays in honour of C.A.R. Hoare. Prentice-Hall, Englewood Cliffs

    Google Scholar 

  10. Scattergood J (1998) The semantics and implementation of machine-readable CSP. PhD thesis, Oxford Un. Computing Laboratory

  11. Magee J, Kramer J (2006) Concurrency: state models and java programs, 2nd edn. Wiley, New York

    Google Scholar 

  12. Poizat P, Royer J, Salaun G (2006) Bounded analysis and decomposition for behavioural descriptions of components. In: FMOODS, LNCS, vol 4037. Springer

  13. Poizat P, Royer J (2006) A formal architectural description language based on transition systems and modal logic. J Univers Comput Sci 12(12):1741–1782

    Google Scholar 

  14. Barros T, Boulifa R, Madelaine E (2004) Parameterized models for distributed Java objects. In: Forte’04 conference. LNCS, vol 3235. Springer, Madrid

    Google Scholar 

  15. Boulifa R (2004) Génération de modèles comportementaux des applications réparties. PhD thesis, University of Nice - Sophia Antipolis – UFR Sciences

  16. Barros T, Henrio L, Madelaine E (2005) Behavioural models for hierarchical components. In: Godefroid P (ed) Model checking software, 12th int SPIN workshop, LNCS, vol 3639. Springer, San Francisco

    Google Scholar 

  17. Barros T (2005) Formal specification and verification of distributed component systems. PhD thesis, University of Nice - Sophia Antipolis

  18. Caromel D, Delbé C, di Costanzo A, Leyton M (2006) ProActive: an integrated platform for programming and running applications on grids and P2P systems. Comput Methods Sci Technol 12(1):69–77

    Google Scholar 

  19. Caromel D, Henrio L, Serpette B (2004) Asynchronous and deterministic objects. In: Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on principles of programming languages. ACM, New York, pp 123–134

    Chapter  Google Scholar 

  20. Caromel D, Henrio L (2005) A theory of distributed object. Springer, Heidelberg

    Google Scholar 

  21. Lin H (1996) Symbolic transition graph with assignment. In: Montanari U, Sassone V (eds) CONCUR ’96, LNCS, vol 1119. Pisa, Italy

  22. Lakas A (1996) Les Transformations Lotomaton: une contribution à la pré-implémentation des systèmes Lotos. Ph.D. thesis, Univ. Paris VI

  23. Najm E, Lakas A, Serouchni A, Madelaine E, de Simone R (1992) ALTO: an interactive transformation tool for LOTOS and LOTOMATON. In: Bolognesi T, Brinksma E, Vissers C (eds) Third lotosphere workshop and seminar, Pisa

  24. Madelaine E (1992) Verification tools from the CONCUR project. In: Rozenberg G (ed) EATCS Bull, vol 47. B. Rovan, Bratislava

  25. Cleaveland R, Riely J (1994) Testing-based abstractions for value-passing systems. In: CONCUR’94, LNCS, vol 836. Springer, Heidelberg

    Google Scholar 

  26. Cleaveland R, Hennessy M (1993) Testing equivalence as a bisimulation equivalence. Form Asp Comput 5:1–20

    Article  MATH  Google Scholar 

  27. Attali I, Barros T, Madelaine E (2004) Formalisation and proofs of the chilean electronic invoices system. In: Proc. of the XXIV international conference of the Chilean computer science society (SCCC’04). IEEE, Arica

    Google Scholar 

  28. Barros T, Cansado A, Madelaine E, Rivera M (2006) Model checking distributed components: the Vercors platform. In: 3rd workshop on formal aspects of component systems. ENTCS, Prague

    Google Scholar 

  29. Ahumada S, Apvrille L, Barros T, Cansado A, Madelaine E, Salageanu E (2007) Specifying fractal and GCM components With UML. In: Proc of the XXVI international conference of the Chilean computer science society (SCCC’07). IEEE, Iquique

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Universidad de Chili, Ejército 441, Santiago, Chile

    Tomás Barros

  2. GET/ENST/LabSoC, Telecom Paristech, BP 193, 06904, Sophia-Antipolis Cedex, France

    Rabéa Ameur-Boulifa

  3. INRIA Sophia-Antipolis, CNRS, UNSA, INRIA, Oasis. 2004, Route des Lucioles, BP 93, 06902, Sophia-Antipolis Cedex, France

    Antonio Cansado, Ludovic Henrio & Eric Madelaine

Authors
  1. Tomás Barros
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Rabéa Ameur-Boulifa
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Antonio Cansado
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Ludovic Henrio
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Eric Madelaine
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Eric Madelaine.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Barros, T., Ameur-Boulifa, R., Cansado, A. et al. Behavioural models for distributed Fractal components. Ann. Telecommun. 64, 25–43 (2009). https://doi.org/10.1007/s12243-008-0069-7

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s12243-008-0069-7

Keywords

Search

Navigation