Difference between revisions of "Java Team2 Benchmark1"

From CRV
Jump to: navigation, search
(→‎Formal Specification)
(→‎The Trace Part)
 
(26 intermediate revisions by 3 users not shown)
Line 7: Line 7:
 
=== The Trace Part ===
 
=== The Trace Part ===
  
−
The relevant files can be found on the server at: '''''filepath'''''
+
The relevant files can be found on the server at: ''home/larva/Benchmark1''
  
−
The script will run a scenario that '''''violates/satisfies''''' the property defined in the rest of this page.
+
The script will run a scenario that '''violates''' the property defined in the rest of this page.
  
−
== Instrumentation Information ==
+
''Instrumentation Information''
  
 
We have defined the following pointcuts to capture the relevant events for this benchmark (see the next section for their use):
 
We have defined the following pointcuts to capture the relevant events for this benchmark (see the next section for their use):
  
−
     pointcut userDepositFromExternal(Integer uid, Integer sid, String to_account_number, double amount) :  
+
     pointcut greylistUser(Integer uid) :  
−
         call(public boolean USER_depositFromExternal(Integer, Integer, String, double) && args(uid, sid, to_account_number, amount));
+
         call(public void Interface.ADMIN_greylistUser(Integer)) && args(uid);
 
 
−
     pointcut userPayToExternal(Integer uid, Integer sid, String from_account_number, double amount) :  
+
     pointcut whitelistUser(Integer uid) :  
−
         call(public boolean USER_payToExternal(Integer, Integer, String, double) && args(uid, sid, from_account_number, amount));
+
         call(public void Interface.ADMIN_whitelistUser(Integer)) && args(uid);
−
+
−
     pointcut userTransferOwnAccounts(Integer uid, Integer sid, String from_account_number, String to_account_number, double amount) :  
+
     pointcut depositTo(Integer uid, double amount, String to_account_number, Integer sid) :  
−
         call(public boolean USER_transferOwnAccounts(Integer, Integer, String, String, double) && args(uid, sid, from_account_number, to_account_number, amount));
+
         call(public void Interface.USER_depositFromExternal(..)) && args(uid, sid, to_account_number, amount);
−
 
+
−
    pointcut reconcile() :
+
−
        call(public void ADMIN_reconcile());
+
−
 
+
  
−
== Trace Statistics ==
 
  
 +
''Trace Statistics''
  
 
{| class="wikitable"
 
{| class="wikitable"
Line 36: Line 32:
 
! Occurrences
 
! Occurrences
 
|-
 
|-
−
| userDepositFromExternal
+
| greylistUser
−
|  
+
| 10001
 
|-
 
|-
−
| userPayToExternal
+
| whitelistUser
−
|  
+
| 10001
 
|-
 
|-
−
| userTransferOwnAccounts
+
| depositTo
−
|  
+
| 40002
−
|-
+
−
| reconcile
+
 
|}
 
|}
  
Line 52: Line 46:
 
==== Informal Description ====
 
==== Informal Description ====
  
−
The administrator must reconcile accounts after every 1000 attempted external money transfers or after an aggregate total of one million dollars in attempted external transfers (attempted transfers include transfers requested which never took place due to lack of funds).
+
FiTS contains an object ''UserInfo'' that corresponds to a user. A user can be greylisted, blacklisted, or whitelisted.
 +
 
 +
Once greylisted, a user must perform at least three incoming transfers before being whitelisted.
  
 
==== Demonstration Traces ====
 
==== Demonstration Traces ====
  
