Search NASA⌕ Search
Home/Archive/NASA NTRS

NASA NTRS · 20120013817

Checking Flight Rules with TraceContract: Application of a Scala DSL for Trace Analysis

Barringer, Howard·Havelund, Klaus·Morris, Robert A.
View original source ↗Export metadata ↓

Abstract

Typically during the design and development of a NASA space mission, rules and constraints are identified to help reduce reasons for failure during operations. These flight rules are usually captured in a set of indexed tables, containing rule descriptions, rationales for the rules, and other information. Flight rules can be part of manual operations procedures carried out by humans. However, they can also be automated, and either implemented as on-board monitors, or as ground based monitors that are part of a ground data system. In the case of automated flight rules, one considerable expense to be addressed for any mission is the extensive process by which system engineers express flight rules in prose, software developers translate these requirements into code, and then both experts verify that the resulting application is correct. This paper explores the potential benefits of using an internal Scala DSL for general trace analysis, named TRACECONTRACT, to write executable specifications of flight rules. TRACECONTRACT can generally be applied to analysis of for example log files or for monitoring executing systems online.

Explore related subjects

temporal logicflight rules.Scaladomain specific languagestate machinestrace analysis

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Barringer, Howard, Havelund, Klaus, Morris, Robert A.. 2011-06-02. Checking Flight Rules with TraceContract: Application of a Scala DSL for Trace Analysis. https://ntrs.nasa.gov/citations/20120013817

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related reports

NASA NTRSDate not supplied

Seeing is Believing: Monitoring Future Time Temporal Logic

Runtime monitors for future-time unbounded temporal logics like RVLTL, LTL 3 and FLTL, have double-exponential (2^2^n) worst-case space complexity bounds in size of the input formula. The semantics of these logics require monitors to perform general satisfiability solving for LTL expressions, a well-studied problem whose computational complexity is NP-hard and PSPACE-complete. This paper introduces an unbounded future-time linear temporal logic defined over a lattice. We call our logic an incremental temporal logic as it can be viewed as incrementally constructing proofs about the trace. On this account, we view online runtime monitoring as a decision procedure for proofs systems about incrementally growing traces. We demonstrate that our incremental temporal logic allows monitor construction to void satisfiability solving while still soundly detecting when the property is violated in an online fashion. This enables asymptotic improvements in space complexity. As proof, we provide a procedure to construct monitors that utilize linear space and time in the size of the input formula, while remaining constant in the size of the input stream and suitable for online monitoring. We further demonstrate, through several examples, that our incremental temporal logic is straightforward to adopt and practical for runtime verification.

temporal logic↗