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

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 Chapter_4_image002a.gif and a rectangular real-valued parameter domain V0, what is the largest set of parameters values for which Chapter_4_image002a.gif 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 ...

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