Title :
From Data to Events: Checking Properties on the Control of a System
Author :
Jacquet, Christophe ; Boulanger, Frederic ; Marcadet, Dominique
Author_Institution :
SUPELEC, Gif-sur-Yvette
Abstract :
We present a component-based description language for heterogeneous systems composed of several data flow processing components and a unique event- based controller. Descriptions are used both for generating and deploying implementation code and for checking safety properties on the systems. The only constraint is to specify the controller in a synchronous reactive language. We propose an analysis tool which transforms temporal logic properties of the system as a whole into properties on the events of the controller, and hence into synchronous reactive observers. If checks succeed, the final system is therefore correct by construction. When properties cannot be translated exactly into observers of the control, our tool is capable of generating approximate observers. In this case, the results are subject to interpretation, but can prove useful and help detect defects or even guarantee the correctness of a system.
Keywords :
data flow analysis; data flow computing; component-based description language; data flow processing components; event-based controller; heterogeneous systems; synchronous reactive language; Automatic control; Automatic generation control; Control system synthesis; Control systems; Data processing; Flexible printed circuits; Formal verification; Logic; Safety; Signal design;
Conference_Titel :
Formal Methods and Models for Co-Design, 2008. MEMOCODE 2008. 6th ACM/IEEE International Conference on
Conference_Location :
Anaheim, CA
Print_ISBN :
978-1-4244-2417-7
DOI :
10.1109/MEMCOD.2008.4547682