Difference between revisions of "Offline Team3 Benchmark1"

From CRV
Jump to: navigation, search
(Created page with "'''AuctionBidding'''. This property is about bids on items on an online auction site. == Benchmark Data == === The Trace Part === There are 4 traces in marq/offline/bench1...")
 
(Clarification Requests)
 
(4 intermediate revisions by 2 users not shown)
Line 1: Line 1:
'''AuctionBidding'''. This property is about bids on items on an online auction site.
+
This benchmark aims at detecting hazardous behaviours in aeronautic operations,
 +
and more specifically security procedure breaches. The data flow to be analysed
 +
results from the informations collected observing air traffic in a given area
 +
where air space is divided into several controlled or uncontrolled areas.
 +
 
 +
Category:Aerospace
  
 
== Benchmark Data ==
 
== Benchmark Data ==
Line 5: Line 10:
 
=== The Trace Part ===
 
=== The Trace Part ===
  
There are 4 traces in marq/offline/bench1
+
==== Trace structure ====
  
* auction_trace_valid
+
Traces are made of events with associated attributes. Events are essentially of two kinds: position-related (e.g. an aircraft is located at a given position), or communication-related (e.g. an aircraft sets its radio to a given frequency, or an aircraft asks for or receives a clearance, or an aircraft indicates having reached a waypoint, or a meteorological alert is raised...). Attributes are values associated to each event instance.
* auction_trace_invalid1
+
* auction_trace_invalid2
+
* auction_trace_invalid3
+
  
The first trace satisfies the property and is a long trace of 13,430,408 events with 484,416 create_auction events, 12,846,793 bid events, 98,199 sold events and 1000 endOfDay events.
+
The following examples show attributes associated to various events:
  
The other three traces are relatively short traces capturing different ways in which the property can be violated.
+
* position (attributes: aircraft id, latitude, longitude, altitude, velocity, horizontal velocity, vertical velocity): an aircraft with a given id is at given coordinates at the time where the event occurs;
* invalid1 sells an item for less than the minimum
+
* clear_takeoff (attributes: aircraft id): an aircraft with a given id has received a clearance to take off at the time where the event occurs;
* invalid2 sells an item after its period expires
+
* set_frequency (attributes: aircraft id, frequency): an aircraft with a given id has its radio set to a given frequency at the time where the event occurs;
* invalid3 sells an item twice
+
* wind_information (attributes: wind direction, wind speed): meteorological information is provided for wind, including its direction and speed;
 +
* etc.
  
These are all based on a trace consisting of the first 6 days (84,780 events) of the valid trace. This consists of 3062 create_auction events, 80,742 bid events, 970 sold events and 6 endOfDay events. In the first two cases data values are altered to make the traces invalid and in the third case an additional sold event occurs.
+
Traces are found in different files:
  
The trace to be used in the competition is auction_trace_valid, other traces are for demonstration/testing.
+
* 1 position file for each aircraft
 +
* a single file for all communication-related events
  
=== The Property Part ===
+
The entries in these files are as follows:
  
==== Informal Description ====
+
Time, Event name, attribute_name_1, value_1, attribute_name_2, value_2, ..., attribute_name_n, value_n
  
When an item is being sold an auction is created and recorded using the create_auction(item,minimum,period) event where minimum is the minimum price the item can be sold for and period is the number of days the auction will last. Each bid on the item must be strictly larger than the previous bid; bids are recorded by the event bid(item,amount). The auction is over when the period is over or the item is sold. An item can only be and must be sold if the last bid amount is greater than the minimum price; the sold(item) event records when an item is sold. After the auction is over no events related to the item are allowed. An item can only be placed for auction once. The passing of days is recorded by a propositional endOfDay event; the period of an auction is over when there have been period number of endOfDay events.
+
where n is the maximum number of attributes associated to an element (in our example, 7).
  
==== Demonstration Traces ====
+
==== Provided traces ====
  
The following traces should be accepted
+
In the example provided here, there are two aircrafts considered, hence two file for positions (trajectory_153.csv and trajectory_147.csv).
  
    create_auction(hat,4,10).bid(hat,1).bid(hat,3).bid(hat,4).sold(hat)
