WO2016078715A1

WO2016078715A1 - Method and device for verifying a persistence property of a dynamical technical system

Info

Publication number: WO2016078715A1
Application number: PCT/EP2014/075152
Authority: WO
Inventors: Jan Richter
Original assignee: Siemens AG; Siemens Corp
Current assignee: Siemens AG; Siemens Corp
Priority date: 2014-11-20
Filing date: 2014-11-20
Publication date: 2016-05-26
Anticipated expiration: 2017-05-20

Abstract

A method for checking whether a system remains in a pregiven part of state space shall be provided, i.e. the system shall be proven to be positive invariant. Therefore, a method for automatically verifying a persistence property of a design of a dynamical technical system is suggested, including the steps of providing a discrete-time state model of the technical system, providing at least one formal requirement for the technical system, formulating a mixed integer optimization problem on the basis of the discrete-time state model and the formal requirement, checking whether all solutions of the mixed integer optimization problem reach a pregiven polytope (P) in a state space in a pregiven time, each solution representing a state of the technical system, and checking whether one solution of the mixed integer optimization problem within the polytope (P) leaves the polytope after one pregiven time step and delivering a respective result.

Description

Method and device for verifying a persistence property of a dynamical technical system

The present invention relates to a method for automatically verifying a persistence property of a design of a dynamical technical system.

This invention addresses the process of verifying the satisfaction of formal requirements within the Systems

Engineering process. Formal requirements refer to products or engineered artefacts, as we call them throughout this invention. Mechanical components, electrical circuits, hydraulic circuits, etc. as well as combinations of such things, are examples of engineered artefacts. Within the scope of this invention, Systems Engineering is understood as an interdisciplinary process that typically involves

mechanics, electricity, electronics, hydraulics etc.

simultaneously .

With the current invention, we aspire to enhance the systems engineering process by formal methods. Using formal methods may greatly speed up the design cycles, which becomes increasingly relevant due to unbroken trends towards smaller production lots and more product variants in shorter time, culminating in built-to-order concepts.

The automotive industry is forced to release new variants of its cars in 6 month cycles, which tend to shorten.

Maintaining high product quality while keeping R&D and test costs at acceptable levels is becoming more and more of a challenge. This invention tries to contribute to making this complexity manageable.

A typical design validation technique used today is the numerical simulation of sets of test scenarios, e.g. using simulation tools such as LMS Amesim, MATLAB Simulink, Dymola, etc. Today, the simulation process for design validation consists the following steps:

1. Requirement formulation in natural language, by nature somewhat vague and open to ambiguous interpretation.

2. Translation of the requirements into simulation scenarios: initial conditions, selection of external input trajectories, and characterization of desired simulation outputs.

3. Simulation and interpretation of the results.

In this connection it is referred to F. Liang, W. Schamai, 0. Rogovchenko, S. Sadeghi, M. Nyberg, P. Fritzson: Model-based requirement verification: a case study, Proc. 9^th Modelica Conference Munich, pp. 385-392, 2012 which, despite its title, talks about simulation.

Checking whether or not the engineered artifacts together satisfy the requirements is a task that is typically

performed by a group of experts that is distinct from the designers .

The problem with this approach is that one never knows when the simulation results can be trusted, due to issues with numerical algorithm stability, rounding error effects, and sensitivity towards uncertain parameters. This lack of confidence is particularly disturbing in connection with safety requirements, where one needs to ensure that a system never enters dangerous regions of its state space.

The above problem has been approached in multi-domain Systems Engineering by:

Requirements formulation in prose/natural language.

Interpretation of prose requirements by developers, designers and testers.

Tests, either automatically generated scenarios or manually selected test scenarios (See also the paper "Model-based Requirement Verification") . Sufficiently many design/test loops.

Simulation experts for setting up trustworthy

simulations .

In parts of embedded system design microprocessor industry formal verification methods complementing simulation-based tests have been established. In fact, this industry is an early adopter of such methods, since the verification problems met there are typically single-domain, namely involving discrete logic. Involved methods are: logical equivalence checking, finite state machine (FSM) equivalence checking, model checking and theorem proving.

Up to now bounded model checking is known in the sense that all properties are proven only on a finite time horizon. For certain liveness properties, bounded model checking is unsatisfactory because liveness properties are per definition expressed without time bounds. Hence, an extension is needed.

