LeGESD: A framework oriented to the specification and formal validation of concurrent and distributed systems based on a graphical language and its process algebra semantics
DOI:
https://doi.org/10.17533/udea.redin.12492Keywords:
distributed systems, process algebra, specificationAbstract
The specification and formal verification of distributed systems is usually a complex task. It requires extensive knowledge of algorithm theory and modeling of distributed or concurrent systems. In this context, we present LeGESD which is a framework oriented to support the specification and formal validation of concurrent and distributed systems. LeGESD has a graphical formal language for the specification and analysis of distributed systems which is used to describe functional and of communication requirements. The semantics of LeGESD is based on the process algebra. This semantics is also described in this paper and it is called Analysis and Design of Distributed Systems (ADSD). ADSD is an algebraic specification with operational semantics defined to be used with LeGESD. ADSD provides graphical-algebraic equivalence relations which can be used to generate formal specifications of distributed systems. Lastly, this paper presents an example which shows the usefulness and potential of the language and its semantics.
Downloads
References
L. Arief, M. Little, S. Shrivastava, N. Speirs, S. Wheater. “Specifying distributed system services”. BT Technical Journal. (Special Issue). Vol. 3. 1999. pp. 120-128.
N. Lynch, M. Tuttle. “An introduction to input/output automata”. CWI-Quarterly. Vol. 3. 1989. pp. 219-246.
J. Cortes, F. Menchaca. Graphical Specification Language for Distributed Systems. Proceeding IEEE on 15th International Conference on Computing. México D.F. (México). 2006. pp. 120-126.
I. Kinchin, D. Hay. “How a qualitative approach to concept map analysis can be used to aid learning by illustrating patterns of conceptual development”. Educational Research. Vol. 42. 2000. pp. 43-57. DOI: https://doi.org/10.1080/001318800363908
J. Rumbaugh, I. Jacobson, G. Booch. “The unified modeling language reference manual”. Object Technology Series. Vol. 1. 1998. pp. 13-62.
D. Luckham. “Specification and analysis of system architecture”. IEEE Transactions on Software Engineering. Vol. 21. 1995. pp. 336-355. DOI: https://doi.org/10.1109/32.385971
A. Rodriguez, C. Killian. “MACEDON: Methodology for automatically creating, evaluating, and designing overlay networks”. Proceedings of the NSDI. Vol. 1. 2004. pp. 20-34.
S. Garland, N. Lynch. “The IOA language and toolset: Support for designing, analyzing, and building distributed systems”. MIT Press Technical Report. Vol. 1. 1998. pp. 1-42.
D. Regep, F. Kordon. LfP: A specification language for rapid prototyping of concurrent systems. Proceedings of the 12th International IEEE Workshop on Rapid System Prototyping. Monterey (Estados Unidos de America). 2001. pp. 90-97.
D. Zhang, K. Zhang. A Visual Programming Environment for Distributed Systems. Proceedings of the 11th International IEEE Symposium on Visual Languages. Washington (Estados Unidos de America). 1995. pp. 310-317.
J. Cortes, F. Menchaca. Algebra de Procesos Aplicada a la Especificación Formal de Sistemas Distribuidos. 1er Congreso Internacional en Sistemas Computacionales y Electrónicos. México D.F. (México). 2006. pp. 30- 38.
H. Hermanns, U. Herzog. “Process algebra for performance evaluation”. Theoretical Computer Science. Vol. 274. 2002. pp. 43-87. DOI: https://doi.org/10.1016/S0304-3975(00)00305-4
M. Bravetti, M. Bernardo. Compositional asymmetric cooperations for process algebras with probabilities, priorities and time. 1st International Workshop on Models for Time Critical Systems. Pennsylvania (Estados Unidos de America). 2000. pp. 3-16. DOI: https://doi.org/10.1016/S1571-0661(05)01220-X
K. Honda, K. Tokoro. “On Asynchronous Communication Semantics”. Object-Based Concurrent Computing. Vol. 612. 1992. pp. 21-51. DOI: https://doi.org/10.1007/3-540-55613-3_2
R. Milner. A calculus of communication systems. Ed. Springer Verlag. Nueva York (Estados Unidos de América). 1980. pp. 126-157.
Downloads
Published
How to Cite
Issue
Section
License
Copyright (c) 2018 Revista Facultad de Ingeniería
This work is licensed under a Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International License.
Revista Facultad de Ingeniería, Universidad de Antioquia is licensed under the Creative Commons Attribution BY-NC-SA 4.0 license. https://creativecommons.org/licenses/by-nc-sa/4.0/deed.en
You are free to:
Share — copy and redistribute the material in any medium or format
Adapt — remix, transform, and build upon the material
Under the following terms:
Attribution — You must give appropriate credit, provide a link to the license, and indicate if changes were made. You may do so in any reasonable manner, but not in any way that suggests the licensor endorses you or your use.
NonCommercial — You may not use the material for commercial purposes.
ShareAlike — If you remix, transform, or build upon the material, you must distribute your contributions under the same license as the original.
The material published in the journal can be distributed, copied and exhibited by third parties if the respective credits are given to the journal. No commercial benefit can be obtained and derivative works must be under the same license terms as the original work.
Twitter