Systems and Methods for Verifying Train Controllers

Related Applications

[0001] This application claims the benefit of U.S. Provisional Patent Applications Nos. 63/276,225, filed November 5, 2021 and 63/290,860, filed December 17, 2021, the contents of which are incorporated herein in their entireties.

Government Interest

[0002] This invention was made with United States Government support under contract 693JJ620C000025 awarded by the Federal Railroad Administration Office of Research, Development and Technology. The U.S. Government has certain rights in the invention.

Background

[0003] Embedded software for many complex cyber-physical systems, for example, trains, planes, and self-driving cars is safety critical. Errors can have disastrous consequences. To ensure the safety of controllers, formal verification with computer-checked, repeatable mathematical proofs presents a particularly trustworthy method for controller design.

[0004] Automated train control improves railroad operation by safeguarding the motion of trains while increasing efficiency by enabling motion within a safe envelope. Train controllers decide when to slow trains down to avoid collisions with other trains on the track, stay inside movement authorities, and navigate slopes, curves and tunnels safely. These systems must base their decisions on detailed motion models to guarantee the absence of overshoot of the movement authority (safety) and limit undershoot (efficiency).Train controllers decide when to enforce braking to prevent movement authority violation and collisions. They must account for all the competing influences that govern train motion. Uphill slopes, for example, decrease velocity, which decreases resistance, which permits a more rapid increase in velocity, slope and curve effect, all while the train's brake force builds gradually until saturation as air pressure propagates along brake pipes. These complex interactions make it hard to design a safe and efficient train controller, and even harder to ensure it is always safe.

[0005] Train controllers are assessed relative to a (changing) destination stopping point- called end of movement authority. An overshoot of the end of movement authority is a safety violation, because that risks collision with other trains. The efficiency of the train controller is measured in terms of end of movement authority undershoot.

[0006] Existing studies of formally verified train motion do not account for at least two effects amongst track grade, track curvature, resistance, and air brake propagation time, rendering their results inapplicable to most real-world scenarios. The kinematics of a train can be described by a kinematics model. For example, the Federal Railroad Administration has developed such a model, referred to here as the FRA model. [0007] Verification against the full dynamics of the FRA model, in which these effects interact subtly with each other is a challenge. Verification of the FRA model would be significant, because these parameters influence the motion of the train in safety-critical and/or performance-critical ways. Neglecting track slope profile and the gradual propagation of air pressure braking, in particular, can render otherwise verifiably safe train controllers unsafe, since their influence may diminish the train's ability to decelerate, causing collisions.

Summary of the Invention

[0008] The embodiments described herein use formal verification as a tool to design and verify a train controller, which is a practically important, representative problem with challenges common in other safety-critical embedded systems: complex dynamics with transcendental arithmetic, competing forces with subtle interaction, and effects whose exact magnitude is unknown at proof time.

[0009] Before verifying the safety of a controller, the controller must first be designed. Controllers balance efficiency with provable safety. Conservative controllers are mathematically more simplistic, and easier to design and verify, but make railway operations inefficient, but violate performance objectives. A conservative safe controller is first described, and then iteratively made more efficient through the exploitation of characteristics of the physical train dynamics for better but safe control. [0010] The absence of end of movement authority overshoot is proven when using the controller on the FRA model by verification and efficiency is demonstrated by simulation.

[0011] To keep the proofs as general and widely applicable as possible, nondeterministic controllers and a paradigm of mathematical abstraction are leveraged. Each controller is intentionally built to be set-valued such that all of its control choices are simultaneously proved safe under all circumstances in the FRA model. The safety of these controllers implies the safety of all their specializations, giving railroads significant freedom in how to adapt the verified controllers for their purposes.

[0012] Controller verification follows a two stage process. First, mathematical models of abstract train control motion are proven. Second, proofs of the actual physical models of train control are obtained by uniform substitution to replace the abstract function symbols of the mathematical models with physical terms specific to the FRA model or even specific railroads.

[0013] Crucially, the disclosed embodiments use three different types of models: (i) the high-fidelity physics model describing the kinematic motion of trains along the track; (ii) the generalized mathematical abstractions of the physics model disclosed herein; and (iii) simplified but computable approximations of motion models disclosed herein (e.g., Eqs. (4), (5), (12) etc.) and used by the respective train controllers. [0014] The verification provided by the disclosed embodiments proves that the safety of (i) derives from the safety of (ii) and that all control decisions following (iii) are safe in (ii). The proof is written in differential dynamic logic and performed using a hybrid systems theorem prover.

[0015] It should be noted that the embodiments are explained in the context of the FRA model, but it is to be understood that the techniques could be applied to any train kinematics model.

Brief Description of the Drawings

[0016] FIG. 1 is a block diagram showing the relationship between different train models.

[0017] FIG. 2 is a listing of the mathematical model (referred to herein as "Model 1") for train control expressed as a hybrid program of the train's stopping distance.

