Publications

 We present a new automata-based interface model describing the
  interaction behavior of software components. Contrary to earlier
  component- or in\-terface-based approaches, the interface model we
  propose specifies all the non-blockable interaction  behaviors of a
  component with any environment. To this end, we develop an algorithm
  to compute the unblockable interaction behavior, called the
  \emph{interface model of a component}, from its execution
  model. Based on this model, we introduce composition
  operators for the components and prove important
  compositionality results, showing the conditions under which
  composition of interface models preserves unblockable sequences of
  provided services.

Model-driven architecture (MDA) has become a main stream technology for software-intensive system design. The main engineering principle behind it is that the inherent complexity of software development can only be mastered by building, analyzing and manipulating system models. MDA also deals with system complexity by providing component-based design techniques, allowing independent component design, implementation and deployment, and then system integration and reconfiguration based on component interfaces. The model of a system in any stage is an integration of models of different viewpoints. Therefore, for a model-driven method to be applied effectively, it must provide a body of techniques and an integrated suite of tools for model construction, validation, and transformation. This requires a number of modeling notations for the specification of different concerns and viewpoints of the system. These notations should have formally defined syntaxes and a unified theory of semantics. The underlying theory of the method is needed to underpin the development of tools and correct use of tools in software development, as well as to formally verify and reason about properties of systems in mission-critical applications. The modeling notations, techniques, and tools must be designed so that they can be used seamlessly in supporting development activities and documentation of artifacts in software design processes. This article presents such a method, called the rCOS, focusing on the models of a system at different stages in a software development process, their semantic integration, and how they are constructed, analyzed, transformed, validated, and verified.