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

2

The Inverse Method for Parametric Timed Automata

In section I.2, we introduced the good parameters problem that aims at synthesizing values for timing parameters such that a concurrent real-time system behaves well. We will consider this problem in the framework of systems modeled using parametric timed automata. In this chapter, we first consider the following inverse problem: “Given a reference parameter valuation, synthesize a constraint on the parameters such that, for any valuation satisfying this constraint, the trace set of the system is the same as under the reference valuation”. This notion of equality of trace sets gives a guarantee of time-abstract equivalence of the behavior of the system. This problem can be seen as a subproblem of the good parameters problem, and we will show in Chapter 4 how this inverse problem will be used to solve the good parameters problem.

We introduce in this chapter a method for solving the inverse problem. This inverse method supposes that we are given a parametric timed automaton and a reference valuation π₀ of the parameters that we want to generalize. It synthesizes a constraint K₀ on the parameters that corresponds to a set such that, for all valuations π of parameters in this set, the trace sets of [π₀] and [π] are equal, that is the ...