Temporally unbounded model checking is commonplace in discrete verification, but a rare concept for hybrid systems (mixed continuous/discrete systems) verification. So far, only one method for unbounded model checking of MLD systems is known, E.M. Wolff and R.M. Murray: "Optimal Control of Mixed Logical Dynamical Systems with Long-Term Temporal Logic Specifications" (Persistent URL:

http://resolver.caltech.edo/CaltechCDSTR:2013.001) . It is quite restrictive and conservative, since it requires the presence of an infinite repetitive cycle that must be repeated in exactly the same way over and over again.

The object of the present invention is to provide a method which facilitates verification of a persistence property of a design of a dynamical technical system. Furthermore, a corresponding engineering system shall be provided.

According to the present invention this object is solved by a method for automatically verifying a persistence property of a design of a dynamical technical system, the method

including the steps of

- providing a discrete-time state model of the technical

system,

- providing at least one formal requirement for the

technical system,

- formulating a mixed integer optimization problem on the basis of the discrete-time state model and the formal requirement ,

- checking whether all solutions starting from admissible initial conditions of the mixed integer optimization problem reach a pregiven polytope in a state space in a pregiven time, each solution representing a state of the technical system, and

- checking whether there exists at least one two-step

solution of the mixed integer optimization problem

starting within the polytope and leaving the polytope after one time step and delivering a respective result.

Additionally, there is provided a method for automatically verifying a persistence property of a design of a dynamical technical system, the method including the steps of

- pregiving a class of functions with at least one parameter in a state space of the technical system,

- providing at least one formal requirement for the

technical system, the at least one formal requirement separating allowed states and forbidden states of the technical system in the state space,

- formulating a mixed integer optimization problem on the basis of the class of functions and the at least one formal requirement and

- determining a barrier between said allowed states and said forbidden states by solving said mixed integer

optimization problem and delivering a respective result.

The current invention addresses the behavioral verification of liveness properties on an infinite time horizon preferably in mixed-logical dynamical (MLD) models. Technically, this invention is based on two alternative ideas:

1. The verification of positive invariance for target regions in variable space, and

2. The verification of barrier certificates for unsafe regions in variable space

This invention is helpful for creating a dedicated Systems Engineering product that allows top-down engineering

according to the RFLP framework (requirements, functional models, logical models, physical models) . According to expert consensus, tangible amounts of time and money are wasted in early top-down engineering phases, due to missing feedback from design validation. This invention opens the way for design validation techniques at the level of logical

component models "L", before the detailed engineering of components that results in the physical "P" models.

The two methods described here allow unbounded-in-time property verification without imposing infinite repetitive cycles. Such cycles never exist in perturbed systems under the influence of external disturbances.

Preferably the discrete-time state model is a mixed-logical dynamical model. Such a mixed-logical dynamical model can be expressed with few state equations and inequations.

Furthermore, the discrete-time state model may be formulated in the language HYSDEL. HYSDEL is a higher-level language so that the models do not need to be expressed directly in the MLD format (Mixed-Logical Dynamical) .

The formal requirement of the dynamical technical system may be formulated by temporal logic with signal abstraction. Such temporal logic allows for unambiguously formulating

behavioural requirements of the technical system. Furthermore, all possible solutions of the mixed integer optimization problem are checked whether each solution within the polytope leaves the polytope after the pregiven one time step or not. This ensures that the complete state of space is checked and a reliable persistence statement can be given for the technical system.

Additionally, there may be provided an engineering system designed to perform one of the methods described above. Such engineering system can provide a behavioural verification of liveness properties on an infinite time horizon.

The present invention will now be described in more detail in connection with the attached drawings showing in:

FIG 1 a counter example of a positive invariant set of solutions of a mixed integer optimization problem;

FIG 2 a production system as example; and

FIG 3 an automotive drivetrain as further example.

The following embodiments are specific example of the present invention. The features described within the examples are depicted in a specific combination. However, the features may also be implemented in another combination or may be used separate from other features.

The aim of the following example is unbounded-in-time property verification without imposing infinite repetitive cycles. For the respective solutions presented here some preliminaries are necessary here. Such preliminaries relate to models as described in following formula (1) and to formal requirements formulated in following formula (2) .

Referring to the article of A. Bemporad and M. Morari:

"Control of systems integrating logic, dynamics and

constrains", Automatica 35 (1999, pages 407-427) and specifically to paragraph "3. Mixed logical dynamical (MLD) Systems" on page 409-415 the design artefacts may be

represented by discrete-time mixed-logical dynamical (MLD) models of the form x(t + 1)= Ax{t) + B_uu(t) + B_auxw(t) + B_l

y(t)= Cx(t) + D_uu(t) + D_auxw(t) + D_aff (1)

E_xx(t) + E_uu(t) + E_auxw(t)<E_aff (index sets) J_X,J_U,J_W,J ,J ineq x is the state vector of a system, y is the output vector and the discrete time period is given by t e Z . u represents a control signal, i.e. an input signal including noise and w represents an auxiliary signal vector for expressing certain classes of non-linear functions. The fixed parameters A, B., C., D., E. with different indices usually have the form of matrices . Formal requirements are represented as temporal logic (LTL) formulas φ with signal abstraction built from atomic propositions p conforming to the following Backus-Naur grammar

where are the negation, disjunction, next, and until operators . An atomic proposition p can be either true (T) or false (-L) . For convenience, further logical operators constructed from the above ones are admitted, namely

conjunction (Λ), implication ( => ) , equivalence ( ) eventually (0), and always (°) . Signal abstraction is achieved by comparing affine functions of signals to

Two different approaches to unbounded verification are described now. One of them, positive invariant sets, is we suited to check persistence properties, whereas the other one, barrier certificates, is well suited to check safety properties .

Positive Invariant Set Method

A persistence specification demands that a solution

obeying dynamics (1) reaches a polytope target set PP in finite time and stays within ° forever. Such a set is called positive invariant under dynamics (1) .

The polytope set P is described as an intersection of half- spaces

with matrix HH and vector ^ , each of compatible

dimensions. The rows of W describe the orientation of facets of , and rows of ^ describe corresponding offsets from the origin .

Persistence can be proven by a complete induction argument, showing that

1. all solutions reach the set P in finite time >0 _r and

2. all solutions that start in P remain in under

application of the dynamics (1) for one time step.

3. By induction, the solution remains in for all times t≥ T,t e Nt T.ten .

Step 1 is a classical reachability test. In this test is checked, whether each state reaches the pregiven polytope P (see left side of FIG 1) in a state space xi , X2 within in a pregiven time period T. This requirement is expressed as an LTL formula φ = {t≥ T] => {JC( e P} where the inclusion test x(t) εί³ is written in shorthand notation; what is really checked is the constraint

P : Hx(t) < k. This verification step is done on finite time horizon.

Step 2 of the verification serves for checking whether each state of the polytope P remains within in the polytope P, so that the system is positive (for the future) invariant. This step 2 is expressed by the following problem, which can be checked completely independently of Step 1 . Note that it is logically negated by asking whether there exist initial state conditions -^(1) *O)within ^ that leave P in one step (see right side of FIG 1 ) . Note that one time step is sufficient, since all initial conditions in P are checked.

Check whether there exists any admissible II E U _f W G W , any initial condition i(l) e P and a next state x(2) such that x(2) = Axil) + B_uu(l) + B_aiaw(l) + B_aff

