1 Background

It is now a commonplace idea to stress the fact that industry needs tools to help in the design of (correct) computing systems. Reuse, simulation and testing have been advocated as good industrial practices that should help in devising correct products. However, recent (computer caused) disasters such as the Ariane 5 first flight [LeL96] illustrate too well how such a ``proven'' component can badly fail when inconsiderately reused.

Being a world leader in electronics products, THOMSON-CSF has engaged through its Corporate Research Laboratory a wide scale research activity in the architecture and system technologies. The long term goal is to provide tools to designers to help them design systems and verify their properties before producing a single line of code. The derivation of timing constraints and the construction of a system structure that guarantees to satisfy those constraints are the core objectives of our ongoing research.

In fact, modelling a system can be sliced in two parts [Rus97]: requirements elicitation and requirements engineering. As noted in [Rus97]:

Requirements elicitation is concerned with discovering what is wanted; [...] Requirements engineering, on the other hand, is concerned with turning the products of requirements elicitation into precise, unambiguous, and complete description of what the system under consideration is to do.

Formal methods, because they support analysis through formal deduction, are an appropriate technique in requirements engineering : its mathematical modelling and calculation oriented capability allow consequences of requirements and properties of the design to be predicted and evaluated before a line of code is written.

Our (partial) solution involves the executable description of the system architecture as being the model of the future system. A system's software architecture [GS93] and its description in an architectural description language [Ves93,Med97] are the common framework shared by clients, users, architects and developpers. A system's architecture is a set of dynamically connected dynamically created and destroyed components. Properties of the overall system are usually derived through the execution of its architecture. We aim at introducing more ``formality'' in this design process. Recent developments in formal methods [Rus96] convinced us that a formal approach to the certification of, at least the critical points, is now feasible. Thanks to the architectural approach, the designer of the (model of the) system has to reason about components and component interconnections. Components' formal specification process will force the designer to elaborate very precisely the behavior of each component, exposing ambiguities early in the design process. Formal proofs on the behaviour of composed components and its architecture execution will give the users and designers confidence in the system.

It remains to understand how formal methods and composition of well described components can harmoniously fit together in order to help ensure properties on the composed model. For instance, timing constraints are usually global constraints (time being a global variable). It is not clear whether and how they can be obtained compositionally.