Difference between revisions of "Java Team2 Benchmark2"

From CRV
Jump to: navigation, search
(The Trace Part)
(Clarification Requests)
 
Line 99: 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.
 
* Is the lack of breaks in the switch in the Main.main intended? In case of the CLI argument "2" the two scenarios Scenarios.runNonViolatingScenarioForProperty(8), and Scenarios.runViolatingScenarioForProperty(10) are executed. --Malte, Mufin, 2016-07-05T18
 
* Is the lack of breaks in the switch in the Main.main intended? In case of the CLI argument "2" the two scenarios Scenarios.runNonViolatingScenarioForProperty(8), and Scenarios.runViolatingScenarioForProperty(10) are executed. --Malte, Mufin, 2016-07-05T18
 +
**Nope, sorry, corrected. -- Shaun, Larva, 2016-07-12
 
* The signature of the pointcut userDepositFromExternal doesn't match the signature of the method with the same name in the Interface class: The return type differs. --Malte, Mufin, 2016-07-05T19
 
* The signature of the pointcut userDepositFromExternal doesn't match the signature of the method with the same name in the Interface class: The return type differs. --Malte, Mufin, 2016-07-05T19
 +
**Corrected. -- Shaun, Larva, 2016-07-12
 
* The reconcile pointcut is called 673 times which is one more then mentioned in the table above. --Malte, Mufin, 2016-07-05T19
 
* The reconcile pointcut is called 673 times which is one more then mentioned in the table above. --Malte, Mufin, 2016-07-05T19
 +
**Corrected. -- Shaun, Larva, 2016-07-12
 
* Please consider whether the workload is sufficient for performance measurement -- Giles 2016-07-06
 
* Please consider whether the workload is sufficient for performance measurement -- Giles 2016-07-06
 +
**Corrected. -- Shaun, Larva, 2016-07-12

Latest revision as of 14:03, 12 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/Benchmark2

The script will run a scenario that 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 void 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 reconcile() : 
       call(public void ADMIN_reconcile());

Trace Statistics

Event Occurrences
userDepositFromExternal 10000
userPayToExternal 10000
reconcile 9673

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

Satisfying Traces

  • userDepositFromExternal999; userDepositFromExternal; reconcile
  • userPayToExternal999; userPayToExternal; reconcile
  • userPayToExternal [Verification.totalExternalTransferAttempts < 1000000]; userPayToExternal [Verification.totalExternalTransferAttempts >= 1000000]; reconcile

Violating Traces

  • userDepositFromExternal999; userDepositFromExternal; userDepositFromExternal;
  • userPayToExternal999; userPayToExternal; userDepositFromExternal;
  • userPayToExternal [Verification.totalExternalTransferAttempts < 1000000]; userPayToExternal [Verification.totalExternalTransferAttempts >= 1000000]; userDepositFromExternal

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

   userDepositFromExternal | -> { 
         Verification.countExternalTransferAttempts++; 
         Verification.totalExternalTransferAttempts += amount; 
         if (Verification.countExternalTransferAttempts > 1000
             || Verification.totalExternalTransferAttempts > 1000000) {
                Verification.fail("Property violated");
         }
   }
   userPayToExternal | -> {
         Verification.countExternalTransferAttempts++; 
         Verification.totalExternalTransferAttempts += amount; 
         if (Verification.countExternalTransferAttempts > 1000 
             || Verification.totalExternalTransferAttempts > 1000000) {
                Verification.fail("Property violated");
         }
   }
   reconcile | -> { 
         Verification.countExternalTransferAttempts = 0; 
         Verification.totalExternalTransferAttempts = 0; 
   }

Note that we also make use of the static class Verification for the counting external transfer attempts and their amounts. This can be used by any attempts to monitor for this property.

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.

  • Is the lack of breaks in the switch in the Main.main intended? In case of the CLI argument "2" the two scenarios Scenarios.runNonViolatingScenarioForProperty(8), and Scenarios.runViolatingScenarioForProperty(10) are executed. --Malte, Mufin, 2016-07-05T18
    • Nope, sorry, corrected. -- Shaun, Larva, 2016-07-12
  • The signature of the pointcut userDepositFromExternal doesn't match the signature of the method with the same name in the Interface class: The return type differs. --Malte, Mufin, 2016-07-05T19
    • Corrected. -- Shaun, Larva, 2016-07-12
  • The reconcile pointcut is called 673 times which is one more then mentioned in the table above. --Malte, Mufin, 2016-07-05T19
    • Corrected. -- Shaun, Larva, 2016-07-12
  • Please consider whether the workload is sufficient for performance measurement -- Giles 2016-07-06
    • Corrected. -- Shaun, Larva, 2016-07-12