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

4

Behavioral Cartography of Timed Automata

In Chapter 2, we introduced the inverse method, allowing us to synthesize constraints on a system modeled by parametric timed automata. Starting from a reference valuation of the parameters, the inverse method synthesizes a constraint such that, for any valuation satisfying this constraint, the trace set of the system is the same as under the reference valuation. However, the inverse method suffers from two limitations. First, the constraint synthesized by the method is not necessarily maximal, that is there may exist parameter valuations outside the constraint such that the behavior is the same as under the reference valuation. Second, the method focuses on the equality of trace sets, which can be seen as a strong property, because the good behavior of a timed system can correspond to different trace sets.

Recall from section 1.2 that we are interested in solving the following good parameters problem: “Given a parametric timed automaton and a rectangular real-valued parameter domain V₀, what is the largest set of parameters values for which behaves well?” In this chapter, we present an approach for solving this problem, based on the inverse method. By iterating the inverse method on the integer points of the rectangular parametric domain ...