Conventional diagnostic systems often fail to account for temporal dynamics - such as duration, frequency, or sequence of events - which are critical for accurate fault assessment. Existing solutions that model time, like Dynamic Bayesian Networks (DBNs), typically suffer from computational complexity and scalability issues. This paper introduces a hybrid diagnostic architecture that integrates a standard Bayesian Networks (BNs) with a powerful temporal reasoner R2U2 (Realizable Responsive Unobtrusive Unit). By decoupling temporal logic from probabilistic inference, our approach allows the specialized R2U2 engine to efficiently process complex time-dependent conditions and provide nuanced inputs to the BNs. The result is a more scalable, flexible, and robust framework for diagnosing failures in systems where temporal behavior is a key factor. The paper will detail this architecture, its generation from system models, and demonstrate its capabilities using a UAV electric powertrain example.

Cyberphysical systems with autonomous functions are complex pieces of software, consisting of many components, some of which implement autonomous functionality and some may use AI or machine learning algorithms. Software bugs in an autonomous system are of particular concern, as they can have catastrophic consequences. However, detailed studies based on empirical data are rare and therefore these bugs are not well understood. This paper aims to contribute towards filling that gap by investigating the software changes and bugs in Autonomy Operating System (AOS) for Unmanned Aircraft Systems (UAS), which consist of 26 components containing about 103,000 lines of code and having a total of 772 bugfixes. Based on the data extracted from the code repository and semi-structured interviews with the developers of AOS, we explore the differences among autonomous software components, components developed using Model-based Software Engineering, and reuse with respect to change proneness, fault proneness, distribution of bugfixes among AOS components and files of these components, and characteristics of bugs of different AOS components. Our results show that the autonomous components were significantly more change prone (measured in number of commits and code churn) and fault prone (measured in bugfixes per KLoC) than non-autonomous components. The distribution of the locations of bugfixes was skewed, both at component and file level (i.e., a small number of components / files contained the majority of bugs). These evidence-based findings provide important insights to researchers and practitioners alike and can be used to efficiently improve the quality and reliability of autonomous systems.

Abstract Requirements formalization has become increasingly popular in industrial settings as an effort to disambiguate designs and optimize development time and costs for critical system components. Formal requirements elicitation also enables the employment of analysis tools to prove important properties, such as consistency and realizability. In this paper, we present the realizability analysis framework that we developed as part of the Formal Requirements Elicitation Tool (FRET). Our framework prioritizes usability, and employs state-of-the-art analysis algorithms that support infinite theories. We demonstrate the workflow for realizability checking, showcase the diagnosis process that supports visualization of conflicts between requirements and simulation of counterexamples, and discuss results from industrial-level case studies.

Deep Neural Networks (DNNs) have gained tremendous popularity in many application areas over the recent years. Safety-critical applications as found in the aerospace domain require that the behavior of the DNN is validated and tested rigorously for system safety.In this paper, we present a framework to support testing of DNNs. Our framework employs techniques from statistical modeling and active learning to effectively generate test cases for DNNs used in Aerospace systems and also supports a comparison between different DNNs. In this paper, we will describe our statistical framework, the algorithms for model construction and the metric guiding the test case generation process.We will present a case study on a physics-based Deep recurrent residual neural network (DR-RNN), which has been trained to emulate the aerodynamics behavior of a Boeing 747-100 aircraft.

Capturing and analyzing requirements of Cyber-Physical Systems (CPS) can be challenging, since CPS models typically involve time-varying and real-valued variables, physical system dynamics, or even adaptive behavior. MATLAB/Simulink is a development and simulation framework that is widely used in industry to capture such systems. In this paper, we report on the application of NASA Ames tools to perform end-to-end analysis of the Ten Lockheed Martin Challenge Problems (LMCPS). LMCPS is a set of industrial Simulink model benchmarks and natural language requirements developed by domain experts. Our framework, which integrates the tools FRET and COCOSIM, is used to: 1) elicit, explain, and formalize the semantics of the given natural language requirements; 2) generate verification code and monitors that can be automatically attached to the Simulink models; 3) perform verification by using SMT-based model checkers. FRET and COCOS1M are open source, and can be used by other researchers and practitioners to replicate our case study. We provide a categorization of recurring patterns in the formalization of the requirements and discuss the strengths and weaknesses of our automated verification approach.

