ABD+LBSD: Formal models for design analysis

This session is devoted to the extraction of formal models from design descriptions, and their use for analysis and synthesis. The first paper proposes a formal method for the design, analysis and verification of systems for a partial reconfiguration target technology. The second paper describes a formal network model to facilitate the optimal — wrt. a given set of constraints, synthesis of interconnection networks. The third paper presents the extraction of a ForSyDe model from an untimed SystemC specification, for validation and synthesis verification. The last contribution describes a method to translate small gate-level designs into timed automata and perform detailed exhaustive timing analysis.