███╗ ██╗███████╗███████╗██████╗
████╗ ██║██╔════╝██╔════╝██╔══██╗
██╔██╗ ██║█████╗ █████╗ ██████╔╝
██║╚██╗██║██╔══╝ ██╔══╝ ██╔══██╗
██║ ╚████║██║ ███████╗██║ ██║
╚═╝ ╚═══╝╚═╝ ╚══════╝╚═╝ ╚═╝
Version 1.0.1, June 7 - 2021
A stable version of nfer appeared in 2016.
Only minor updates have occurred since.
Copyright (c) 2021 California Institute of Technology (“Caltech”). U.S. Government sponsorship acknowledged.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
nfer is a Scala package for generating abstractions from event traces. nfer allows to define intervals over an event trace. The intervals indicate abstractions that for example can be visualized. An interval consists of a name, two time stamps: the beginning and the end of the interval, and a map from variable names (strings) to values, indicating data that the interval carries.
The nfer system is described in detail in this paper.
As an example, consider a spacecraft scenario where we want to be informed if a downlink operation occurs during a 5-minute time interval where the flight computer reboots twice. This scenario could cause a potential loss of downlink information. We want to identify the following intervals (informally):
- A boot represents an interval during which the rover software is rebooting.
- A double boot represents an interval during which the rover boots twice within a 5-minute timeframe.
- A risk represents an interval during which the rover boots twice, and during which it also attempts to downlink information.
Our objective now is to formalize the definition of such intervals in the nfer specification language, and extract these intervals from a telemetry stream, based on such a specification. Specifically, in this case, we need a formalism for formally defining the following three kinds of intervals.
-
A
BOOTinterval starts with aBOOT_S(boot start) event and ends with aBOOT_E(boot end) event. TheBOOT_SandBOOT_Eevents are assumed to potentially occur in the trace. -
A
DBOOT(double boot) interval consists of two consecutiveBOOTintervals, with no more than 5-minutes from the end of the firstBOOTinterval to the start of the secondBOOTinterval. -
A
RISKinterval is aDBOOTinterval during which aDOWNLINKoccurs. TheDOWNLINKevent is assumed to potentially occur in the trace.
The following time line (with time stamps) illustrates a scenario with two boots, hence a double boot, within 5 minutes, and a downlink occurring during this period.
12923 13112 20439 27626 48028
|--------|--------|---------|------------|---------------->
BOOT_S BOOT_E | BOOT_S BOOT_E
|
|
DOWNLINK
The intervals can be formalized with the following nfer specification, say stored in a file spec.nfer:
BOOT :- BOOT_S before BOOT_E
map {count -> BOOT_S.count}
DBOOT :- b1:BOOT before b2:BOOT
where b2.begin - b1.end <= 300000
map {count -> b1.count}
RISK :- DOWNLINK during DBOOT
map {count -> DBOOT.count}
The specification consists of three rules, one for each generated
interval: the name of the generated interval occurs before the
:- sign. The rules are to be read as follows.
- A
BOOTinterval is created if aBOOT_Sevent occurs before aBOOT_Eevent. In addition thecountdata from the firstBOOT_Sevent is inherited to become part of theBOOTinterval. - Likewise, a
DBOOT(double boot) interval is created when observing aBOOTinterval occurring before anotherBOOTinterval with no more than 5 minutes (300,000 milliseconds) in between. - Finally, a
RISKinterval is created when observing aDOWNLINKduring aDBOOT(double boot) interval.
The nfer specification language also allows rules to be presented in modules, which can import other modules. The specification above can alternatively be presented as follows.
module Booting {
BOOT :- BOOT_S before BOOT_E
map {count -> BOOT_S.count}
}
module DoubleBooting {
import Booting;
DBOOT :- b1:BOOT before b2:BOOT
where b2.begin - b1.end <= 300000
map {count -> b1.count}
}
module Risking {
import DoubleBooting;
RISK :- DOWNLINK during DBOOT
map {count -> DBOOT.count}
}
In a modular specification it is the last module which becomes the effective one, as well as all the modules that it imports transitively.
The following Scala program (located in the diretory src/test/Scala/test/test0) illustrates how a specification is applied to
a trace.
We first import the nfer library.
After an instance of the Nfer class has been created,
it can be initiated with a specification, for example read from a text file (a specification can also be provided directly as a text string).
In this case we read in the specification in spec.nfer shown above (without modules).
Subsequently events can be submitted to the monitor. Finally we print out the generated intervals.
package test.test0
import nfer._
object Example {
def main(args: Array[String]): Unit = {
val nfer = new Nfer()
nfer.specFile("src/test/Scala/test/test0/spec.nfer")
nfer.submit("BOOT_S", 12923, "count" -> 42)
nfer.submit("BOOT_E", 13112)
nfer.submit("DOWNLINK", 20439)
nfer.submit("BOOT_S", 27626, "count" -> 43)
nfer.submit("BOOT_E", 48028)
nfer.printIntervals()
}
}
The output printed by nfer.printIntervals() is in this case the following.
=================================
Generated Intervals:
---------------------------------
BOOT : 2
Interval("BOOT",12923.00000,13112.00000,Map("count" -> 42))
Interval("BOOT",27626.00000,48028.00000,Map("count" -> 43))
DBOOT : 1
Interval("DBOOT",12923.00000,48028.00000,Map("count" -> 42))
RISK : 1
Interval("RISK",12923.00000,48028.00000,Map("count" -> 42))
---------------------------------
We can see that two BOOT intervals are generated, one DBOOT interval, and one RISK interval. E.g. the DBOOT interval:
Interval("DBOOT",12923.00000,48028.00000,Map("count" -> 42))
starts at time 12923, ends at time 48028, and carries the data defined by the map Map("count" -> 42). That is, count has the value 42.
We now present the grammar for the specification language.
The meta symbols used for defining the grammar are as follows.
X*means zero or moreXX+means one or moreX.X,*means zero or moreXseparated by commas.X,+means one or moreXseparated by commas.[X]means zero or oneX.X|YmeansXorY.';'means a symbol, in this case;. Also used for keywords.<spec>means a non-terminal, in this case that of specifications.X ::= ...defines the non-terminalX.int-<exp>means<exp>, but with the informal annotation that it must be an integer.
The grammar for the nfer specification language is as follows.
<spec> ::=
<rule>+
| <module>+
<module> ::= 'module' <ident> '{' [<imports>] <rule>* '}'
<imports> ::= 'import' <ident>,+ ';'
<rule> ::= <ident> ':-' <interval> [<where>] [<map>] [<endPoints>]
<interval> ::= <primaryInterval> (<intervalOp> <primaryInterval>)*
<primaryInterval> ::= <atomicInterval> | <parenInterval>
<atomicInterval> ::= [<label>] <ident>
<parenInterval> := '(' <interval> ')'
<label> ::= <ident> ':'
<where> ::= 'where' bool-<exp>
<map> ::= 'map' '{' (<ident> '->' <exp>),+ '}'
<endPoints> ::= 'begin' int-<exp> 'end' int-<exp>
<intervalOp> ::=
'also'
| 'before'
| 'meet'
| 'during'
| 'start'
| 'finish'
| 'overlap'
| 'slice'
| 'coincide'
<exp> ::=
<unaryOp> <exp> |
| <exp> <binaryOp> <exp>
| <stringLit>
| <natLit>
| <doubleLit>
| <boolLit>
| <beginTime>
| <endTime>
| <mapField>
| <call>
| '(' <exp> ')'
<unaryOp> ::= '-' | '!'
<binaryOp> ::= '&' | '|' | '+' | '-' | '*' | '/' | '%' | '<' | '<=' | '>' | '>=' | '=' | '!='
<stringLit> ::= """"[^"]*"""".r
<natLit> ::= """(\d+)""".r
<doubleLit> ::= """(\d+\.\d*|\d*\.\d+)([eE][+-]?\d+)?[fFdD]?""".r
<boolLit> ::= 'true' | 'false'
<beginTime> ::= <ident> '.' 'begin'
<endTime> ::= <ident> '.' 'end'
<mapField> ::= <ident> '.' <ident>
<call> ::= <ident> '(' <exp>,* ')'
The directory out contains the nfer jar file:
- out/artifacts/nfer_jar/nfer.jar
nfer is implemented in Scala. Install the Scala programming language if not already installed (https://www.scala-lang.org/download). nfer is implemented in Scala 2.13.5.
A thorough explanation of nfer, and its algorithms can be found in the following paper:
Inferring Event Stream Abstractions Sean Kauffman, Klaus Havelund, Rajeev Joshi, and Sebastian Fischmeister.
The nfer system was conceptualized and developed by (in alphabetic order): Klaus Havelund, Rajeev Joshi, and Sean Kauffman during Sean Kauffman's internship at JPL.
Several test cases were originally performed using properties and log files from JPL's MSL mission. These have not been open sourced.
Sean Kauffman implemented a C version of nfer, wrapped in a Python API:
nfer in C wrapped in a Python API
The C version uses a different algorithm, and also allows (a limited form of) negation.