We present R2U2, a novel framework for runtime monitoring of security properties and diagnosing of security threats on-board Unmanned Aerial Systems (UAS). R2U2, implemented in FPGA hardware, is a real-time, Realizable, Responsive, Unobtrusive Unit for runtime system analysis, now including security threat detection. R2U2 is designed to continuously monitor inputs from on-board components such as the GPS, the ground control station, other sensor readings, actuator outputs, and flight software status. By simultaneously monitoring and performing statistical reasoning, attack patterns and post-attack discrepancies in the UAS behavior can be detected. R2U2 uses runtime observer pairs for Linear and Metric Temporal Logics for property monitoring and Bayesian networks for diagnosis of system health during runtime. We discuss the design and implementation that now enables R2U2 to handle security threats and present simulation results of several attack scenarios on the NASA DragonEye UAS.

The analysis of large and complex parameterized software systems, e.g., systems simulation in aerospace, is very complicated and time-consuming due to the large parameter space, and the complex, highly coupled nonlinear nature of the different system components. Thus, such systems are generally validated only in regions local to anticipated operating points rather than through characterization of the entire feasible operational envelope of the system. We have addressed the factors deterring such an analysis with a tool to support envelope assessment: we utilize a combination of advanced Monte Carlo generation with n-factor combinatorial parameter variations to limit the number of cases, but still explore important interactions in the parameter space in a systematic fashion. Additional test-cases, automatically generated from models (e.g., UML, Simulink, Stateflow) improve the coverage. The distributed test runs of the software system produce vast amounts of data, making manual analysis impossible. Our tool automatically analyzes the generated data through a combination of unsupervised Bayesian clustering techniques (AutoBayes) and supervised learning of critical parameter ranges using the treatment learner TAR3. The tool has been developed around the Trick simulation environment, which is widely used within NASA. We will present this tool with a GN&C (Guidance, Navigation and Control) simulation of a small satellite system.

This paper presents a new methodology for automatic knowledge driven data mining based on the theory of Mercer Kernels, which are highly nonlinear symmetric positive definite mappings from the original image space to a very high, possibly infinite dimensional feature space. We describe a new method called Mixture Density Mercer Kernels (MDMK) to learn kernel function directly from data, rather than using pre-defined kernels. These data adaptive kernels can encode prior knowledge in the kernel using a Bayesian formulation, thus allowing for physical information to be encoded in the model. Specifically, we demonstrate the use of the algorithm in situations with extremely small samples of data. We compare the results with existing algorithms on data from the Sloan Digital Sky Survey (SDSS) and demonstrate the method's superior performance against standard methods. The results show that the Mixture Density Mercer Kernel described here outperforms tree-based classification in distinguishing high-redshift galaxies from low-redshift galaxies by approximately 16% on test data, bagged trees by approximately 7%, and bagged trees built on a much larger sample of data by approximately 2%. The code for these experiments has been generated with the AutoBayes tool, which automatically generates efficient and documented C/C++ code from abstract statistical model specifications. The core of the system is a schema library which contains templates for learning and knowledge discovery algorithms like different versions of EM, or numeric optimization methods like conjugate gradient methods. The template instantiation is supported by symbolic-algebraic computations, which allows AutoBayes to find closed-form solutions and, where possible, to integrate them into the code.

autofilter is a tool that generates implementations that solve state estimation problems using Kalman filters. From a high-level, mathematics-based description of a state estimation problem, autofilter automatically generates code that computes a statistically optimal estimate using one or more of a number of well-known variants of the Kalman filter algorithm. The problem description may be given in terms of continuous or discrete, linear or nonlinear process and measurement dynamics. From this description, autofilter automates many common solution methods (e.g., linearization, discretization) and generates C or Matlab code fully automatically. autofilter surpasses toolkit-based programming approaches for Kalman filters because it requires no low-level programming skills (e.g., to "glue" together library function calls). autofilter raises the level of discourse to the mathematics of the problem at hand rather than the details of what algorithms, data structures, optimizations and so on are required to implement it. An overview of autofilter is given along with an example of its practical application to deep space attitude estimation.

