Uma ferramenta formal para especificação e análise de arquiteturas de software

Abstract

Complex computational systems can be organized as components, that execute in a concurrent and possibly in a distributed way. The modeling of such systems has to consider coordination requirements comprising inter-component interaction styles, and intra-component concurrency and synchronization aspects. In the CR RIO framework, which makes use of meta-level and architecture configuration techniques, the coordination aspects can be treated at the software architecture level using the CBabel architecture description language (ADL). CBabel is an ADL that, besides the usual architectural primitives such as components and ports, provides contracts as first class constructions. In that way, coordination aspects can be described with CBabel contracts. Coordination aspects are encapsulated in connectors that mediate all interactions among functional modules. With this approach, one separates coordination aspects concerns from functional aspects, which do not need to be included in the design or implementation of functional modules. The use of a ADL for the specification of a system allows the system to be described in an appropriate level of abstraction allowing the analysis and verifications of architecture level properties in the initial phases of the project. But for the accomplishment of analysis of an architecture it is necessary that both the ADL and the properties to be verified have a formal semantics that gives precise and not-ambiguous meaning for them. Rewriting logic is a logic and semantic framework to which several models of computation, logics and specification languages have been mapped to, due to its unified view of computation and logic. In this dissertation, we present a formal semantics of CBabel in rewriting logic. We also present the implementation of this semantics, the tool Maude CBabel tool, a prototype executable environment for CBabel. Maude CBabel tool is implemented on top of the Maude system, a fast realization of rewriting logic with support to reflection and with a good variety of analysis tools. With Maude CBabel tool during the modeling of complex systems, we can formally analyze CBabel architectural descriptions, identifying possible problems and suggesting solutions still in the initial phase of its life cycle.