Difference between revisions of "Java Team2 Benchmark3"

From CRV
Jump to: navigation, search
(Created page with "'''Name of benchmark''' Two or three sentences that describe the benchmark. These can mention the domain, scope or source or the benchmark. Or might suggest the purpose of the...")
 
Line 1: Line 1:
−
'''Name of benchmark''' Two or three sentences that describe the benchmark. These can mention the domain, scope or source or the benchmark. Or might suggest the purpose of the benchmark i.e. to demonstrate a certain feature. ''List of categories''
+
'''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 [https://drive.google.com/file/d/0B-0CQ8SP0TYjMFVkU244ZXpUOHc/view?usp=sharing]
 +
 
 +
''Categories: Financial''
  
 
== Benchmark Data ==
 
== Benchmark Data ==
Line 5: Line 7:
 
=== The Trace Part ===
 
=== The Trace Part ===
  
−
Please upload your Java program to the server and include the necessary information (see rules document) here
+
The relevant files can be found on the server at: '''''filepath'''''
  
−
=== The Property Part ===
+
The script will run a scenario that '''''violates/satisfies''''' the property defined in the rest of this page.
  
−
See the rules for the necessary descriptions
+
== Instrumentation Information ==
 +
 
 +
We have defined the following pointcuts to capture the relevant events for this benchmark (see the next section for their use):
 +
 
 +
    pointcut openSession(UserSession us) :
 +
        call(public Integer UserSession.openSession() && target(us));
 +
 +
    pointcut closeSession(UserSession us) :
 +
        call(public void UserSession.closeSession() && target(us));
 +
 +
    pointcut log(UserSession us) :
 +
        call(public void UserSession.log(..) && target(us));
 +
 
 +
 
 +
 
 +
== Trace Statistics ==
 +
 
 +
 
 +
{| class="wikitable"
 +
|-
 +
! Event
 +
! Occurrences
 +
|-
 +
| openSession
 +
|
 +
|-
 +
| closeSession
 +
|
 +
|-
 +
| log
 +
|
 +
|-
 +
|}
 +
 
 +
=== The Property Part ===
  
 
==== Informal Description ====
 
==== Informal Description ====
 +
 +
Logging can only be made to an active session (i.e. between a login and a logout).
  
 
==== Demonstration Traces ====
 
==== Demonstration Traces ====
 +
 +
''Satisfying Traces''
 +
 +
* userDepositFromExternal<sup>999</sup>; userDepositFromExternal; reconcile
 +
 +
* userPayToExternal<sup>999</sup>; userPayToExternal; reconcile
 +
 +
* userPayToExternal [Verification.totalExternalTransferAttempts < 1000000]; userPayToExternal [Verification.totalExternalTransferAttempts >= 1000000]; reconcile
 +
 +
''Violating Traces''
 +
 +
* userDepositFromExternal<sup>999</sup>; userDepositFromExternal; userDepositFromExternal;
 +
 +
* userPayToExternal<sup>999</sup>; userPayToExternal; userDepositFromExternal;
 +
 +
* userPayToExternal [Verification.totalExternalTransferAttempts < 1000000]; userPayToExternal [Verification.totalExternalTransferAttempts >= 1000000]; userDepositFromExternal
  
 
==== 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].
 +
 +
    UserSession.openSession(..) target (UserSession s)
 +
          | -> { Verification.openSessions.add(s); }
 +
    UserSession.closeSession(..) target (UserSession s)
 +
          | -> { Verification.openSessions.remove(s); }
 +
    UserSession.log(..) target (UserSession s)
 +
          |  !Verification.openSessions.contains(s)
 +
          -> { Verification.fail("P10 violated"); }
 +
 +
 +
Note that we also make use of the static class ''Verification'' for keeping tracking of the open sessions. This can be used by any attempts to monitor for this property.
 +
 +
We can also specify a regular expression for traces that violate this property as follows:
 +
 +
    property foreach target (UserSession u) not matching{
 +
        (!openSession)*;(openSession;(!closeSession)*;closeSession)*;(!openSession)*;log
 +
    }
  
 
==== A FO-LTL Specification ====
 
==== A FO-LTL Specification ====

Revision as of 19:27, 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 openSession(UserSession us) : 
       call(public Integer UserSession.openSession() && target(us));

   pointcut closeSession(UserSession us) : 
       call(public void UserSession.closeSession() && target(us));

   pointcut log(UserSession us) : 
       call(public void UserSession.log(..) && target(us));


Trace Statistics

Event Occurrences
openSession
closeSession
log

The Property Part

Informal Description

Logging can only be made to an active session (i.e. between a login and a logout).

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

   UserSession.openSession(..) target (UserSession s) 
         | -> { Verification.openSessions.add(s); }
   UserSession.closeSession(..) target (UserSession s) 
         | -> { Verification.openSessions.remove(s); }
   UserSession.log(..) target (UserSession s)
         |  !Verification.openSessions.contains(s)
         -> { Verification.fail("P10 violated"); }


Note that we also make use of the static class Verification for keeping tracking of the open sessions. This can be used by any attempts to monitor for this property.

We can also specify a regular expression for traces that violate this property as follows: 

   property foreach target (UserSession u) not matching{
       (!openSession)*;(openSession;(!closeSession)*;closeSession)*;(!openSession)*;log
   }

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_Benchmark3&oldid=112"