Behavioural Analysis of Component-Based Systems

Software Engineers continue to search for efficient ways to build high quality systems. Two contrasting techniques that promise to help with the effective construction of high quality systems are the use of formal models during design and the use of components during development. In this paper, we take the position that these techniques work well together. Hardware Engineers have shown that building systems from components has brought enormous benefits. Using components permits hardware engineers to consider systems at an abstract level, making it possible for them to build and reason about systems that would otherwise be too large and complex to understand. It also enables them to make effective reuse of existing designs. It seems reasonable to expect that using components in software development will also bring advantages. Formal methods provide a means to reason about a program (or system) enabling the creation of programs which can be proved to meet their specifications. However, the size of real systems makes these methods impractical for any but the simplest of structures constructing a complete formal specification for a commercial system is a daunting task. Using formal methods for the whole of a large commercial system is not practical, but some of the advantages of using them can be obtained where a system is to be built from communicating components, by building and evaluating a formal model of the system. We describe how a model of a system to be implemented using COM might be constructed using a particular modelling tool, RolEnact. We discuss the extent to which validation of the model contributes to the validity of the eventual solution