[0018] FIG. 3 is a listing of the mathematical model (referred to herein as "Model 2") expressed as a hybrid program of the train dynamics.

[0019] FIG. 4 is a listing of the mathematical model (referred to herein as "Model 3") expressed as a hybrid program of the train dynamics split in to three evolution domains.

[0020] FIG. 5 is a listing of the mathematical model (referred to herein as "Model 4") of a train controller and train dynamics, expressed in Taylor polynomials.

[0021] FIG. 6 is a listing of the mathematical model (referred to herein as "Model 5") of a train controller in the kinematic motion model.

[0022] FIG. 7 is a graph showing the base enforcement algorithm showing an undershoot. [0023] FIG. 8 is a graph the base enforcement algorithm with offsets showing an overshoot.

[0024] FIG. 9 is a graph showing an optimized verified controller (Model 5) that limits undershoot.

[0025] FIG. 10 is a graph showing the base enforcement algorithm showing an undershoot for an underpowered train on a crest from 3% uphill to -3% downhill.

[0026] FIG. 11 is a graph the base enforcement algorithm without offsets showing an overshoot.

[0027] FIG. 13 is a graph showing an optimized verified controller (Model 5) that limits undershoot.

Detailed Description

[0028] The embodiments described herein utilize formal verification using differential dynamic logic (DDL) as a tool to design and verify a train controller. This is a practically important, representative problem with challenges common in other safety-critical embedded systems: complex dynamics with transcendental arithmetic, competing forces with subtle interaction, and effects whose exact magnitude is unknown at proof time.

[0029] The disclosed embodiments provide a novel, formal verification of the safety of the Federal Railroad Administration freight train kinematics model with all its relevant forces and parameters, including track slope and curvature, air brake propagation, and [0030] resistive forces as computed by the Davis equation. Due to the significant competing influence of these parameters on train stopping distances, even designing train controllers is a nontrivial control challenge, which is solved using formal verification.

[0031] For increased generality at reduced verification effort, symbolic mathematical generalizations of the train control models are verified and efficient uniform substitutions are subsequently applied to obtain verification results for physical train control models.

[0032] Differential Dynamic Logic - DDL is a logic with a deductive proof system for hybrid systems. DDL extends first-order logic with the notion of hybrid programs. A hybrid program runs according to a binary relation between states, mapping start states to end states that a program could reach. The program constructs include assignment, for example, which instantaneously assigns expression to variable x. In the special case of nondeterministic assignment, the transition relation accounts for any possible real value being assigned to x.

[0033] The test operator, as in ? F, aborts the current run if formula F is false. The continuous evolution operator, follows the ordinary differential equation (ODE) for some nondeterministic amount of time, with evolution domain constraint Q being true throughout the evolution. Sequential composition runs program a followed by program for example, the discrete train controller followed by the train's ODE The nondeterministic choice operator runs either program for example, to either accelerate the train with a or brake with The loop operator a* runs hybrid program a any non-deterministically chosen times. It is important for running a train control loop indefinitely. To express safety properties about hybrid programs, the box modality is used, which is true in any state from which all runs of hybrid program end in states in which the formula F is true.

[0034] For proofs of DDL formulas, DDL inference rules are used. The rules most relevant to the disclosed embodiments are loop (loop), differential invariant (di), and differential cut (dC).

[0035] The loop rule uses an invariant J that holds initially, inductively after each step, and implies the post condition that is to be proven. A differential invariant preserves properties along the flow of a differential equation: if initially and grows slower than e ₂ , so (where and are evaluated after substituting in the assignment from the differential equation), then it remains true that The idea behind a differential cut is that if formula C holds true at the end of every possible run of differential equation then C must hold true throughout its evolution. Differential cuts can be used to accumulate knowledge about a differential equation.

[0036] FRA Model of Train Kinematics - The FRA model, provides the forces acting on a train and is expressed in Eq. (1). After the net force on the train has been identified, Newton's second law, using train mass, determines the acceleration that the train experiences, which in turn determines change in velocity and change in position for train control design. The forces are where:

F _G denotes force due to track grade;

F _c is resistance due to track curvature;

F _B is the braking force;

F _L is the force from the locomotive engine (tractive effort)

F _R is resistive forces; and m _T is the train mass.

[0037] Newton's second law, determines train acceleration a. Resistive force

F _R follows the modified Davis equation: where A _R , B _R , C _R , D _R are experimentally determined positive constants, the numerical value of which, given a choice of units, can be found in other sources. Further, n is the number of axles, and w is the weight of the train.

[0038] Grade and curve forces depend on the train position p on the track. Grade force is proportional to train weight w and average track grade grade p) underneath the train:

[0039] Similarly, curve force is a function of average track curvature curve p) along the train and train weight w: where A _c and A _G are positive multiplicative constants.

[0040] Braking force can be modeled as the minimum of two linear functions to capture the effect of air pressure brake force buildup and stabilization. where:

