Title :
Verification of control properties in the polyhedral model
Author :
Cachera, David ; Morin-Allory, Katell
Author_Institution :
IRISA, Rennes, France
Abstract :
We propose a combination of heuristic methods to prove properties of control signals for regular systems defined by means of affine recurrence equations (AREs). We benefit from the intrinsic regularity of the polyhedral model to handle parameterized systems in a symbolic way. Despite some restrictions on the form of equations we are able to handle, our techniques apply well for a useful set of properties and led us to discover some errors in actual systems. These techniques have been implemented in the MMALPHA environment.
Keywords :
computational complexity; computational geometry; embedded systems; formal verification; theorem proving; MMALPHA environment; affine recurrence equation; codesign tool; control property verification; control signal; embedded system complexity; heuristic method; intrinsic regularity; parameterized system; polyhedral model; proof method; system error discovery; Automatic generation control; Communication system control; Communication system software; Computer interfaces; Control systems; Difference equations; Embedded system; Hardware; Programming environments; Signal generators;
Conference_Titel :
Formal Methods and Models for Co-Design, 2003. MEMOCODE '03. Proceedings. First ACM and IEEE International Conference on
Conference_Location :
Mont Saint Michel, France
Print_ISBN :
0-7695-1923-7
DOI :
10.1109/MEMCOD.2003.1210111