E_xx(\) + E_uu(\) + E_aiaw(\)≤E_aff

E_xx(2) ₊ E_uu(2) + E_auxw(2)≤E_aff

Hx(l)≤ k

h_ix(2)>k_i for some row index i where is the ⁱ th row of matrix Ή , and '^fi is the ⁱ th row of vector ^ . The first three lines of the (un) equation system represent the model for the transition of the discrete point of time t=l to t=2. The fourth line represents the condition that all states are within the polytope P at time point t=l . The last line shows the condition that one state leaves the polytope P at time point t=2 . If this mixed-integer program (i.e. mixed-integer

optimization problem) is infeasible, then the set P has been proven to be positive invariant under the dynamics ( 1 ) . A feasible counterexample solution is shown in FIG 1. Since such a solution was found, P is not positive invariant in FIG 1. Contrariwise, if no such solution exists, is positive invariant .

Barrier certificate method

Metaphorically, a barrier certificate helps verifying a safety property by establishing a reliable barrier between possible evolutions of the system variables and forbidden areas. The key advantage of this approach is the strong degree of abstraction from the details of possible variable evolutions. Such barrier certificate are known from the article of S. Prajna et al . : "Safety Verification of Hybrid Systems Using Barrier Certificates" in "Hybrid Systems:

Computation and Control", 7^th international workshop, HSCC 2004, Philadelphia, PA, USA, March 25 to 27, 2004, pages 477- 492; ISBN 978-3-540-21259-1. A barrier certificate for a dynamical system x = f{x.u) ,