−
The property is specified formally in a Guarded Command Language, units in which consist of an event, guarded by a condition, upon which a specified action is performed. For more information see [https://drive.google.com/file/d/0B-0CQ8SP0TYjWmF5THdmbDNQeHM/view?usp=sharing].
+
Assume that ''userInfo.uid = uid'', and ''userInfo'.uid = uid''' in the following traces.
−
 
+
  
 
''Satisfying Traces''
 
''Satisfying Traces''
  
−
* greylist(u); depositTo(u); depositTo(u); depositTo(u); whitelist(u);
+
* greylist(uid); depositTo(uid); depositTo(userInfo); depositTo(userInfo); whitelist(uid);
  
−
* greylist(u'); depositTo(u); depositTo(u);
+
* greylist(uid'); depositTo(userInfo); depositTo(userInfo);
  
−
* depositTo(u); depositTo(u); greylist(u)
+
* depositTo(userInfo); depositTo(userInfo); greylist(uid)
 +
 
 +
Note how the satisfying traces either whitelist a greylisted user after three deposits (the first one), or do not attempt whitelisting at all (avoiding a possible violation of the property).
  
 
''Violating Traces''
 
''Violating Traces''
  
−
* greylist(u); depositTo(u'); depositTo(u'); depositTo(u'); whitelist(u)
+
* greylist(uid); depositTo(userInfo'); depositTo(userInfo'); depositTo(userInfo'); whitelist(uid)
  
−
* depositTo(u); depositTo(u); depositTo(u); greylist(u'); whitelist(u)
+
* greylist(uid); depositTo(userInfo); depositTo(userInfo); depositTo(userInfo); greylist(uid'); whitelist(uid')
  
−
* depositTo(u); depositTo(u); greylist(u); depositTo(u); depositTo(u); whitelist(u)
+
* depositTo(userInfo); depositTo(userInfo); greylist(uid); depositTo(userInfo); depositTo(userInfo); whitelist(uid)
 +
 
 +
On the other hand these violating traces all attempt to whitelist a greylisted user before three deposits to their account.
  
 
==== Formal Specification ====
 
==== Formal Specification ====
  
−
The property is specified formally in a Guarded Command Language, units in which consist of an event, guarded by a condition, upon which a specified action is performed. For more information see [https://drive.google.com/file/d/0B-0CQ8SP0TYjWmF5THdmbDNQeHM/view?usp=sharing].
+
As a formal specification we use regular expressions over traces, defining both an expression for a satisfying and a violating trace. Each of these events are defined with respect to an object ''u'' of type ''UserInfo'' (e.g. such that the event ''greylist'' refers to ''u'' being greylisted).
 +
 
 +
Regular Expression for satisfying traces:
 +
 
 +
    property foreach target (UserInfo u) matching{
 +
        ((!greylist)* ; greylist ; ((!whitelist)* ; depositTo ; (!whitelist)* ; depositTo ;
 +
        (!whitelist)* ; depositTo ; (!whitelist)*) ; whitelist )*
 +
    }
 +
 
 +
 
 +
Regular Expression for violating traces:
  
−
    userDepositFromExternal | -> {  
+
    property foreach target (UserInfo u) not matching{
−
          Verification.countExternalTransferAttempts++; Verification.totalExternalTransferAttempts+=amount;  
+
        (?)* ; greylist ; ((!depositTo)* + (!depositTo)* ; depositTo ;
−
          if (Verification.countExternalTransferAttempts>1000 || Verification.totalExternalTransferAttempts>1000000) {
+
        (!depositTo)* + (!depositTo)* ; depositTo ; (!depositTo)*; depositTo;
−
            Verification.fail("P8 violated");
+
        (!depositTo)*) ; whitelist
−
          }
+
    }
−
    }
+
−
    userPayToExternal | -> {
+
−
          Verification.countExternalTransferAttempts++; Verification.totalExternalTransferAttempts+=amount;  
+
−
          if (Verification.countExternalTransferAttempts>1000 || Verification.totalExternalTransferAttempts>1000000) {
+
−
            Verification.fail("P8 violated");
+
−
          }
+
−
    }
+
−
    reconcile | -> {
+
−
        Verification.countExternalTransferAttempts=0;
+
−
        Verification.totalExternalTransferAttempts=0;
+
−
    }
+
  
 
==== A FO-LTL Specification ====
 
==== A FO-LTL Specification ====
Line 101: Line 99:
  
 
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.
 
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.
 +
* The pointcut depositTo is never called with the provided definition. The args condition contains uid which is never declared. Furthermore, to match the given traces the pointcut should be parameterized with uid and not with account_number and amount. --Malte, Mufin, 2016-07-05T18
 +
**Sorry missed these; see the corrected pointcut. You can get the relevant uid from the user parameter. -- Shaun, Larva, 2016-07-19
 +
* Is the lack of breaks in the switch in the Main.main intended? In case of the CLI argument "1" all three scenarios Scenarios.runViolatingScenarioForProperty(6), Scenarios.runNonViolatingScenarioForProperty(8), and Scenarios.runViolatingScenarioForProperty(10) are executed. --Malte, Mufin, 2016-07-05T18
 +
** This was corrected. -- Shaun, Larva, 2016-07-19
 +
* The length of the benchmark means that performance monitoring will tell us very little. I suggest two solutions (i) we only score this benchmark for correctness, (ii) you loop some of the behaviour to give a non-trivial workload -- Giles, 2016-07-06
 +
* The clarity of the benchmark would be improved by (i) explaining the demonstration traces and (ii) explaining the relation between the two regular expression properties and what matching means i.e. are the regular expressions 'prefix-closed'.

Latest revision as of 11:12, 23 July 2016

FiTS (A Financial Transaction System) is a bare-bones system mocking the behaviour of a financial transaction system. It emulates a virtual banking system in which users may open accounts from which they may perform money transfers. For more information read the manual at [1]

Categories: Financial

Benchmark Data

The Trace Part

The relevant files can be found on the server at: home/larva/Benchmark1

The script will run a scenario that violates the property defined in the rest of this page.

Instrumentation Information

We have defined the following pointcuts to capture the relevant events for this benchmark (see the next section for their use): 

   pointcut greylistUser(Integer uid) : 
       call(public void Interface.ADMIN_greylistUser(Integer)) && args(uid);

   pointcut whitelistUser(Integer uid) : 
       call(public void Interface.ADMIN_whitelistUser(Integer)) && args(uid);

   pointcut depositTo(Integer uid, double amount, String to_account_number, Integer sid) : 
       call(public void Interface.USER_depositFromExternal(..)) && args(uid, sid, to_account_number, amount);


Trace Statistics

Event Occurrences
greylistUser 10001
whitelistUser 10001
depositTo 40002

The Property Part

Informal Description

FiTS contains an object UserInfo that corresponds to a user. A user can be greylisted, blacklisted, or whitelisted.

Once greylisted, a user must perform at least three incoming transfers before being whitelisted.

Demonstration Traces

Assume that userInfo.uid = uid, and userInfo'.uid = uid' in the following traces.

Satisfying Traces

  • greylist(uid); depositTo(uid); depositTo(userInfo); depositTo(userInfo); whitelist(uid);
  • greylist(uid'); depositTo(userInfo); depositTo(userInfo);
  • depositTo(userInfo); depositTo(userInfo); greylist(uid)

Note how the satisfying traces either whitelist a greylisted user after three deposits (the first one), or do not attempt whitelisting at all (avoiding a possible violation of the property).

Violating Traces

  • greylist(uid); depositTo(userInfo'); depositTo(userInfo'); depositTo(userInfo'); whitelist(uid)
  • greylist(uid); depositTo(userInfo); depositTo(userInfo); depositTo(userInfo); greylist(uid'); whitelist(uid')
  • depositTo(userInfo); depositTo(userInfo); greylist(uid); depositTo(userInfo); depositTo(userInfo); whitelist(uid)

On the other hand these violating traces all attempt to whitelist a greylisted user before three deposits to their account.

Formal Specification

As a formal specification we use regular expressions over traces, defining both an expression for a satisfying and a violating trace. Each of these events are defined with respect to an object u of type UserInfo (e.g. such that the event greylist refers to u being greylisted).

Regular Expression for satisfying traces: 

    property foreach target (UserInfo u) matching{
       ((!greylist)* ; greylist ; ((!whitelist)* ; depositTo ; (!whitelist)* ; depositTo ;
       (!whitelist)* ; depositTo ; (!whitelist)*) ; whitelist )*
    }


Regular Expression for violating traces: 

    property foreach target (UserInfo u) not matching{
        (?)* ; greylist ; ((!depositTo)* + (!depositTo)* ; depositTo ;
        (!depositTo)* + (!depositTo)* ; depositTo ; (!depositTo)*; depositTo; 
        (!depositTo)*) ; whitelist
    }

A FO-LTL Specification

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.

  • The pointcut depositTo is never called with the provided definition. The args condition contains uid which is never declared. Furthermore, to match the given traces the pointcut should be parameterized with uid and not with account_number and amount. --Malte, Mufin, 2016-07-05T18
    • Sorry missed these; see the corrected pointcut. You can get the relevant uid from the user parameter. -- Shaun, Larva, 2016-07-19
  • Is the lack of breaks in the switch in the Main.main intended? In case of the CLI argument "1" all three scenarios Scenarios.runViolatingScenarioForProperty(6), Scenarios.runNonViolatingScenarioForProperty(8), and Scenarios.runViolatingScenarioForProperty(10) are executed. --Malte, Mufin, 2016-07-05T18
    • This was corrected. -- Shaun, Larva, 2016-07-19
  • The length of the benchmark means that performance monitoring will tell us very little. I suggest two solutions (i) we only score this benchmark for correctness, (ii) you loop some of the behaviour to give a non-trivial workload -- Giles, 2016-07-06
  • The clarity of the benchmark would be improved by (i) explaining the demonstration traces and (ii) explaining the relation between the two regular expression properties and what matching means i.e. are the regular expressions 'prefix-closed'.
Retrieved from "http://165.22.237.132/wiki/index.php?title=Java_Team2_Benchmark1&oldid=272"