In this chapter, we present applications of the inverse method using the tool IMITATOR. These applications concern both classical case studies from the literature and several industrial case studies. We consider here a range of case studies, asynchronous circuits and telecommunications protocols, and synthesize constraints for each of these case studies. We show for each example the importance of the inverse method by giving a criterion of robustness, or by optimizing some of the timing bounds of the system. Constraints synthesized by the inverse method are then compared with constraints from the literature, when applicable. In particular, we apply the inverse method to several abstractions of the SPSMALL memory sold by the chipset manufacturer ST-Microelectronics. We give for each case study sufficient details to understand the model. For a fully detailed description, the interested reader may refer to [AND 10d].
We first present in section 3.1 the tool IMITATOR. In particular, we give implementation details and explain algorithmic optimizations. We then present a range of case studies, namely: