Validation and Verification of Timing Properties of an Architecturally Described System.

Laurent Thomas

THOMSON-CSF Corporate Research Laboratory
Domaine de Corbeville, 91404 ORSAY Cedex, France
Tel: (+33) (0)1 69 33 92 92
Fax: (+33) (0)1 69 33 08 65
Email: thomas@thomson-lcr.fr

Abstract:

We are investigating how formal methods can help in establishing global properties of a system's model from the knowledge of properties of its components. It appears that no known model of compositionality yet fully satisfies properties preservation. A general framework for verification and simulation is needed in order to assist in the early phases of design. We strongly believe that the executable architecture description is such a framework. Properties verification, and especially timing properties verification, is of paramount importance in the correction of the systems developped by THOMSON-CSF, and is thus our primarly goal. Hybrid system modelling permits the description of components with emphasis on timing properties. However the level of description of the cooperation of such hybrid components is rather primitive. Thus, formal definitions and properties of various compositions schemas of hybrid components have to be investigated.

Keywords: Hybrid components, Validation, Verification, Architecture, Mathematical models of composition.

Workshop Goals: Networking, Brainstorming