Publications

Model-Driven Software Development is nowadays taken as a mainstream methodology. In the software engineering community, it is a synonym of the OMG Model-Driven Architecture (MDA). However, in the formal method community, model-driven development is broadly seen as model-based techniques for software design and verification. Because of the difference between the nature of research and practical model-driven software engineering, there is a gap between formal techniques, together with their tools, and their potential support to practical software development. In order to bridge this gap, we define the meanings of component-based software architectures in this chapter, and show how software architectures are formally modeled in the formal model-driven engineering method rCOS. With the semantics of software architecture components, their compositions and refinements, we demonstrate how appropriate formal techniques and their tools can be applied in an MDA development process.

 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.