F _BO is the force acting immediately on brake application; f _p is the slope with which brake force increases; t is the elapsed time; and

F _Bmax is the force after air pressure in the air pressure brakes saturates. [0041] Brake enforcement and train protection algorithms approximate a solution to a differential equation derived from Eq. (1) to estimate the velocity and position of the train at future times.

[0042] Mathematical Model Abstraction - To maximize generality of the embedded software design, minimize verification effort, and simplify future proof maintenance, a mathematical abstraction of the FRA model is disclosed. Concrete verified controllers and their safety proofs for the fully expanded model can be obtained automatically from the verified abstract model by uniform substitution.

[0043] The abstract train kinematic model in Eq. (2) below is an ODE in time. The rate of change of position is velocity, and the rate of change of velocity is acceleration. The variables and constants involved, along with their signs, when relevant, are (i) train position p; (ii) velocity v; (iii) velocity and position-independent component of acceleration ranging from immediate braking ability to maximum train engine acceleration acceleration due to air brakes a _a in range (v) rate of change m _b of air brake acceleration, which is when the brakes are ramping up and 0 otherwise; (vi) map a _s from position to acceleration due to grade; (vii) map a _c from position to acceleration due to curvature; and (viii) velocity-dependent resistance a _r . In the chosen sign convention, resistive acceleration is negative. with: and

[0044] The resistance is given by the Davis equation: which has the shape when with gravity g summarizes the linear coefficient of velocity, and summarizes the quadratic coefficient. Grade and curvature are represented by unspecified but bounded functions a _s and a _c that map train positions to a numeric value for acceleration due to slope and average curvature, respectively. The quantity a summarizes locomotive tractive effort and train deceleration as commanded by the train controller, with adjustment for the velocity-independent resistance.

[0045] The proven abstract kinematic train model is then instantiated by uniform substitution of DDL to obtain proofs for specific physical kinematic train models such as the FRA model. Similarly, proofs for specific train configurations result from substituting values for coefficients, or even for a specific train state when additionally substituting speed and position.

[0046] Model Structure

[0047] A conservative train controller is first developed in DDL based on the abstract train kinematic model given by Eq. (2). The challenge of representing track grade and curve, which are unknown at proof time, are addressed using unspecified maps. To reason about them, the maps are bounded with assumptions quantifying over all arguments. The solution of the disclosed embodiments permits the capture of the full Eq. (2) without conservatively neglecting a _s (p) and a _c (p) when reasoning about it during verification. It generalizes to other embedded software that must reason about unspecified, bounded functions, such as noise or potential fields (e.g., electro-magnetic or gravitational effect).

[0048] The conservative controller is then proven to be safe. Relative to Eq. (2), the controller will provably never permit the train's position to exceed the end of movement authority e, although it might be inefficient, braking unnecessarily early. By revising modular components and functions to be more arithmetically sophisticated in provable safety can be retained and the controller made more efficient. FIG. 1 shows the relationship between the resulting controller models.

[0049] Model Description - The train controller consists of a time control loop. The control has a latency of time T > 0. The controller has to wait at most this long before being able to change the throttle position. In practice, reaction time (latency) T is typically on the order of 1 second, but train controllers often keep decisions in effect for a 10 second period without revising them. Every control cycle, the controller computes an over-approximation stopDist(p, v, a _b ~) of the stopping distance, the distance that the train will travel before stopping if it were to accelerate during the current control cycle, but then brake continuously starting at the next control cycle, until it comes to a halt. If the distance left to the end of movement authority e exceeds stopDist(p, v, a _b ), the controller continues free driving (with any acceleration or deceleration choice within the physical limits of the train), otherwise it brakes. This control cycle, is parametric in stopping distance stopDist, and expressed as a hybrid program in Model 1, shown in FIG. 2.

[0050] Train Dynamics - Model 2, shown in FIG. 3, describes the physical motion of the train according to the abstract mathematical model of Eq. (2) augmented with a clock t' = 1 to switch back to control after at most time T. All constants are left as symbolic and safety is proven for all values, so that individual railroads have the flexibility to instantiate them with the values that apply to their system but inherit the safety results of the disclosed embodiments. This generality in controller design comes at the cost of higher proof complexity but compared to the alternative where these constants would be initialized with a conservative value, this allows for more efficient, tailored controllers adapted to the specific rail operation.

[0051] Stopping Distance - To decide between free driving and braking, the controller computes the upper bound on the distance covered over one time period of acceleration and subsequently braking to a stop. Thus, the models provide two distinct specifications of the distance that the train will take to stop. The first, indirect specification is through the differential equation in Model 2 that implicitly describes the physical motion of the train. The second, approximate specification is stopDist in Line 2 of Model 1, an explicit arithmetic expression that the controller can evaluate efficiently to make decisions at runtime. Efficiency concerns demand that stopDist(p, v, a _b ) be as tight as possible. If the bound is too large, the controller enforces braking unnecessarily. But verifiable safety requires stopDist(p, v, a _b ) to provably be an upper bound on the distance that the train covers (as determined by the dynamic model). The tightest possible bound is the exact solution of the differential equation. However, even ignoring the effect of air brakes, the differential equation requires trigonometric solutions. Transcendental function arithmetic is undecidable. To ensure mathematical provability, polynomial approximations are developed, which is a delicate design task because automated decision procedures for polynomial real arithmetic validity are computationally expensive. This constrains the complexity of the polynomial approximations that can be used as upper bounds. A balance can be struck between conflicting concerns: striving for efficiency while satisfying mathematical provability.

