Verification of control properties in the polyhedral model

Author

Cachera, David ; Morin-Allory, Katell

Author_Institution

IRISA, Rennes, France

fYear

2003

Firstpage

265

Lastpage

274

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;

fLanguage

English

Publisher

ieee

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

Type

conf

DOI

10.1109/MEMCOD.2003.1210111

Filename

1210111