NASA Logo, External Link
Facebook icon, External Link to NASA STI page on Facebook Twitter icon, External Link to NASA STI on Twitter YouTube icon, External Link to NASA STI Channel on YouTube RSS icon, External Link to New NASA STI RSS Feed AddThis share icon
 

Record Details

Record 1 of 1
MESA: Message-Based System Analysis Using Runtime Verification
NTRS Full-Text: Click to View  [PDF Size: 387 KB]
Author and Affiliation:
Shafiei, Nastaran(SGT, Inc., Moffett Field, CA, United States)
Tkachuk, Oksana(SGT, Inc., Moffett Field, CA, United States)
Mehlitz, Peter(SGT, Inc., Moffett Field, CA, United States)
Abstract: 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.
Publication Date: Sep 13, 2017
Document ID:
20170010673
(Acquired Nov 13, 2017)
Subject Category: COMPUTER PROGRAMMING AND SOFTWARE; AIRCRAFT COMMUNICATIONS AND NAVIGATION
Report/Patent Number: ARC-E-DAA-TN43183
Document Type: Conference Paper
Meeting Information: International Conference on Runtime Verification (RV 2017); 17th ; 13-16 Sep. 2017; Seattle, WA; United States
Meeting Sponsor: Microsoft Corp.; Redmond, WA, United States
Springer-Verlag G.m.b.H. and Co. K.G.; New York, NY, United States
Contract/Grant/Task Num: NNA14AA60C; WBS 00370.03B.105.001
Financial Sponsor: NASA Ames Research Center; Moffett Field, CA, United States
Organization Source: NASA Ames Research Center; Moffett Field, CA, United States
Description: 16p; In English
Distribution Limits: Unclassified; Publicly available; Unlimited
Rights: Copyright; Public use permitted
NASA Terms: MESSAGE PROCESSING; COMMUNICATION NETWORKS; INFORMATION MANAGEMENT; RUN TIME (COMPUTERS); PROVING; SYSTEMS ANALYSIS; NATIONAL AIRSPACE SYSTEM; AIRSPACE; AIR TRAFFIC; DATA FLOW ANALYSIS; SIMULATION; ERRORS; CONNECTORS; NASA PROGRAMS
Other Descriptors: RUNTIME VERIFICATION; LINEAR TEMPORAL LOGIC; MESSAGE-BASED SYSTEM
› Back to Top
Find Similar Records
NASA Logo, External Link
NASA Official: Gerald Steeman
Site Curator: STI Program
Last Modified: November 13, 2017
Contact Us