+
Traces will differ only on the communication part; however, the position file is also needed as it intervenes in the determination that a behaviour is hazardous.  
    create_auction(hat,4,10).endOfDay.endOfDay.bid(hat,3)
+
    create_auction(shoes,50,2).create_auction(hat,4,10).bid(shoes,50).bid(hat,3).sold(shoes)
+
  
The following traces should be rejected
+
We provide different files exhibiting different behaviours:
  
    create_auction(hat,5,10).bid(hat,1).bid(hat,3).bid(hat,4).sold(hat)
+
* com_1.csv is nominal and no hazardous behaviour is detected
    create_auction(hat,4,1).endOfDay.endOfDay.bid(hat,3)
+
* com_2.csv exhibits an hazardous behaviour that must be detected
    create_auction(shoes,50,2).create_auction(hat,4,10).bid(shoes,50).bid(hat,5).sold(shoes)
+
* com_3.csv exhibits an hazardous behaviour that must be detected
 +
* com_4.csv exhibits an hazardous behaviour that must be detected
 +
* com_5.csv exhibits an hazardous behaviour that must be detected
  
Each of these invalid traces are versions of the valid traces where a number has been changed to make the trace invalid. In the first trace the hat is sold for less than the minimum. In the second trace there is a bid on the hat after the period ends. In the third trace the hat has had a bid that takes it above the minimum but has not been sold.
 
  
 +
=== Property part ===
  
==== Formal Specification ====
+
==== Informal description ====
  
    qea(AuctionBidding){
+
The purpose is to detect when an aircraft violates security procedures, i.e. either takes off without a clearance (or with an expired clearance), or does not set its radio frequency so as to communicate correctly with the air traffic control, or takes off when there is an alert for strong wind.
      Forall(item)
+
 
     
+
These behaviour require the identification of several refined behaviours, some of which are deduced from positions (e.g. takeoff) and some of which are deduced from communications (e.g. clearance received), which
      accept next(start){
+
which are then cross-combined temporally.
          create_auction(item,minimum,period) -> created
+
 
          endOfDay -> start
+
==== Formal description ====
      }
+
 
      accept next(created){
+
Properties are organised in three levels.
          endOfDay if[ period>1 ] do[ period:=period-1 ] -> created
+
 
          endOfDay if[ period=1 ] -> auctionOver
+
The 1st level describes elementary behaviours:
          bid(item,amount) if [ amount > last_amount and amount < minimum ]
+
 
                          do [ last_amount:=amount ] -> created
+
* OnGround(id, h): the aircraft with ID id is on ground (i.e. at an altitude below h), i.e. an event e is detected where e.name = position, e.ID = id, and e.altitude < h
          bid(item,amount) if [ amount > last_amount and amount >= minimum ]
+
* AboveGround(id, h): the aircraft with ID id is on ground (i.e. at an altitude above h), i.e. an event e is detected where e.name = position, e.ID = id, and e.altitude > h
                          do [ last_amount:=amount ] -> aboveMin
+
* FreqDiffFrom (id, f): the aircraft with ID id is not at frequence f, i.e. an event e is detected where e.name = set_frequency, e.ID = id, e.freq /= f
      }
+
* ClearanceTakeOff(id): the aircraft with ID id has received a clearance for takeoff, i.e. an event e is detected where e.name = clear_takeoff and e.ID = id
      next(aboveMin){
+
* WindInfo(d, ws): wind has changed and now originates from direction d and has speed ws.
          bind(item,amount) if[ amount > last_amount ] do [ last_amount:=amount ] -> aboveMin
+
 
          sold(item) -> auctionOver
+
The 2nd level is deduced from the previous one to represent more elaborated properties:
          endOfDay if[ period>1 ] do[ period:=period-1 ] -> aboveMin
+
 
      }
+
* TakeOff(id, H) is described as: this is the first time that property AboveGround(id, h) is satisfied after an instant where property OnGround(id, h) was satisfied
      accept next(auctionOver){ endOfDay -> auctionOver }
+
* WindAlertRaised() is described as: this is the first time that property WindInfo(d, ws) is satisfied with ws >= 40 knots since the beginning or since this property was satisfied with ws < 40 knots
    }
