NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Back to Results
Data Automata in ScalaThe field of runtime verification has during the last decade seen a multitude of systems for monitoring event sequences (traces) emitted by a running system. The objective is to ensure correctness of a system by checking its execution traces against formal specifications representing requirements. A special challenge is data parameterized events, where monitors have to keep track of the combination of control states as well as data constraints, relating events and the data they carry across time points. This poses a challenge wrt. efficiency of monitors, as well as expressiveness of logics. Data automata is a form of automata where states are parameterized with data, supporting monitoring of data parameterized events. We describe the full details of a very simple API in the Scala programming language, an internal DSL (Domain-Specific Language), implementing data automata. The small implementation suggests a design pattern. Data automata allow transition conditions to refer to other states than the source state, and allow target states of transitions to be inlined, offering a temporal logic flavored notation. An embedding of a logic in a high-level language like Scala in addition allows monitors to be programmed using all of Scala's language constructs, offering the full flexibility of a programming language. The framework is demonstrated on an XML processing scenario previously addressed in related work.
Document ID
20160005624
Document Type
Other
External Source(s)
Authors
Havelund, Klaus (Jet Propulsion Lab., California Inst. of Tech. Pasadena, CA, United States)
Date Acquired
May 2, 2016
Publication Date
September 1, 2014
Subject Category
Computer Programming and Software
Funding Number(s)
CONTRACT_GRANT: NSF CCF-0926190
Distribution Limits
Public
Copyright
Other
Keywords
runtime verification
XML
monitor
internal DSL
parameterized state machines