[0052] To illustrate this approach, start with a simple conservative expression for stopDist. This expression is proved safe for the full model including slope, curve friction, air brake propagation, and aerodynamic drag. The approximation is then improved, focusing on one contributing factor at a time.

[0053] Conservative Stopping Distance - A conservative controller will now be constructed by instantiating control loop with an expression for stopDist and proving it safe. Referring back to the train dynamics in Eq. (2), an upper bound for v is first needed. Integrating this bound via p' = v computes a stopping distance upper bound.

[0054] The first impediment to obtaining a provable upper bound for v is that grade and curvature maps a _s and a _c are arbitrary functions, constrained only by upper and lower bounds, and bounded gradients. At runtime, the train knows their exact values as the controller is instantiated with maps for the railroad it runs on. However, these maps are unknown at proof time. And yet, the proof has to show safety of the train control ahead of time for all possible track maps in order to justify safety of the train controller. To obtain a provable upper bound on stopping distance, the proof is therefore based on the limited information that we do have about the maps: upper bounds on the potential values of a _s and a _c .

[0055] A naive upper bound on a _s is the value of acceleration that the train experiences when it is on the steepest permissible downward slope, m _s . The proof shows that the distance required to stop for any permissible grade map cannot exceed the distance computed with the steepest downward slope. It first shows that the true acceleration is bounded above by an acceleration that uses the highest permissible value of grade acceleration, then that actual velocity cannot exceed the velocity computed using the worst-case acceleration, and consequently, that traveled distance cannot exceed the stopping distance computed using the worst-case estimate of velocity.

[0056] Accounting for grade force is important. On a downward hill, for example, a train with a controller that ignores grade would roll forward even at the end of its movement authority which may cause accidents. In contrast, curve resistance can be safely ignored when approximating stopDist, because resistances shorten stopping distance (upper bound 0). These simplifications result in differential equation because while the train is accelerating, where v ₂ is the upper bound on v that is integrated to compute stopDist. However, the solution v ₂ (t) is still transcendental:

[0057] The culprits are the linear and quadratic terms in velocity from the Davis equation.