Neuromodulatory receptors in presynaptic position have the ability to suppress synaptic transmission for seconds to minutes when fully engaged. This effectively alters the synaptic strength of a connection. Much work on neuromodulation has rested on the assumption that these effects are uniform at every neuron. However, there is considerable evidence to suggest that presynaptic regulation may be in effect synapse-specific. This would define a second "weight modulation" matrix, which reflects presynaptic receptor efficacy at a given site. Here we explore functional consequences of this hypothesis. By analyzing and comparing the weight matrices of networks trained on different aspects of a task, we identify the potential for a low complexity "modulation matrix", which allows switching between differently trained subtasks while retraining general performance characteristics for the task. This means that a given network can adapt itself to different task demands be regulating its release of neuromodulators. Specifically, we suggest that (a) a network can provide optimized responses for related classification tasks without the need to train entirely separate networks and (b) a network can blend a "memory mode" which aims at reproducing memorized patterns and a "novelty mode" which aims to facilitate classification of new patterns. We relate this work to the known effects of neuromodulators on brain-state dependent processing.

We take a typical scientific data analysis task, the analysis of planetary nebulae images taken by the Hubble Space Telescope, and describe how program synthesis can be used to generate the necessary analysis programs from high-level models. We describe the AutoBayes synthesis system, discuss its fully declarative specification language, and present the automatic program derivation starting with the scientists' original analysis.

Data analysis is an important scientific task which is required whenever information needs to be extracted from raw data. Statistical approaches to data analysis, which use methods from probability theory and numerical analysis, are well-founded but difficult to implement: the development of a statistical data analysis program for any given application is time-consuming and requires substantial knowledge and experience in several areas. In this paper, we describe A UTO B AYES , a program synthesis system for the generation of data analysis programs from statistical models. A statistical model specifies the properties for each problem variable (i.e. observation or parameter) and its dependencies in the form of a probability distribution. It is a fully declarative problem description, similar in spirit to a set of differential equations. From such a model, A UTO B AYES generates optimized and fully commented C/C++ code which can be linked dynamically into the Matlab and Octave environments. Code is produced by a schema-guided deductive synthesis process. A schema consists of a code template and applicability constraints which are checked against the model during synthesis using theorem proving technology. A UTO B AYES augments schema-guided synthesis by symbolic-algebraic computation and can thus derive closed form solutions for many problems. It is well-suited for tasks like estimating best-fitting model parameters for the given data. Here, we describe A UTO B AYES 's system architecture, in particular the schema-guided synthesis kernel. Its capabilities are illustrated by a number of advanced textbook examples and benchmarks.

Machine learning has reached a point where many probabilistic meth- ods can be understood as variations, extensions and combinations of a much smaller set of abstract themes, e.g., as different instances of the EM algorithm. This enables the systematic derivation of algorithms cus- tomized for different models. Here, we describe the AUTO BAYES sys- tem which takes a high-level statistical model specification, uses power- ful symbolic techniques based on schema-based program synthesis and computer algebra to derive an efficient specialized algorithm for learning that model, and generates executable code implementing that algorithm. This capability is far beyond that of code collections such as Matlab tool- boxes or even tools for model-independent optimization such as BUGS for Gibbs sampling: complex new algorithms can be generated with- out new programming, algorithms can be highly specialized and tightly crafted for the exact structure of the model and data, and efficient and commented code can be generated for different languages or systems. We present automatically-derived algorithms ranging from closed-form solutions of Bayesian textbook problems to recently-proposed EM algo- rithms for clustering, regression, and a multinomial form of PCA. 1 Automatic Derivation of Statistical Algorithms Overview. We describe a symbolic program synthesis system which works as a “statistical algorithm compiler:” it compiles a statistical model specification into a custom algorithm design and from that further down into a working program implementing the algorithm design. This system, AUTOBAYES, can be loosely thought of as “part theorem prover, part Mathematica, part learning textbook, and part Numerical Recipes.” It provides much more flexibility than a fixed code repository such as a Matlab toolbox, and allows the creation of efficient algorithms which have never before been implemented, or even written down. AUTOBAYES is intended to automate the more routine application of complex methods in novel contexts. For example, recent multinomial extensions to PCA [2, 4] can be derived in this way.
The algorithm design problem. Given a dataset and a task, creating a learning method can be characterized by two main questions: 1. What is the model? 2. What algorithm will optimize the model parameters? The statistical algorithm (i.e., a parameter optimization algorithm for the statistical model) can then be implemented manually. The system in this paper answers the algorithm question given that the user has chosen a model for the data,and continues through to implementation. Performing this task at the state-of-the-art level requires an intertwined meld of probability theory, computational mathematics, and software engineering. However, a number of factors unite to allow us to solve the algorithm design problem computationally: 1. The existence of fundamental building blocks (e.g., standardized probability distributions, standard optimization procedures, and generic data structures). 2. The existence of common representations (i.e., graphical models [3, 13] and program schemas). 3. The formalization of schema applicability constraints as guards.1 The challenges of algorithm design. The design problem has an inherently combinatorial nature, since subparts of a function may be optimized recursively and in different ways. It also involves the use of new data structures or approximations to gain performance. As the research in statistical algorithms advances, its creative focus should move beyond the ultimately mechanical aspects and towards extending the abstract applicability of already existing schemas (algorithmic principles like EM), improving schemas in ways that gener- alize across anything they can be applied to, and inventing radically new schemas. 2 Combining Schema-based Synthesis and Bayesian Networks with 0 < n_points; 1 model mog as ’Mixture of Gaussians’; with 0 < nclasses with nclasses << n_points; with 1 = sum(I := 1..n_classes, phi(I)); 7 double phi(1..nclasses) as ’weights’ 8 9 double mu(1..nclasses); 9 double sigma(1..n_classes); 2 const int npoints as ’nr. of data points’ 3 4 const int nclasses := 3 as ’nr. classes’ 5 6 Statistical Models. Externally, AUTOBAYES has the look and feel of a compiler. Users specify their model of interest in a high-level specification language (as opposed to a program- ming language). The figure shows the specification of the mixture of Gaus- sians example used throughout this paper.2 Note the constraint that the sum of the class probabilities must equal one (line 8) along with others (lines 3 and 5) that make optimization of the model well-defined. Also note the ability to specify assumptions of the kind in line 6, which may be used by some algorithms. The last line specifies the goal 10 int c(1..npoints) as ’class labels’; 11 c ˜ disc(vec(I := 1..nclasses, phi(I))); 12 data double x(1..n_points) as ’data’; 13 x(I) ˜ gauss(mu(c(I)), sigma(c(I))); 14 max pr(x| phi,mu,sigma
) wrt phi,mu,sigma
;  inference task: maximize the conditional probability pr rameters 

