ABD1: Formal models for verification and debug

The first paper defines an operational model for specifying application specific programmable modules, and a methodology to perform the automatic generation of safety properties as well as the formal proof of correctness of a pipelined implementation. The second paper presents a typology of programming and design faults, and characterizes them as a mutation of the design Control Dependence Graph, as a basis for a debugging procedure. In the third paper, SystemC-OSSS descriptions are transformed into a formal model called "function network", for the verification of temporal and safety requirements.