O'Reilly logo

The Inverse Method: Parametric Verification of Real-time Embedded Systems by Romain Soulat, Etienne André

Stay ahead with the world's most comprehensive technology and business learning platform.

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, tutorials, and more.

Start Free Trial

No credit card required

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 image and a reference valuation π0 of the parameters that we want to generalize. It synthesizes a constraint K0 on the parameters that corresponds to a set such that, for all valuations π of parameters in this set, the trace sets of image [π0] and [π] are equal, that is the ...

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, interactive tutorials, and more.

Start Free Trial

No credit card required