Engineering topics

Mehlitz, Peter

Publications and source records attributed to Mehlitz, Peter.

5 records

NASA NTRS2020

Actor-based Runtime Verification with MESA

This work presents a runtime verification approach implemented in the tool MESA (MEssage-based System Analysis) which allows for using concurrent monitors to check for properties specified in data parameterized temporal logic and state machines. The tool is implemented as an internal Scala DSL. We employ the actor programming model to implement MESA where monitors are captured by concurrent actors that communicate via messaging. The paper presents a case study in which MESA is used to effectively monitor a large number of flights from live US airspace data streams. We also perform an empirical study by conducting experiments using monitoring systems with different num- bers of concurrent monitors and different layers of indexing on the data contained in events. The paper describes the experiments, evaluates the results, and discusses challenges faced during the study. The evaluation shows the value of combining concurrency with indexing to handle data rich events.

Mehlitz, Peter↗

NASA NTRS2017

MESA: Message-Based System Analysis Using Runtime Verification

In this paper, we present a novel approach and framework for run-time verication of large, safety critical messaging systems. This work was motivated by verifying the System Wide Information Management (SWIM) project of the Federal Aviation Administration (FAA). SWIM provides live air traffic, site and weather data streams for the whole National Airspace System (NAS), which can easily amount to several hundred messages per second. Such safety critical systems cannot be instrumented, therefore, verification and monitoring has to happen using a nonintrusive approach, by connecting to a variety of network interfaces. Due to a large number of potential properties to check, the verification framework needs to support efficient formulation of properties with a suitable Domain Specific Language (DSL). Our approach is to utilize a distributed system that is geared towards connectivity and scalability and interface it at the message queue level to a powerful verification engine. We implemented our approach in the tool called MESA: Message-Based System Analysis, which leverages the open source projects RACE (Runtime for Airspace Concept Evaluation) and TraceContract. RACE is a platform for instantiating and running highly concurrent and distributed systems and enables connectivity to SWIM and scalability. TraceContract is a runtime verication tool that allows for checking traces against properties specified in a powerful DSL. We applied our approach to verify a SWIM service against several requirements.We found errors such as duplicate and out-of-order messages.

Message-based System↗

NASA NTRS2016

RACE: Building Airspace Simulations Faster and Better with Actors

Large, distributed aerospace simulations traditionally have been the domain of customized, closed designs, using statically compiled code based on specialized messaging systems such as DDS and HLA. While this can be suitable for one-off systems or specialized in-house product lines, it increases development costs and lowers extensibility. We propose to use contemporary internet software technology to solve this problem.Our Runtime for Airspace Concept Evaluation (RACE) architecture was born out of the need to rapidly develop and evaluate what-if scenarios that involve the whole National Airspace System (NAS), live NAS data feeds such as the FAA's System Wide Information Management (SWIM) servers, and existing flight simulators. It had to run on off-the-shelf hardware, be open sourced, and support visualization components up to multiple synchronized large screen geo viewers used in situation rooms. Most of all, it had to be extensible - being a viable platform for the development of future simulation components.

Mehlitz, Peter↗

NASA NTRS2005

Seeing the Invisible: Embedding Tests in Code That Cannot be Modified

The difficulty of characterizing and observing valid software behavior during testing can be very difficult in flight systems. To address this issue, we evaluated several approaches to increasing test observability on the Shuttle Abort Flight Management (SAFM) system. To increase test observability, we added probes into the running system to evaluate the internal state and analyze test data. To minimize the impact of the instrumentation and reduce manual effort, we used Aspect-Oriented Programming (AOP) tools to instrument the source code. We developed and elicited a spectrum of properties, from generic to application specific properties, to be monitored via the instrumentation. To evaluate additional approaches, SAFM was ported to Linux, enabling the use of gcov for measuring test coverage, Valgrind for looking for memory usage errors, and libraries for finding non-normal floating point values. An in-house C++ source code scanning tool was also used to identify violations of SAFM coding standards, and other potentially problematic C++ constructs. Using these approaches with the existing test data sets, we were able to verify several important properties, confirm several problems and identify some previously unidentified issues.

O'Malley, Owen↗

NASA NTRS2003

Propel: Tools and Methods for Practical Source Code Model Checking

The work reported here is an overview and snapshot of a project to develop practical model checking tools for in-the-loop verification of NASA s mission-critical, multithreaded programs in Java and C++. Our strategy is to develop and evaluate both a design concept that enables the application of model checking technology to C++ and Java, and a model checking toolset for C++ and Java. The design concept and the associated model checking toolset is called Propel. It builds upon the Java PathFinder (JPF) tool, an explicit state model checker for Java applications developed by the Automated Software Engineering group at NASA Ames Research Center. The design concept that we are developing is Design for Verification (D4V). This is an adaption of existing best design practices that has the desired side-effect of enhancing verifiability by improving modularity and decreasing accidental complexity. D4V, we believe, enhances the applicability of a variety of V&V approaches; we are developing the concept in the context of model checking. The model checking toolset, Propel, is based on extending JPF to handle C++. Our principal tasks in developing the toolset are to build a translator from C++ to Java, productize JPF, and evaluate the toolset in the context of D4V. Through all these tasks we are testing Propel capabilities on customer applications.

Mansouri-Samani, Massoud↗