+
* WindAlertLifted() is described as: this is the first time that property WindInfo(d, ws) is satisfied with ws < 40 knots since this property was satisfied with ws >= 40 knots
 +
 
 +
 
 +
The 3rd level is deduced from the two previous one and represents security breaches to be detected
 +
 
 +
* NoClearanceToTakeOff(id) is described as: either TakeOff(id, 15) has been detected and no ClearanceTakeOff(id) has been detected previously, or this is the first time that TakeOff(id, 15) is detected after the detection of ClearanceTakeOff(id) but at least 60 seconds have elapsed since this last detection
 +
* NoFrequencyToTakeOff(id) is described as either one of three possibilities: (1) a wrong frequency is set after which 5 seconds elapse, during which no other frequency is set, or (2) within 5 seconds after takeoff a wrong frequency is set and the right frequency is not set before the end of these 5 seconds, or (3) no frequency has been set at until at least 5 seconds after takeoff
 +
* TakeOffByStrongWind(id) is described by: either TakeOff(id, 15) takes place and, within 10 seconds before or after takeoff, WindAlertRaised() is satisfied, or WindAlertRaised() is followed by TakeOff(id, 15) without WindAlertLifted() taking place at least 10 seconds before takeoff.
 +
 
 +
Note that the airport considered in the example has an altitude of 15, which is why this value appears in the behaviours above to determine takeoff.
 +
 
 +
==== Demonstration Traces ====
 +
 
 +
Let us recall that a trace is made of three files: trajectory_153.csv and trajectory_747.csv describing aircraft positions, and com_n.csv (where n is a scenario number ranging from 1 to 4) describing communications.
 +
 
 +
The following results must be obtained:
 +
 +
* with both trajectories and com_1.csv, no hazardous behaviour must be detected
 +
* with both trajectories and com_2.csv, only hazardous behaviour NoFrequencyToTakeOff(153) must be detected
 +
* with both trajectories and com_3.csv, only hazardous behaviour NoClearanceToTakeOff(153) must be detected
 +
* with both trajectories and com_4.csv, only hazardous behaviour NoFrequencyToTakeOff(153) must be detected
 +
* with both trajectories and com_5.csv, only hazardous behaviours TakeOffByStrongWind(153) and TakeOffByStrongWind(747) must be detected
  
==== A FO-LTL Specification ====
 
  
 
== Clarification Requests ==
 
== Clarification Requests ==
  
This is a space where other teams can ask for clarifications and the submitting team can answer. When a team requests a clarification, the team should be mentioned in the request and the request timestamped. The team submitting the benchmark should ensure they watch this page so that they get notifications of questions.
+
A few initial comments.
 +
 
 +
Firstly, it seems to me that each of the four com_x files represent separate 'benchmarks' in the competition terminology. Therefore, for consistency a separate page should be created for each one. The property part etc need not be replicated (reference the first benchmark).
 +
 
 +
Secondly, in NoFrequencyToTakeOff I am not sure what wrong and right frequencies means, these do not seem to relate to previously introduced definitions.
 +
 
 +
Thirdly, the idea of the demonstrator traces is to give short explanations of the behaviour without referring to external information or any formal specification. When I have looked at the properties further I can give an example of what I mean by this.
 +
 
 +
Finally, the rules state that there should be a single trace file. I suggest using the following script to merge the trace files into a single trace and making both the merged and unmerged versions available.
 +
 
 +
    #!/usr/bin/env python
 +
   
 +
    import sys
 +
   
 +
    if len(sys.argv) != 3:
 +
      print "Give the two csv files to merge"
 +
      sys.exit(0)
 +
   
 +
    one = sys.argv[1]
 +
    two = sys.argv[2]
 +
   
 +
    l1 = [line.strip().split(',') for line in open(one, 'r')]
 +
    l2 = [line.strip().split(',') for line in open(two, 'r')]
 +
   
 +
    h1 = l1[0]
 +
    h2 = l2[0]
 +
   
 +
    if cmp(h1,h2):
 +
      print "The headers should be the same"
 +
      sys.exit(0)
 +
   
 +
    print ", ".join(h1)
 +
   
 +
    l1=l1[1:]
 +
    l2=l2[1:]
 +
   
 +
    while l1 and l2:
 +
   
 +
      if float(l1[0][0]) < float(l2[0][0]):
 +
        print ", ".join(l1[0])
 +
        l1 = l1[1:]
 +
      else:
 +
        print ", ".join(l2[0])
 +
        l2 = l2[1:]
 +
   
 +
    for l in l1:
 +
      print ", ".join(l)
 +
    for l in l2:
 +
      print ", ".join(l)