Previous work on domain-specific deductive program synthesis described the Amphion/NAIF system for generating Fortran code from high-level graphical specifications describing problems in space system geometry. Amphion/NAIF specifications describe input-output functions that compute geometric quantities (e.g., the distance between two planets at a point in time, or the time when a radio communication path between a spacecraft and earth is occluded) by composing together Fortran subroutines from the NAIF subroutine library developed at the Jet Propulsion Laboratory. In essence, Amphion/NAIF synthesizes code for glueing together the NAIF components in a way such that the generated code implements the specification, with a concurrently generated proof that this implementation is correct. Amphion/NAIF demonstrated the success of domain-specific deductive program synthesis and is still in use today within the space science community. However, a number of questions remained open that we will attempt to answer in this paper.

This paper presents an algorithm for automatically generating UML statecharts from a collection of UML sequence diagrams. Computer support for this transition between requirements and design is important for a successful application of UML's highly iterative, distributed software development process. There are three main issues which must be addressed when generating statecharts from sequence diagrams. Firstly, conflicts arising from the merging of independently developed sequence diagrams must be detected and resolved. Secondly, different sequence diagrams often contain identical or similar behaviors. For a true interleaving of the sequence diagrams, these behaviors must be recognized and merged. Finally, generated statecharts usually are only an approximation of the system and thus must be hand-modified and refined by designers. As such, the generated artifact should be highly structured and readable. In terms of statecharts, this corresponds to the introduction of hierarchy. Our algorithm successfully tackles all three of these aspects and will be illustrated in this paper with a well-known ATM example.

Deduction-based software component retrieval uses pre- and postconditions as indexes and search keys and an automated theorem prover (ATP) to check whether a component matches. This idea is very simple but the vast number of arising proof tasks makes a practical implementation very hard. We thus pass the components through a chain of filters of increasing deductive power. In this chain, rejection filters based on signature matching and model checking techniques are used to rule out non-matches as early as possible and to prevent the subsequent ATP from "drowning". Hence, intermediate results of reasonable precision are available at (almost) any time of the retrieval process. The final ATP step then works as a confirmation filter to lift the precision of the answer set. We implemented a chain which runs fully automatically and uses SETHEO for model checking and the automated prover SETHEO as confirmation filter. We evaluated the system over a medium-sized collection of components. The results encourage our approach.

No abstract available.