Difference between revisions of "Java Team2 Benchmark1"

From CRV
Jump to: navigation, search
Line 15: Line 15:
 
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 greylistUser(Integer uid) :  
+
     pointcut userDepositFromExternal(Integer uid, Integer sid, String to_account_number, double amount) :  
−
         call(public void Interface.ADMIN_greylistUser(Integer) && args(uid));
+
         call(public boolean USER_depositFromExternal(Integer, Integer, String, double) && args(uid, sid, to_account_number, amount));
 
 
−
     pointcut whitelistUser(Integer uid) :  
+
     pointcut userPayToExternal(Integer uid, Integer sid, String from_account_number, double amount) :  
−
         call(public void Interface.ADMIN_whitelistUser(Integer) && args(uid));
+
         call(public boolean USER_payToExternal(Integer, Integer, String, double) && args(uid, sid, from_account_number, amount));
−
+
−
     pointcut depositTo(String account_number, double amount) :  
+
     pointcut userTransferOwnAccounts(Integer uid, Integer sid, String from_account_number, String to_account_number, double amount) :  
−
         call(public void UserInfo.depositTo(String, double) && args(uid, account_number, amount));
+
         call(public boolean USER_transferOwnAccounts(Integer, Integer, String, String, double) && args(uid, sid, from_account_number, to_account_number, amount));
 +
 
 +
    pointcut reconcile() :
 +
        call(public void ADMIN_reconcile());
 +
 
  
 
== Trace Statistics ==
 
== Trace Statistics ==
Line 32: Line 36:
 
! Occurrences
 
! Occurrences
 
|-
 
|-
−
| greylistUser
+
| userDepositFromExternal
 
|  
 
|  
 
|-
 
|-
−
| whitelistUser
+
| userPayToExternal
 
|  
 
|  
 
|-
 
|-
−
| depositTo
+
| userTransferOwnAccounts
 
|  
 
|  
 +
|-
 +
| reconcile
 
|}
 
|}
  
Line 46: Line 52:
 
==== Informal Description ====
 
==== Informal Description ====
  
−
FiTS contains an object ''UserInfo'' that corresponds to a user. A user can be greylisted, blacklisted, or whitelisted.
+
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).
−
 
+
−
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].
 +
  
 
''Satisfying Traces''
 
''Satisfying Traces''
Line 70: Line 77:
 
==== Formal Specification ====
 
==== 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).
+
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].
−
 
+
−
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 | -> {
 +
          Verification.countExternalTransferAttempts++; Verification.totalExternalTransferAttempts+=amount;
 +
          if (Verification.countExternalTransferAttempts>1000 || Verification.totalExternalTransferAttempts>1000000) {
 +
            Verification.fail("P8 violated");
 +
          }
 +
    }
 +
    userPayToExternal | -> {
 +
          Verification.countExternalTransferAttempts++; Verification.totalExternalTransferAttempts+=amount;
 +
          if (Verification.countExternalTransferAttempts>1000 || Verification.totalExternalTransferAttempts>1000000) {
 +
            Verification.fail("P8 violated");
 +
          }
 +
    }
 +
    reconcile | -> {
 +
        Verification.countExternalTransferAttempts=0; Verification.totalExternalTransferAttempts=0;
 +
    }
  
−
    property foreach target (UserInfo u) not matching{
 
−
        (?)* ; greylist ; ((!depositTo)* + (!depositTo)* ; depositTo ;
 
−
        (!depositTo)* + (!depositTo)* ; depositTo ; (!depositTo)*; depositTo;
 
−
        (!depositTo)*) ; whitelist
 
−
    }
 
  
 
==== A FO-LTL Specification ====
 
==== A FO-LTL Specification ====

Revision as of 18:23, 2 June 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: filepath

The script will run a scenario that violates/satisfies 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 userDepositFromExternal(Integer uid, Integer sid, String to_account_number, double amount) : 
       call(public boolean USER_depositFromExternal(Integer, Integer, String, double) && args(uid, sid, to_account_number, amount));

   pointcut userPayToExternal(Integer uid, Integer sid, String from_account_number, double amount) : 
       call(public boolean USER_payToExternal(Integer, Integer, String, double) && args(uid, sid, from_account_number, amount));

   pointcut userTransferOwnAccounts(Integer uid, Integer sid, String from_account_number, String to_account_number, double amount) : 
       call(public boolean USER_transferOwnAccounts(Integer, Integer, String, String, double) && args(uid, sid, from_account_number, to_account_number, amount));

   pointcut reconcile() : 
       call(public void ADMIN_reconcile());


Trace Statistics

Event Occurrences
userDepositFromExternal
userPayToExternal
userTransferOwnAccounts
reconcile

The Property Part

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).

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 [2].


Satisfying Traces

  • greylist(u); depositTo(u); depositTo(u); depositTo(u); whitelist(u);
  • greylist(u'); depositTo(u); depositTo(u);
  • depositTo(u); depositTo(u); greylist(u)

Violating Traces

  • greylist(u); depositTo(u'); depositTo(u'); depositTo(u'); whitelist(u)
  • depositTo(u); depositTo(u); depositTo(u); greylist(u'); whitelist(u)
  • depositTo(u); depositTo(u); greylist(u); depositTo(u); depositTo(u); whitelist(u)

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 [3]. 

   userDepositFromExternal | -> { 
         Verification.countExternalTransferAttempts++; Verification.totalExternalTransferAttempts+=amount; 
         if (Verification.countExternalTransferAttempts>1000 || Verification.totalExternalTransferAttempts>1000000) {
            Verification.fail("P8 violated");
         }
   }
   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

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.

Retrieved from "http://165.22.237.132/wiki/index.php?title=Java_Team2_Benchmark1&oldid=91"