DOI:
https://doi.org/10.14483/23448350.608Published:
08/19/2011Issue:
No. 12 (2010): Enero-diciembreSection:
Ciencia y TecnologíaEspecificación formal de arquitecturas de software basadas en componentes: chequeo de corrección con cálculo −Parq
Formal Specification of Component-Based Software Architectures: Correctness Checking with Parq − Calculus
Keywords:
arquitectura de referencia, modelo de referencia, cálculo − ρarq, método formal, componentes de software, Sistema de Transición Rotulado, chequeo de corrección, equivalencia de observación. (es).Keywords:
Reference architecture, reference model, ρarq − Calculus, formal method, software components, labelled transition systems, correctness checking, observation equivalence (en).Downloads
Abstract (es)
En esta publicación se propone un método formal para el chequeo de corrección de arquitecturas de referencia basadas en componentes de software. Estos modelos son especificados por medio del cálculo − ρarq . Se hace uso de dos herramientas formales; la primera, el concepto de Sistema de Transición Rotulado ( STR, en adelante) ampliado con el concepto de transición condicionada para variables lógicas cuya resolución podría obtenerse desde un repositorio global de restricciones. La segunda, la teoría de equivalencia de observación propuesta por Robin Milner y sus colaboradores en la Universidad de Cambridge.Abstract (en)
In this paper we describe a correctness checking formal method of reference architectures against reference models in a component-based software development perspective. These models are specified by means of ρarq − calculus. We use two formal tools; the first, the concept of Labelled Transition System (LTS) enhanced with the conditional-transition concept for logical variables whose resolution may be obtained from a global store of constraints. The second, the observation equivalence theory proposed by Robin Milner and his collaborators in Cambridge University.References
Antonia Bertolino, P. I. and Muccini, H. (2003). Formal Methods in Testing Software Architectures. In Bernardo, M. and Inverardi, P., editors, Formal Methods for Software Architectures, Lecture Notes in Computer Science. Advanced Lectures, pages 122147. Third International School on Formal Methods for the Design of Computer, Communication and Software Systems:Software Architectures, Springer.
David Garlan /, R. T. M. and Wile, D. (1997). ACME:An Architecture Description Interchange Language. CASCON'97.
Department of Computing, Imperial College London (2007). Labelled Transition System Analyzer. http://www.doc.ic.ac.uk/ltsa/eclipse/.
Diosa, H. A. (2008). Especificaci´n de un Modelo de Referencia Arquitectural de Software a Nivel de Configuraci´n, Estructura y Comportamiento. PhD o thesis, Universidad del Valle. Doctorado en Ingeniería con Enfasis en Ciencias de la Computación.
Girault, C. and R¨diger (2003). Petri Nets for Systems Engineering.A Guide to Modeling, Verification, and Applications. Springer.
Harel, D. (1987). Statecharts: a visual formalism for complex systems. Science of Computer Programming 8, 21(8):231274.
Henry Diosa ; Juan F. Diaz and Mauricio Gaona (2005). arq : Cálculo para el Modelamiento Formal de Arquitecturas de Software Basadas en Componentes y con Restricciones en Tiempo de Ejecución. Conferencia Latinoamericana de Informática 2005.
Inverardi, P. and Tivoli, M. (2003). Software Architecture for Correct Components Assembly. In Bernardo, M. and Inverardi, P., editors, Formal Methods for Software Architectures, Lecture Notes in Computer Science. Advanced Lectures, pages 92121. Third International School on Formal Methods for the Design of Computer, Communication and Software Systems:Software Architectures, Springer.
Issarny, V. and Zarras, A. (2003). Software Architecture and Dependability. In Bernardo, M. and Inverardi, P., editors, Formal Methods for Software Architectures, Lecture Notes in Computer Science. Advanced Lectures, pages 259285. Third International School on Formal Methods for the Design of Computer, Communication and Software Systems:Software Architectures, Springer.
Jeff Kramer J. M. and Uchitel, S. (2003). Software Architecture Modeling '&' Analysis: A Rigorous Approach. In Bernardo, M. and Inverardi, P., editors, Formal Methods for Software Architectures, Lecture Notes in Computer Science. Advanced Lectures, pages 4451. Third International School on Formal Methods for the Design of Computer, Communication and Software Systems:Software Architectures, Springer.
Jeff Magee/, Naranker Dulay/, S. E. and Kramer, J. (1995). Specifying Distributed Software Architectures. Fifth European Software Engineering Conference. Joachim Niehren and Martin Muller (1995). Constraints for Free in Concurrent Computation. Asian Computer Science Conference ACSC'95.
Judith A. Stafford A. L. W. and Caporuscio, M. (2003). The Application of Dependence Analysis to Software Architecture Descriptions. In Bernardo, M. and Inverardi, P., editors, Formal Methods for Software Architectures, Lecture Notes in Computer Science. Advanced Lectures, pages 5262. Third International School on Formal Methods for the Design of Computer, Communication and Software Systems:Software Architectures, Springer.
Len Bass P. C. and Kazman, R. (1998). Software Architecture in Practice. Addison-Wesley.
Milner, R. (1999). Communicating and Mobile Systems:the -Calculus. Cambridge University Press.
Murata, T. (1989). Petri Nets: Properties, Analysis and Applications. volume 77, pages 541580. IEEE.
Nima Kaveh and Wolfgang Emmerich (2003). Validating Distributed Object and Component Designs. In Bernardo, M. and Inverardi, P., editors, Formal Methods for Software Architectures, Lecture Notes in Computer Science. Advanced Lectures, pages 6391. Third International School on Formal Methods for the Design of Computer, Communication and Software Systems:Software Architectures, Springer.
Object Management Group (2007). UML 2.1.2 Superstructure Specification.
Pahl, C. (2001). A Pi-Calculus based Framework for the Composition and Replacement of Components. OOPSLA'2001-Workshop on Specification and Verification of Component-Based Systems.
Roy, P. V. and Haridi, S. (2004). Concepts, Techniques and Models of Computer Programming. MIT Press.
Sangiorgi, D. and Walker, D. (2003). The -calculus. A theory of Mobile Processes. Cambridge University Press.
Saraswat, V. A. (1992). Concurrent Constraint Programming. The MIT Press.
Simonneta Balsamo M. B. and Simeoni, M. (2003). Performance Evaluation at the Software Architecture Level. In Bernardo, M. and Inverardi, P., editors, Formal Methods for Software Architectures, Lecture Notes in Computer Science. Advanced Lectures, pages 207258. Third International School on Formal Methods for the Design of Computer, Communication and Software Systems:Software Architectures, Springer.
Smolka, G. (1994a). A Calculus for Higher-order Concurrent Constraint Programming with Deep Guards. Technical report, Bundesminister fi£¡r Forschung und Technologie.
Smolka, G. (1994b). A Foundation for Higher-order Concurrent Constraint Programming. Technical report, Bundesminister fi£¡r Forschung und Technologie.
van Lamsweerde, A. (2003). From System Goals to Software Architecture. In Bernardo, M. and Inverardi, P., editors, Formal Methods for Software Architectures, Lecture Notes in Computer Science. Advanced Lectures, pages 2543. Third International School on Formal Methods for the Design of Computer, Communication and Software Systems:Software Architectures, Springer.
How to Cite
APA
ACM
ACS
ABNT
Chicago
Harvard
IEEE
MLA
Turabian
Vancouver
Download Citation
License
When submitting their article to the Scientific Journal, the author(s) certifies that their manuscript has not been, nor will it be, presented or published in any other scientific journal.
Within the editorial policies established for the Scientific Journal, costs are not established at any stage of the editorial process, the submission of articles, the editing, publication and subsequent downloading of the contents is free of charge, since the journal is a non-profit academic publication. profit.
