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

7

Conclusion and Perspectives

We presented in this book methods for the parametric verification of real-time systems. The inverse method algorithm for timed automata synthesizes a constraint on the delays viewed as parameters, guaranteeing the same time-abstract behavior as for a reference valuation. This has much interest in practice because, in many cases, engineers know a good reference valuation, but ignore how the system behaves around this valuation. This quantifies the system robustness: we can guarantee that the values around a given value of the delays will not impact the time-abstract overall behavior of the system. Moreover, the constraint synthesized allows for optimizing some of the timing delays, without changing the overall behavior of the system.

By iterating the inverse method on various points of a bounded parameter domain, we can partition the parametric space into good tiles and bad tiles, with respect to a given property we want to verify. This gives a behavioral cartography of the system. The main interest of this technique is that it does not depend on the property we want to verify: only the partition into good and bad tiles does. When verifying another property, the decomposition into tiles remains the same; we only need to check one point in each tile to compute the new partition into good and bad tiles.

Extensions of the inverse method have been designed for automata with stopwatches, linear hybrid automata and affine automata. Whereas the application ...