Polyhedral Analysis for Synchronous Languages

We define an operational semantics for the Signal language and design an analysis which allows to verify properties pertaining to the relation between values of the numeric and boolean variables of a reactive system. A distinguished feature of the analysis is that it is expressed and proved correct with respect to the source program rather than on an intermediate representation of the program. The analysis calculates a safe approximation to the set of reachable states by a symbolic fixed point computation in the domain of convex polyhedra using a novel widening operator based on the convex hull representation of polyhedra.

• Type: Conference
• Year: 1999
• Where: SAS
• Authors: Frédéric Besson, Thomas P. Jensen, Jean-Pierre Talpin
• Keywords: Convex Hull Representation, Convex Polyhedra, Formal Methods, SAS 1999, Symbolic fixed Point