Latest revision as of 16:32, 14 June 2016

This benchmark aims at detecting hazardous behaviours in aeronautic operations, and more specifically security procedure breaches. The data flow to be analysed results from the informations collected observing air traffic in a given area where air space is divided into several controlled or uncontrolled areas.

Category:Aerospace

Benchmark Data

The Trace Part

Trace structure

Traces are made of events with associated attributes. Events are essentially of two kinds: position-related (e.g. an aircraft is located at a given position), or communication-related (e.g. an aircraft sets its radio to a given frequency, or an aircraft asks for or receives a clearance, or an aircraft indicates having reached a waypoint, or a meteorological alert is raised...). Attributes are values associated to each event instance.

The following examples show attributes associated to various events:

  • position (attributes: aircraft id, latitude, longitude, altitude, velocity, horizontal velocity, vertical velocity): an aircraft with a given id is at given coordinates at the time where the event occurs;
  • clear_takeoff (attributes: aircraft id): an aircraft with a given id has received a clearance to take off at the time where the event occurs;
  • set_frequency (attributes: aircraft id, frequency): an aircraft with a given id has its radio set to a given frequency at the time where the event occurs;
  • wind_information (attributes: wind direction, wind speed): meteorological information is provided for wind, including its direction and speed;
  • etc.

Traces are found in different files:

  • 1 position file for each aircraft
  • a single file for all communication-related events

The entries in these files are as follows:

Time, Event name, attribute_name_1, value_1, attribute_name_2, value_2, ..., attribute_name_n, value_n

where n is the maximum number of attributes associated to an element (in our example, 7).

Provided traces

In the example provided here, there are two aircrafts considered, hence two file for positions (trajectory_153.csv and trajectory_147.csv).

Traces will differ only on the communication part; however, the position file is also needed as it intervenes in the determination that a behaviour is hazardous.

We provide different files exhibiting different behaviours:

  • com_1.csv is nominal and no hazardous behaviour is detected
  • com_2.csv exhibits an hazardous behaviour that must be detected
  • com_3.csv exhibits an hazardous behaviour that must be detected
  • com_4.csv exhibits an hazardous behaviour that must be detected
  • com_5.csv exhibits an hazardous behaviour that must be detected


Property part

Informal description

The purpose is to detect when an aircraft violates security procedures, i.e. either takes off without a clearance (or with an expired clearance), or does not set its radio frequency so as to communicate correctly with the air traffic control, or takes off when there is an alert for strong wind.

These behaviour require the identification of several refined behaviours, some of which are deduced from positions (e.g. takeoff) and some of which are deduced from communications (e.g. clearance received), which which are then cross-combined temporally.

Formal description

Properties are organised in three levels.

The 1st level describes elementary behaviours:

  • OnGround(id, h): the aircraft with ID id is on ground (i.e. at an altitude below h), i.e. an event e is detected where e.name = position, e.ID = id, and e.altitude < h
  • AboveGround(id, h): the aircraft with ID id is on ground (i.e. at an altitude above h), i.e. an event e is detected where e.name = position, e.ID = id, and e.altitude > h
  • FreqDiffFrom (id, f): the aircraft with ID id is not at frequence f, i.e. an event e is detected where e.name = set_frequency, e.ID = id, e.freq /= f
  • ClearanceTakeOff(id): the aircraft with ID id has received a clearance for takeoff, i.e. an event e is detected where e.name = clear_takeoff and e.ID = id
  • WindInfo(d, ws): wind has changed and now originates from direction d and has speed ws.

