In this thesis, we investigate the integration of two forms of non-determinism in specification methods of open systems that 1) combine the use of state variables and actions and 2) adopt an action-based discipline of interaction. Concretely, two specification methods are presented which support two forms of non-determinism. One that concerns the situations in which the choice is controlled by the developer and the other that concerns the situations in which the choice is controlled by the environment.
Program design primitives are proposed that allow us to model three different basic notions: blocking conditions, liveness requirements and readiness requirements on action execution. These mechanisms are integrated in the Community language defined by Fiadeiro and Maibaum.
A logic specification formalism is also presented. The logic we adopt to express system properties is based on both linear temporal logic and modal logic, which are combined by the use of the branching operator A introduced by Emerson and Clarke. In order to model, in a compositional way, the co-operation properties of a system in regard to its environment, we extend the traditional notion of specification based on theories and interpretation morphisms. The key idea behind this extension is to consider that the properties that are expressed by the formulas of a specification are local and grouped according to the relations that can be established between component and system properties.
Category Theory is used as a mathematical framework for expressing the structural aspects of interaction and refinement. On the one hand, morphisms are used to express interconnections and diagrams are used to model system configurations. On the other hand, a different class of morphisms is considered. These morphisms are used to model the relationship between more abstract and more concrete specifications of a system, i.e., refinement mappings.
In the context of the categorical approach to systems design an algebraic characterization of compositionality and coordination is presented. Furthermore, notions of Software Architecture are formalised, namely, the notion of architectural connector proposed by Allen and Garlan.