l e l c f , u e U , x(0) e X_Q and a forbidden area S c l in state space is a function E X \- > R that is differentiable with respect to its argument and satisfies the following

conditions :

E(X)≤ Ofor x e X₀

— f(x, d)≤0for x G R"

dx In other words, there is a pregiven class of functions E (x) with at least one parameter x in a state space of the technical system. Formal requirements determine whether these functions are greater or smaller than zero. Additionally, it is required that the function of the forbidden area is differentiable and the differential is less than zero. On the basis of these inequalities a mixed integer optimization problem is formulated. The solution of this problem leads to a barrier function which separates the allowed states and the forbidden states.

The existence of a barrier function E with these qualities implies that the forbidden area B is never reached from any initial condition x_n e X_n .

The present invention thus allows an unbounded model checki procedure without the need for repetitive cycles through positive invariant sets . An integration into a tool set for systems engineering is possible.

In an advantageous variant of the invention, the models for the components of the technical system are expressed not directly by discrete-time mixed-logical dynamical (MLD) models, but in higher-level language such as HYSDEL.

A concrete example referring to a simple production system is shown in FIG 2. The system consists of two tanks 8, 9 filled by inputs ui and U2, which deposit material on a transport belt 10 in a desired proportion, adjustable by means of the outlet valves. The packer unit 11 will then combine the material mix into packages 12, which shall come out of the production system at a desired rate.

The objective would be, from startup conditions, to exceed a minimum required production rate fttt __n bounded time

(time > 1 min ute) => \ 50 P^ackaS^es < _prate < 70 P^ackag^es I

minute minute J

A verification method not presented here might confirm that the desired production rate can be achieved.

The method of the present invention can show that the region

minute minute J

indeed positive invariant; hence, the system will remain there for all future times in spite of the perturbations

As further example consider an automotive drivetrain

consisting of an engine 13, gear 14, differential 15, axes 16, and tires 17. An example for a relevant safety

requirement is that the torque on the main shaft never exceeds a bound. This property would be accessible based on a barrier certificate. An example for a relevant persistence requirement is that the engine cooling circuit reaches its target temperature band robustly under all ambient conditions and remains there henceforth, given that the engine keeps running .

Additional application domains may include embedded systems verification, especially mixed-signal designs: although formal methods originate from microprocessor design dominated by discrete behaviors, this invention may be attractive for that domain, at least as far as mixed signal designs are concerned. Mixed signals (digital/analogue or, in

optimization parlance, discrete-continuous signals) occur naturally in the class of mixed-integer optimization problems and solvers, which are the basis of our invention.

List of reference signs

8 tank

9 tank

10 transport belt

11 packer unit

12 packages

13 engine

14 gear

15 differential

16 axes

17 tires i, u₂ input

Claims

1. Method for automatically verifying a persistence property of a design of a dynamical technical system, the method including the steps of

- providing a discrete-time state model of the technical system,

- providing at least one formal requirement for the

technical system,

- checking whether all solutions (x (t ) ) starting from

admissible initial conditions (x(0)) of the mixed integer optimization problem reach a pregiven polytope (P) in a state space in a pregiven time, each solution (x(t)) representing a state of the technical system, and

- checking whether there exists at least one two-step

solution (x(l) and x(2)) of the mixed integer optimization problem starting within the polytope (P) (x(l) in P) and leaving the polytope (P) after one time step (x(2) not in P) and delivering a respective result.

2. Method for automatically verifying a persistence property of a design of a dynamical technical system, the method including the steps of

- providing at least one formal requirement for the

optimization problem and delivering a respective result.

3. Method according to one of the preceding claims, wherein the model is a mixed-logical dynamical model.

4. Method according to one of the preceding claims, whe the model is formulated in the language HYSDEL.

5. Method according to one of the preceding claims, wherein the formal requirement is formulated by temporal logic with signal abstraction.

6. Method according to one of the claims 1, 4 and 5, wherein all possible solutions of the mixed integer optimization problem are checked whether each solution within the polytope (P) leaves the polytope after the pregiven one time step or not .

7. Engineering system designed to perform the method

according to one of the preceding claims.