The Inverse Method: Parametric Verification of Real-time Embedded Systems

3

The Inverse Method in Practice: Application to Case Studies

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].

Outline of the chapter

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:

• the flip-flop circuit from the introduction (section 3.2);
• a sample example of “SR-latch” (section 3.3);
• an “AND–OR” circuit (section 3.4);
• the Root Contention Protocol (section 3.5);
• the Bounded Retransmission Protocol (section 3.6);
• the Carrier sense multiple access with collision detection (CSMA/CD) protocol ...