-
Monitoring Unmanned Aircraft: Specification, Integration, and Lessons-learned
Authors:
Jan Baumeister,
Bernd Finkbeiner,
Florian Kohn,
Florian Löhr,
Guido Manfredi,
Sebastian Schirmer,
Christoph Torens
Abstract:
This paper reports on the integration of runtime monitoring into fully-electric aircraft designed by Volocopter, a German aircraft manufacturer of electric multi-rotor helicopters. The runtime monitor recognizes hazardous situations and system faults. Since the correct operation of the monitor is critical for the safety of the aircraft, the development of the monitor must follow strict aeronautica…
▽ More
This paper reports on the integration of runtime monitoring into fully-electric aircraft designed by Volocopter, a German aircraft manufacturer of electric multi-rotor helicopters. The runtime monitor recognizes hazardous situations and system faults. Since the correct operation of the monitor is critical for the safety of the aircraft, the development of the monitor must follow strict aeronautical standards. This includes the integration of the monitor into different development environments, such as log-file analysis, hardware/software-in-the-loop testing, and test flights. We have used the stream-based monitoring framework RTLola to generate monitors for a range of requirements. In this paper, we present representative monitoring specifications and our lessons learned from integrating the generated monitors. Our main finding is that the specification and the integration need to be decoupled, because the specification remains stable throughout the development process, whereas the different development stages require a separate integration of the monitor into each environment. We achieve this decoupling with a novel abstraction layer in the monitoring framework that adapts the monitor to each environment without affecting the core component generated from the specification. The decoupling of the integration has also allowed us to react quickly to the frequent changes in the hardware and software environment of the monitor due to the fast-paced development of the aircraft in a startup company.
△ Less
Submitted 18 April, 2024;
originally announced April 2024.
-
Real-time Visualization of Stream-based Monitoring Data
Authors:
Jan Baumeister,
Bernd Finkbeiner,
Stefan Gumhold,
Malte Schledjewski
Abstract:
Stream-based runtime monitors are used in safety-critical applications such as Unmanned Aerial Systems (UAS) to compute comprehensive statistics and logical assessments of system health that provide the human operator with critical information in hand-over situations. In such applications, a visual display of the monitoring data can be much more helpful than the textual alerts provided by a more t…
▽ More
Stream-based runtime monitors are used in safety-critical applications such as Unmanned Aerial Systems (UAS) to compute comprehensive statistics and logical assessments of system health that provide the human operator with critical information in hand-over situations. In such applications, a visual display of the monitoring data can be much more helpful than the textual alerts provided by a more traditional user interface. This visualization requires extensive real-time data processing, which includes the synchronization of data from different streams, filtering and aggregation, and priorization and management of user attention. We present a visualization approach for the \rtlola monitoring framework. Our approach is based on the principle that the necessary data processing is the responsibility of the monitor itself, rather than the responsibility of some external visualization tool. We show how the various aspects of the data transformation can be described as RTLola stream equations and linked to the visualization component through a bidirectional synchronous interface. In our experience, this approach leads to highly informative visualizations as well as to understandable and easily maintainable monitoring code.
△ Less
Submitted 25 May, 2022;
originally announced May 2022.
-
A Temporal Logic for Asynchronous Hyperproperties
Authors:
Jan Baumeister,
Norine Coenen,
Borzoo Bonakdarpour,
Bernd Finkbeiner,
Cesar Sanchez
Abstract:
Hyperproperties are properties of computational systems that require more than one trace to evaluate, e.g., many information-flow security and concurrency requirements. Where a trace property defines a set of traces, a hyperproperty defines a set of sets of traces. The temporal logics HyperLTL and HyperCTL* have been proposed to express hyperproperties. However, their semantics are synchronous in…
▽ More
Hyperproperties are properties of computational systems that require more than one trace to evaluate, e.g., many information-flow security and concurrency requirements. Where a trace property defines a set of traces, a hyperproperty defines a set of sets of traces. The temporal logics HyperLTL and HyperCTL* have been proposed to express hyperproperties. However, their semantics are synchronous in the sense that all traces proceed at the same speed and are evaluated at the same position. This precludes the use of these logics to analyze systems whose traces can proceed at different speeds and allow that different traces take stuttering steps independently. To solve this problem in this paper, we propose an asynchronous variant of HyperLTL. On the negative side, we show that the model-checking problem for this variant is undecidable. On the positive side, we identify a decidable fragment which covers a rich set of formulas with practical applications. We also propose two model-checking algorithms that reduce our problem to the HyperLTL model-checking problem in the synchronous semantics.
△ Less
Submitted 28 April, 2021;
originally announced April 2021.
-
On the value function for nonautonomous optimal control problems with infinite horizon
Authors:
J. Baumeister,
A. Leitao,
G. N. Silva
Abstract:
In this paper we consider nonautonomous optimal control problems of infinite horizon type, whose control actions are given by $L^1$-functions. We verify that the value function is locally Lipschitz. The equivalence between dynamic programming inequalities and Hamilton-Jacobi-Bellman (HJB) inequalities for proximal sub (super) gradients is proven. Using this result we show that the value function i…
▽ More
In this paper we consider nonautonomous optimal control problems of infinite horizon type, whose control actions are given by $L^1$-functions. We verify that the value function is locally Lipschitz. The equivalence between dynamic programming inequalities and Hamilton-Jacobi-Bellman (HJB) inequalities for proximal sub (super) gradients is proven. Using this result we show that the value function is a Dini solution of the HJB equation. We obtain a verification result for the class of Dini sub-solutions of the HJB equation and also prove a minimax property of the value function with respect to the sets of Dini semi-solutions of the HJB equation. We introduce the concept of viscosity solutions of the HJB equation in infinite horizon and prove the equivalence between this and the concept of Dini solutions. In the appendix we provide an existence theorem.
△ Less
Submitted 22 January, 2021;
originally announced January 2021.
-
Modified iterated Tikhonov methods for solving systems of nonlinear ill-posed equations
Authors:
J. Baumeister,
A. De Cezaro,
A. Leitao
Abstract:
We investigate iterated Tikhonov methods coupled with a Kaczmarz strategy for obtaining stable solutions of nonlinear systems of ill-posed operator equations. We show that the proposed method is a convergent regularization method. In the case of noisy data we propose a modification, the so called lo** iterated Tikhonov-Kaczmarz method, where a sequence of relaxation parameters is introduced and…
▽ More
We investigate iterated Tikhonov methods coupled with a Kaczmarz strategy for obtaining stable solutions of nonlinear systems of ill-posed operator equations. We show that the proposed method is a convergent regularization method. In the case of noisy data we propose a modification, the so called lo** iterated Tikhonov-Kaczmarz method, where a sequence of relaxation parameters is introduced and a different stop** rule is used. Convergence analysis for this method is also provided.
△ Less
Submitted 22 December, 2020;
originally announced December 2020.
-
Optimal exploitation of renewable resource stocks: Necessary conditions
Authors:
J. Baumeister,
A. Leitao
Abstract:
We study a model for the exploitation of renewable stocks developed in Clark et al. (Econometrica 47 (1979), 25-47). In this particular control problem, the control law contains a measurable and an impulsive control component. We formulate Pontryagin's maximum principle for this kind of control problems, proving first order necessary conditions of optimality. Manipulating the correspondent Lagrang…
▽ More
We study a model for the exploitation of renewable stocks developed in Clark et al. (Econometrica 47 (1979), 25-47). In this particular control problem, the control law contains a measurable and an impulsive control component. We formulate Pontryagin's maximum principle for this kind of control problems, proving first order necessary conditions of optimality. Manipulating the correspondent Lagrange multipliers we are able to define two special switch functions, that allow us to describe the optimal trajectories and control policies nearly completely for all possible initial conditions in the phase plane.
△ Less
Submitted 30 November, 2020;
originally announced December 2020.
-
On iterative methods for solving ill-posed problems modeled by PDE's
Authors:
J. Baumeister,
A. Leitao
Abstract:
We investigate the iterative methods proposed by Maz'ya and Kozlov (see [KM1], [KM2]) for solving ill-posed inverse problems modeled by partial differential equations. We consider linear evolutionary problems of elliptic, hyperbolic and parabolic types. Each iteration of the analyzed methods consists in the solution of a well posed problem (boundary value problem or initial value problem respectiv…
▽ More
We investigate the iterative methods proposed by Maz'ya and Kozlov (see [KM1], [KM2]) for solving ill-posed inverse problems modeled by partial differential equations. We consider linear evolutionary problems of elliptic, hyperbolic and parabolic types. Each iteration of the analyzed methods consists in the solution of a well posed problem (boundary value problem or initial value problem respectively). The iterations are described as powers of affine operators, as in [KM2]. We give alternative convergence proofs for the algorithms by using spectral theory and the fact that the linear parts of these affine operators are non-expansive with additional functional analytical properties (see [Le1,2]). Also problems with noisy data are considered and estimates for the convergence rate are obtained under a priori regularity assumptions on the problem data.
△ Less
Submitted 29 November, 2020;
originally announced November 2020.
-
Automatic Optimizations for Stream-based Monitoring Languages
Authors:
Jan Baumeister,
Bernd Finkbeiner,
Matthis Kruse,
Maximilian Schwenger
Abstract:
Runtime monitors that are specified in a stream-based monitoring language tend to be easier to understand, maintain, and reuse than those written in a standard programming language. Because of their formal semantics, such specification languages are also a natural choice for safety-critical applications. Unlike for standard programming languages, there is, however, so far very little support for a…
▽ More
Runtime monitors that are specified in a stream-based monitoring language tend to be easier to understand, maintain, and reuse than those written in a standard programming language. Because of their formal semantics, such specification languages are also a natural choice for safety-critical applications. Unlike for standard programming languages, there is, however, so far very little support for automatic code optimization. In this paper, we present the first collection of code transformations for the stream-based monitoring language RTLola. We show that classic compiler optimizations, such as Sparse Conditional Constant Propagation and Common Subexpression Elimination, can be adapted to monitoring specifications. We also develop new transformations -- Pacing Type Refinement and Filter Refinement -- which exploit the specific modular structure of RTLola as well as the implementation freedom afforded by a declarative specification language. We demonstrate the significant impact of the code transformations on benchmarks from the monitoring of unmanned aircraft systems (UAS).
△ Less
Submitted 26 November, 2020;
originally announced November 2020.
-
On Levenberg-Marquardt-Kaczmarz iterative methods for solving systems of nonlinear ill-posed equations
Authors:
J. Baumeister,
B. Kaltenbacher,
A. Leitao
Abstract:
In this article a modified Levenberg-Marquardt method coupled with a Kaczmarz strategy for obtaining stable solutions of nonlinear systems of ill-posed operator equations is investigated. We show that the proposed method is a convergent regularization method. Numerical tests are presented for a non-linear inverse do** problem based on a bipolar model.
In this article a modified Levenberg-Marquardt method coupled with a Kaczmarz strategy for obtaining stable solutions of nonlinear systems of ill-posed operator equations is investigated. We show that the proposed method is a convergent regularization method. Numerical tests are presented for a non-linear inverse do** problem based on a bipolar model.
△ Less
Submitted 18 November, 2020;
originally announced November 2020.
-
Layered Drawing of Undirected Graphs with Generalized Port Constraints
Authors:
Johannes Zink,
Julian Walter,
Joachim Baumeister,
Alexander Wolff
Abstract:
The aim of this research is a practical method to draw cable plans of complex machines. Such plans consist of electronic components and cables connecting specific ports of the components. Since the machines are configured for each client individually, cable plans need to be drawn automatically. The drawings must be well readable so that technicians can use them to debug the machines. In order to m…
▽ More
The aim of this research is a practical method to draw cable plans of complex machines. Such plans consist of electronic components and cables connecting specific ports of the components. Since the machines are configured for each client individually, cable plans need to be drawn automatically. The drawings must be well readable so that technicians can use them to debug the machines. In order to model plug sockets, we introduce port groups; within a group, ports can change their position (which we use to improve the aesthetics of the layout), but together the ports of a group must form a contiguous block.
We approach the problem of drawing such cable plans by extending the well-known Sugiyama framework such that it incorporates ports and port groups. Since the framework assumes directed graphs, we propose several ways to orient the edges of the given undirected graph. We compare these methods experimentally, both on real-world data and synthetic data that carefully simulates real-world data. We measure the aesthetics of the resulting drawings by counting bends and crossings. Using these metrics, we experimentally compare our approach to Kieler [JVLC 2014], a library for drawing graphs in the presence of port constraints. Our method produced 10--30 % fewer crossings, while it performed equally well or slightly worse than Kieler with respect to the number of bends and the time used to compute a drawing.
△ Less
Submitted 25 April, 2023; v1 submitted 24 August, 2020;
originally announced August 2020.
-
RTLola Cleared for Take-Off: Monitoring Autonomous Aircraft
Authors:
Jan Baumeister,
Bernd Finkbeiner,
Sebastian Schirmer,
Maximilian Schwenger,
Christoph Torens
Abstract:
The autonomous control of unmanned aircraft is a highly safety-critical domain with great economic potential in a wide range of application areas, including logistics, agriculture, civil engineering, and disaster recovery. We report on the development of a dynamic monitoring framework for the DLR ARTIS (Autonomous Rotorcraft Testbed for Intelligent Systems) family of unmanned aircraft based on the…
▽ More
The autonomous control of unmanned aircraft is a highly safety-critical domain with great economic potential in a wide range of application areas, including logistics, agriculture, civil engineering, and disaster recovery. We report on the development of a dynamic monitoring framework for the DLR ARTIS (Autonomous Rotorcraft Testbed for Intelligent Systems) family of unmanned aircraft based on the formal specification language RTLola. RTLola is a stream-based specification language for real-time properties. An RTLola specification of hazardous situations and system failures is statically analyzed in terms of consistency and resource usage and then automatically translated into an FPGA-based monitor. Our approach leads to highly efficient, parallelized monitors with formal guarantees on the noninterference of the monitor with the normal operation of the autonomous system.
△ Less
Submitted 29 July, 2020; v1 submitted 27 March, 2020;
originally announced April 2020.
-
FPGA Stream-Monitoring of Real-time Properties
Authors:
Jan Baumeister,
Bernd Finkbeiner,
Maximilian Schwenger,
Hazem Torfah
Abstract:
An essential part of cyber-physical systems is the online evaluation of real-time data streams. Especially in systems that are intrinsically safety-critical, a dedicated monitoring component inspecting data streams to detect problems at runtime greatly increases the confidence in a safe execution. Such a monitor needs to be based on a specification language capable of expressing complex, high-leve…
▽ More
An essential part of cyber-physical systems is the online evaluation of real-time data streams. Especially in systems that are intrinsically safety-critical, a dedicated monitoring component inspecting data streams to detect problems at runtime greatly increases the confidence in a safe execution. Such a monitor needs to be based on a specification language capable of expressing complex, high-level properties using only the accessible low-level signals. Moreover, tight constraints on computational resources exacerbate the requirements on the monitor. Thus, several existing approaches to monitoring are not applicable due to their dependence on an operating system. We present an FPGA-based monitoring approach by compiling an RTLola specification into synthesizable VHDL code. RTLola is a stream-based specification language capable of expressing complex real-time properties while providing an upper bound on the execution time and memory requirements. The statically determined memory bound allows for a compilation to an FPGA with a fixed size. An advantage of FPGAs is a simple integration process in existing systems and superb executing time. The compilation results in a highly parallel implementation thanks to the modular nature of RTLola specifications. This further increases the maximal event rate the monitor can handle.
△ Less
Submitted 18 March, 2020;
originally announced March 2020.