With another simplification of 0 as an upper bound for a _r (resistance always works against the train's motion), a polynomial expression is derived for stopDist: where: and are the initial values of speed and position.

[0058] The solutions provide a conservative stopping distance bound.

[0059] Where the first and second terms represent the distance while accelerating and the third term represents the stopping distance from increased speed. [0060] The conservative stopping distance stopDistj, ignores its arguments p and a _b , but later refinements of stopDist functions also depend on p and a _b , which is why they are passed in.

[0061] The first two terms are the distance covered by the train in one control cycle of acceleration, while the third term is the distance that the train needs to stop should it start braking right after, assuming the worst-case value of 0 for a _a . This conservative distance is adjusted to account for grade force with its worst-case accelerating or decelerating effects. Substituting Eq. (4) into control cycle a results in the DDL hybrid program of the conservative controller:

[0062] A physically important quantity is braking distance, the distance that the train will travel before coming to a stop should it start braking right now. an upper bound, is derived, which will be crucial to the proofs and the initial assumptions and is improved upon later. [0063] The last term of Eq. (4) is with v ₃ according to Eq. (3) when

[0064] Initial assumptions init(brakeDist) parametrized by brakeDist, and initAirbrake (assumptions on air brakes) are required to prove the conservative controller safe. Assumptions about unspecified functions are represented by universal quantification over their input. This representation permits derivation of a formula about the unspecified function at any point of the train's evolution by substituting the quantified input with current values.

[0065] Theorem 1 is the DDL formula representing the safety of the conservative controller:

[0066] Theorem 1: The conservative braking controller guarantees that the train always remains within the end of the movement authority. The DDL formula below is provable, where a is the control loop from Model 1 parameterized with Eg. (4) for stopDist.

[0067] The proof has been done in the theorem prover KeYmaera X, but the central ideas are disclosed here. Loop invariant is used and split into cases for free driving and braking corresponding to the nondeterministic choice in Lines 2-5 of Model 1. On braking, the invariant is maintained because the derivative of the distance that the train will take to come to a stop does not exceed the derivative of the distance to the end of movement authority On free driving for a control period T, the train maintains a distance to the end of movement authority of at least stopDist adjusted for time t since the last control decision: by dC and di. The required inequality relation between the derivatives: holds because

[0068] Safe Efficiency Improvements

[0069] To make our controller more efficient, the over-approximation for stopping distance must be improved. The FRA model presents two challenges common in embedded controllers: it uses functions whose exact values are unknown at proof time (slope and curve maps) and has many interacting forces. The disclosed techniques address these problems with two general principles: using quantified worst case bounds on unknown functions, and separation of dependencies. The first technique relies on the observation that the track changes are gradual and predictable (the rate of change of unknown functions is bounded). It drastically improves bounds on the effect of grade and curve over one time period of acceleration, after resolving circular dependencies between the variables of motion. The second technique improves the estimate brakeDist by accounting for air brake dynamics. It demonstrates a handling of triple integration, using modesplitting to deal with the non-analytical change of behavior when brakes saturate. The third technique uses Taylor polynomials to capture the effect of resistance, which would otherwise lead to transcendental arithmetic.

[0070] Bound on Gradient - The train controller knows the current slope and vertical curves of the track, which determine transitions from one track grade to another. This knowledge results in a bound on the difference in grade per unit length:

[0071] The second inequality follows from the first using the chain rule and p' = v. After time T, a _s could have increased by no more than where it is some upper bound on v over the course of T time

[0072] Bound on Curve Resistance - Similar to bounding the gradient change, an upper bound on the rate of change of curve resistance can be computed as a function of velocity using track geometry. Curve resistance depends on average curve curve(p). Assume that the tightest permissible curvature for the railroad corresponds to radius r. The greatest change in average curvature occurs when a train goes from a track with the greatest permissible curvature to a straight track (or vice versa). Over a small period of time dt, the portion of the train transitioning from greatest curvature to 0 curvature is dv, where v is velocity. So the rate of change of curve(p) (taken in radians) with respect to time is where I is the length of the train. For a given train, a _c relates to curve with some constant multiplicative factor q. In this case, use with the constant factor

[0073] With this bound on the maximum rate of change of we now estimate the upper bound on curve resistance over time T, where is initial train position, to be:

As before, it is an upper bound on velocity for duration T.

[0074] Tight Stopping Distance Approximation - The upper bounds a _s on gradient and a _c on curve resistance are summarized as:

[0075] This enables improvement of the estimation of stopping distance: [0076] Upper bound v ₄ is tighter than v ₃ of Eq. (3) and thus integrates to an improved stopping distance estimate. It depends (transitively through a _s and a _c ) on the unknown upper bound it on velocity, which is still needed to estimate provably correctly.

[0077] Circular Dependencies - The upper bound on velocity, it, is undefined in Eq, (7) above. The bound cannot be used for it, since itself is phrased in terms of it. The problem is a circular dependency between a _s and v the bound on slope acceleration a _s depends on speed v, while the upper bound on speed v, in turn, depends on slope acceleration a _s and likewise for a _c . Physically, this is because if the train is moving faster, less is known about the nature of the track (e.g., its curve and slope) after the passage of some time, as the train is farther from its previous position on the track. However, information about the grade curve is needed to better estimate the velocity at which the train is traveling. To cut through these circular dependencies, the conservative estimations of these quantities are used as a base case to bootstrap incrementally finer computations, as presented below.

[0078] The initial upper bounds for and 0 for are used to get a conservative bound so that Because is ^a positive upper bound on the train's acceleration, velocity could have increased no more than Hence, it is indeed an upper bound on v through the T time interval. Substituting this it refines the gradient and curve resistance bounds.

[0079] These expressions give the chosen definitions of and by replacing placeholder velocity bound

[0080] In principle, this upper bound could be further improved on speed by using v ₄ to obtain an even better bound on and which could in turn yield an improved bound on v. However, extra levels of extrapolation increase proof cost and computation time when the controller is run. Each extra intermediate bound requires a constant number of extra steps in the proof, but provides diminishing efficiency gains in return. Intuitively, proof length is asymptotically linear in number of iterations because under optimal proof rule application ordering, each iteration induces one extra application of rule dC to introduce the intermediate bound into the proof tree, and rule dl to justify this intermediate bound.

[0081] The stopDist expression below uses v ₄ with to estimate stopping distance, which is sufficiently tight to make useful control decisions.

[0082] Further initial assumptions are needed to prove the improved slope-exploiting controller safe. These assumptions represent the result of the track environment discussion used for the computer-checked proof. [0083] This technique applies to time-triggered controllers (where a control loop runs with some known maximum latency and sensors measure current state every cycle) for physical systems with functions affecting the environment that are unknown except for bounds on their rate of change. The future value of the functions can be bounded in terms of their worst-case rate of change. Furthermore, these bounds can be used to compute bounds on other variables in the system, just as here a bound on velocity was used to bound slope and curve effect, which was again used to obtain a better bound on velocity. The situation arises frequently in practice: examples of unknown functions are a potential field, or a noise or error effect, which may have circular dependence with position.

[0084] Theorem 2: The slope-estimating controller guarantees that the train stays within its movement authority. The DDL formula below is provable, where a is the control loop from Model 1 parameterized with Eg. (8) for stopDist.

[0085] The proof (by proof in KeYmaera X) builds on the ideas from Theorem 1. The loop rule is applied with the same loop invariant as Theorem 1. If the train brakes, differential invariant rule dl again shows that the loop invariant holds throughout differential equation evolution.

[0086] If the train chooses to accelerate, then as before, the train maintains at least a distance of stopDist _s adjusted for time t since the last control decision. Unlike before, instead of m _s accounts for worst-case and instead of 0 accounts for worst-case Again, dl proves that this adjusted inequality remains true. To prove the required inequality on the derivatives, differential cut rule dC is used to show throughout the control cycle, and There are two branches for each cut corresponding to how the min in a _s and c resolve. For example, using initial position and velocity and for it is necessary to show that and While the former follows from the quantified assumption on a _s (p), to prove the latter, elapsed time is adjusted for t, to argue that proved using di. The required derivative inequality follows from instantiating the quantified assumption bounding the rate of change of with the current position and showing that it is an upper bound on v in the control loop. The argument for a _c is analogous.

[0087] Effect of Air Pressure Brakes - The term brakeDistj, conservatively neglects the significant effects of air brakes to avoid reasoning about their time dependence. A tighter brakeDist _a that accounts completely for air brakes will now be derived. It specifies a controller that simultaneously benefits from the slope and curve estimation previously discussed, and from air brake dynamics. The central insight required to prove the improved controller safe is how to compose reasoning about time-dependent air brake propagation and velocity-dependent slope and curve estimations. The component of stopDist affected by air brakes, brakeDist _a is first shown to be the desired upper bound on distance to brake throughout the control loop. Then, holding brakeDist _a constant, the differential reasoning on slope and curve estimation previously described is performed. The two results together permit an overall proof of safety of the air brake-exploiting controller.

[0088] To derive the improved brakeDist _a , some intermediate functions from air brake dynamics are first computed. In Eq. (2), during brake ramp-up, with slope relaxed pessimistically to m _s , and curve and resistance to 0, max evaluates to a _b , and m _b to m _p . The solution for v in the resulting differential equation v' = is quadratic in t:

[0089] Function t _b in Eq. (11) computes the time the train takes to achieve full braking by subtracting current brake buildup a _b from maximal air braking and dividing by the rate of increase in air brake force m _p . If the train comes to a stop before air brake saturation, it instead evaluates to the time until the train stops, as computed by solving Eq. (10) for v = 0.

[0090] The distance that the train travels before either stopping or reaching maximum air brake effect is:

[0091] The velocity of the train after this period of buildup, by Eq. (10), is: [0092] So, after the brakes finished ramping up, the distance traveled until the train comes to a halt is: using Newton's third equation of motion. If the train stops before finishing brake ramp-up, v? evaluates to 0, as required. Adding the upper bounds on distance traveled before and after brake ramp-up results in brakeDist _a (v, a _b ) in Eq. (12) below, an upper bound on braking distance that accounts for the effect of air brakes. While this derivation for controller design is manual, its result will be verified by computer-checked proof in Theorem 3 below. stopDist _a (p, V, a _b ) [0093] To prove the invariant that after a control cycle of braking, e — p > three dynamically distinct cases must be considered: (i) when evaluates to

[0094] The model dynamics are split into these three evolution domains, branching between the three possibilities in a loop to transition between modes freely (Model 3, shown in FIG. 4). This does not affect the semantics of evolution: per train dynamics, mode transition happens at most once (from (ii) to (i) or (ii) to (iii)). Unrolling the loop to two iterations, one per mode, suffices to model train behavior. This split formulation simplifies syntactic proofs.

[0095] Theorem 3: The air-brake-exploiting controller guarantees that the train stays within its movement authority. The DDL formula below is provable, where a is the control loop from Model 1 parameterized with Eg. (12) for stopDist.

[0096] The high level idea of the proof (in KeYmaera X) is to use an outer loop invariant and again split into free driving and braking cases. On braking, the outer loop invariant is maintained in each of the three dynamics modes using an inner loop invariant consisting of 4 formulas, the most important of which is

[0097] On free driving: is truly an upper bound on all reachable values in the control cycle. Then, holding constant, a proof similar to that for Theorem 2 is followed to show that, in every mode, the increase in p does not exceed the decrease in distance buffer

The free driving inner loop invariant consists of 14 formulas, most of which state that various upper bound expressions (such as on velocity, grade and curve) remain upper bounds over the course of the loop. By monotonicity, then, e — p >

[0098] Exploiting Resistance - Exactly accounting for the quadratic dependence of resistance on velocity, as discussed above, leads to an undecidable, transcendental exact solution for stopping distance. The controller must instead use an approximation. Because polynomial arithmetic is decidable, Taylor polynomials are a natural way to obtain decidable approximations. The disclosed embodiments apply Taylor approximations to the FRA model, identifying techniques generalizable to verified control for other embedded systems with transcendental dynamics.

[0099] The Davis equation implies The first-order Taylor polynomial of this expression for velocity is

[0100] Using this approximation at time as an upper bound for velocity after a time period of acceleration, Eq. (13) is computed for stopping distance that leverages resistance. While this derivation is manual, its result will be verified by computer-checked proof in Theorem 4 below.

[0101] Unlike previous stopping distance estimates, this expression is not always an upper bound. It uses resistance for the original velocity v _Q , which is only a conservative bound when resistance is low enough to permit acceleration. This condition is captured by predicate vbound in Eq. (14):

[0102] For the Taylor approximation controller (Model 4), the predicate is defined in Eq. (15), which, unlike previous expressions for stopping distance, returns a truth value. It uses previous definitions from Eq. (13), vbound. From Eq. (14) to determine when is applicable, and stopDistj, from Eq. (8) is used as a fallback. [0103] Higher order Taylor polynomials permit analogous reasoning. Theorem 4 expresses that the Taylor polynomial controller in Model 4, shown in FIG. 5, is safe.

[0104] Theorem 4: The Taylor polynomial controller guarantees that the train stays within its movement authority. The DDL formula below is provable:

[0105] The proof (in KeYmaera X) starts by showing that the loop invariant from Theorem 3 is maintained (using DDL rule loop). The case where the train is braking proceeds similar to Theorem 3. When the train is accelerating, a showing that the controller has insisted on a sufficient distance margin (stopping distance), so that even after a time period, the train has enough space to stop, is necessary. As the Taylor polynomial computes the stopping distance, it must be proven that it actually is an upper bound. A monotonicity argument is used by introducing an auxiliary variable that represents a "ghost" train, perpetually traveling down worst possible slope and curve This isolates slope and curve from the effect of resistance, breaking interdependence. The Taylor polynomial result, derived on the ghost train, shows that it goes no slower than the real train, and that consequently the Taylor polynomial result must hold for the real train. Other elements of the proof remain similar to Theorem 1. [0106] Kinematic Train Model Proofs

[0107] A proof for the FRA model derives from the proof for the abstract mathematical models (e.g., Theorem 4), by uniform substitution, which replaces abstract function symbols with specific terms using the correspondence previously discussed. Model

5, shown in FIG. 6, lists the model resulting from substitution.

[0108] A corollary posits that the kinematic train model is safe. That is, the train controller for the FRA model never overshoots the end of movement authority. The following formula is provable with

[0109] Here is the proof. By uniform substitution from Theorem 4, using the substitutions below:

[0110] Evaluation

[0111] For validation, ModelPlex can be used to derive a controller monitor from Model 5 that measures the safety margin in decisions of previous brake enforcement controllers and the verified control presented herein. That way, measurements of if, and how well, the verified train controllers and existing controllers agree can be used to assess the safety of those existing systems and the efficiency of the model. Existing brake enforcement controllers brake to a full stop once engaged.

[0112] The ModelPlex monitor computes a robustness measure indicating how close a decision is to losing the safety proof. When the robustness measure is positive, the decision is guaranteed to remain provably safe so that the system enjoys the safety proof of the verified model. When it is negative, emergency brakes should be applied for safety reasons. The ModelPlex controller monitor follows the structure of the verified model when it computes robustness. For example, a monitor for Lines 2-3 of Model 5 describes their effect with the formula which translates to the robustness measure.

[0113] The most important elements of the full Model 5 monitor are: (1) in free driving (when is satisfied) it combines remaining position margin, that is, the larger of Taylor margin when vbound(v), or fallback margin e — p — stopDist _a with acceleration choice robustness from control decision and speed robustness. That is, v from evolution domain and (2) during braking, which is always allowed, it measures speed robustness, that is, v per evolution domain constraint.

[0114] Because the robustness measure of ModelPlex combines multiple quantities of incompatible units, there is no direct interpretation of its magnitude, but only of its sign. For validation, the train model of Eq. (2) was implemented in Python by numerical integration, instantiating the model parameters per the FRA model. These parameter values are estimated from train test runs and standards and require careful consideration of their units.

[0115] The evaluation compares start braking and stopping points of trains, highlighting braking performance in terms of overshoot (safety risk) and undershoot (performance objective of a maximum undershoot of 1000ft) of the end of movement authority. The baseline controllers were implemented using numeric forward Euler integration to simulate the model to determine the stopping distance. The verified controllers neither use numeric integration nor include the dynamic model, but instead decide based on the stopping distance overapproximation from Eq. (15).

[0116] The most interesting train behavior arises from the subtle interplay between air pressure propagation, aerodynamic/roll resistance, and acceleration/deceleration due to slope. It peaks on crests that change gradient from uphill to downhill and in troughs that change gradient from downhill to uphill. When calculating stopping distance, numerical integration in the baseline enforcement algorithms discretizes train speed and position to calculate forces, which overestimates resistance while simultaneously underestimating available brake force. Acceleration/deceleration due to slope is even more subtle as it depends on the position of the train along the slope (e.g., on a crest changing from uphill to downhill, deceleration on the uphill segment is overestimated until the train passes the top, afterwards acceleration is underestimated). These effects do not balance out and thus make numerical integration errors unreliable and hard to predict. Moreover, changing the integration step size shifts how distance estimates are biased towards undershoot or overshoot (e.g., in typical configurations, brake ramp-up is the dominating influence on stopping distance, and so larger integration step sizes bias towards undershoot). As a result, for any given configuration of numerical integration in enforcement algorithms, scenarios can be constructed where the numerical integration underestimates stopping distance and train enforcement exhibits unsafe behavior. The formal models and proofs presented herein design provably correct stopping distance over-approximations instead of using numerical integration and are, therefore, not subject to these intricate safety tradeoffs.

[0117] Stopping Behavior in Troughs - The first validation in FIGS. 7-9 shows a train configuration of a medium (75 cars), loaded (car weight 286klbf), mixed freight train traveling at an initial speed of 60mph in a trough, with train starting position at Oft. The trough is configured with uniform rate of change from 0.5% downhill to - 0.5% uphill between positions Oft and 7000ft. Locomotive tractive effort and locomotive braking compensates for speed loss and gain due to gradient. Air brakes engage only for the full braking maneuver when attempting to not exceed the movement authority. The monitors and controllers are configured to match the trough maximum u phil l/down h i 11 gradient of 0.5% for slope estimation. A sweep of movement authority endpoints in the range 4000ft-8000ft with 10ft steps identifies challenging configurations. The base enforcement algorithm underestimates stopping distance for 19 (of the 400) endpoints.

[0118] The base enforcement algorithm in FIG. 7 uses numeric integration to determine the stopping distance and adds a generous constant safety factor plus speeddependent safety offset resulting in the train initiating braking at 3609ft. The maneuver finishes at 5889ft, stopping 2021ft short of the end of movement authority. In FIG. 8, the verified controller does not use any such offsets. It initiates braking much later at position 5368ft and stops at 7578ft, which is significantly closer to the movement authority endpoint, limiting undershoot to 332ft. The results shown in FIG. 8 removes the safety offset from the base enforcement algorithm in an experiment illustrating the subtle interplay between forces and their safety consequences. Even though the uphill segment of the trough helps reduce stopping distance, numeric integration overestimates this effect and initiates braking too late, which the monitor detects at 5368ft. Should the train ignore the warning, it overshoots by 9ft (highlighted in red) with a remaining speed of 7.8 fps when passing the desired stopping point. Initiating fallback at the monitor violation would have kept the train from overshooting the movement authority. FIG. 9 shows that the verified controller (Model 5) limits the undershoot to 332ft.

[0119] Stopping Behavior on Crests - An assumption in the brake enforcement algorithms and thus an initial condition in the proof is that train locomotives are not underpowered: their tractive effort is enough to overcome maximum uphill slope and stay stopped on the maximum downhill slope. FIG. 10 illustrates how an underpowered, initially stopped train starts rolling downhill until the air brakes build enough deceleration to stop the train. This configuration, violating initial conditions, is unsafe to start in the first place.

[0120] Underpowered locomotives are especially challenging on a crest where (full) tractive effort is needed to limit the speed loss on the uphill slope and regain desired speed on the downhill segment, but air brakes are needed to stay stopped. FIGS. 11-14 compares the behavior of the base enforcement algorithms and the verified algorithm with underpowered locomotives on a crest with movement authority endpoint at 7920ft. In this experiment, the monitors and controllers are configured for a maximum up hil l/down hi II gradient of 3% for slope estimation.

[0121] Numeric integration underestimates stopping distance in several configurations, whereas our verified controller correctly identifies the need to engage air brakes in time while simultaneously avoiding the inefficiencies of fudge factors. FIG. 11 shows the base enforcement algorithm results in a 1538ft undershoot. FIG. 12 shows that the base enforcement algorithm with offset overshoots by 14 ft. The Light-gray dotted lines mark other movement authority endpoints in the range 4000ft-8000ft that the algorithm would also overshoot. FIG. 13 shows that the verified controller (Model 5) limits the undershoot to 528ft.

[0122] Verified train controllers that account for the FRA model were formally verified with all its competing influences of track grade, curve resistance, air brakes and

Davis resistance. Techniques that generalize to resolve challenges in safety critical embedded software design improved controller efficiency. Validation in simulation shows significant improvement in undershoot over conservative controllers that use safety offsets, and improved safety compared to controllers without safety offsets.

[0123] The invention has been described in the context of specific embodiments, which are intended only as exemplars of the invention. As would be realized, many variations of the described embodiments are possible. For example, variations in the design, shape, size, location, function and operation of various components, including both software and hardware components, would still be considered to be within the scope of the invention, which is defined by the following claims.