2.2 Proposition

 

Many of the problems in software and hardware design are due to imprecision, ambiguity, incompletness, misunderstanding, and just plain mistakes in the statement of top-level requirements, in the description of intermediate designs, or in the specifications of components and interfaces. [Rus92]

Our current approach to the modelisation and verification problem is to define a system by its architecture. An architecture reflects the structure of a system in term of a set of its (dynamically created and destroyed) components, the nature of the connections between them, and its (dynamically evolving) topology. Each component can be described by many views depending on the peculiar properties we want to prove on their composition. Among those views, the composition rules, the behavior description formalisms and the kinds of properties to be verified are obvious choices.

Extending towards an architectural description language a programming language like Shift [DGS97] seems a better approach to make complex systems' designers confident in the possibility of specifying and verifying properties before implementation.

Our proposal is to investigate how architecture description languages can help in the design and specification of various composition operators and help in the verification process of the overall correctness.