The 2nd level is deduced from the previous one to represent more elaborated properties:

  • TakeOff(id, H) is described as: this is the first time that property AboveGround(id, h) is satisfied after an instant where property OnGround(id, h) was satisfied
  • WindAlertRaised() is described as: this is the first time that property WindInfo(d, ws) is satisfied with ws >= 40 knots since the beginning or since this property was satisfied with ws < 40 knots
  • WindAlertLifted() is described as: this is the first time that property WindInfo(d, ws) is satisfied with ws < 40 knots since this property was satisfied with ws >= 40 knots


The 3rd level is deduced from the two previous one and represents security breaches to be detected

  • NoClearanceToTakeOff(id) is described as: either TakeOff(id, 15) has been detected and no ClearanceTakeOff(id) has been detected previously, or this is the first time that TakeOff(id, 15) is detected after the detection of ClearanceTakeOff(id) but at least 60 seconds have elapsed since this last detection
  • NoFrequencyToTakeOff(id) is described as either one of three possibilities: (1) a wrong frequency is set after which 5 seconds elapse, during which no other frequency is set, or (2) within 5 seconds after takeoff a wrong frequency is set and the right frequency is not set before the end of these 5 seconds, or (3) no frequency has been set at until at least 5 seconds after takeoff
  • TakeOffByStrongWind(id) is described by: either TakeOff(id, 15) takes place and, within 10 seconds before or after takeoff, WindAlertRaised() is satisfied, or WindAlertRaised() is followed by TakeOff(id, 15) without WindAlertLifted() taking place at least 10 seconds before takeoff.

Note that the airport considered in the example has an altitude of 15, which is why this value appears in the behaviours above to determine takeoff.

Demonstration Traces

Let us recall that a trace is made of three files: trajectory_153.csv and trajectory_747.csv describing aircraft positions, and com_n.csv (where n is a scenario number ranging from 1 to 4) describing communications.

The following results must be obtained:

  • with both trajectories and com_1.csv, no hazardous behaviour must be detected
  • with both trajectories and com_2.csv, only hazardous behaviour NoFrequencyToTakeOff(153) must be detected
  • with both trajectories and com_3.csv, only hazardous behaviour NoClearanceToTakeOff(153) must be detected
  • with both trajectories and com_4.csv, only hazardous behaviour NoFrequencyToTakeOff(153) must be detected
  • with both trajectories and com_5.csv, only hazardous behaviours TakeOffByStrongWind(153) and TakeOffByStrongWind(747) must be detected


Clarification Requests

A few initial comments.

Firstly, it seems to me that each of the four com_x files represent separate 'benchmarks' in the competition terminology. Therefore, for consistency a separate page should be created for each one. The property part etc need not be replicated (reference the first benchmark).

Secondly, in NoFrequencyToTakeOff I am not sure what wrong and right frequencies means, these do not seem to relate to previously introduced definitions.

Thirdly, the idea of the demonstrator traces is to give short explanations of the behaviour without referring to external information or any formal specification. When I have looked at the properties further I can give an example of what I mean by this.

Finally, the rules state that there should be a single trace file. I suggest using the following script to merge the trace files into a single trace and making both the merged and unmerged versions available.

   #!/usr/bin/env python
   
   import sys
   
   if len(sys.argv) != 3:
     print "Give the two csv files to merge"
     sys.exit(0)
   
   one = sys.argv[1]
   two = sys.argv[2]
   
   l1 = [line.strip().split(',') for line in open(one, 'r')]
   l2 = [line.strip().split(',') for line in open(two, 'r')]
   
   h1 = l1[0]
   h2 = l2[0]
   
   if cmp(h1,h2):
     print "The headers should be the same"
     sys.exit(0)
   
   print ", ".join(h1)
   
   l1=l1[1:]
   l2=l2[1:]
   
   while l1 and l2:
   
     if float(l1[0][0]) < float(l2[0][0]):
       print ", ".join(l1[0])
       l1 = l1[1:]
     else:
       print ", ".join(l2[0])
       l2 = l2[1:]
   
   for l in l1:
     print ", ".join(l)
   for l in l2:
     print ", ".join(l)