Difference between revisions of "Java Team2 Benchmark1"
(→The Trace Part) |
(→The Trace Part) |
||
| Line 7: | Line 7: | ||
=== The Trace Part === | === The Trace Part === | ||
| − | The relevant files can be found on the server at: '' | + | 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. | The script will run a scenario that '''violates''' the property defined in the rest of this page. | ||
Revision as of 17:18, 3 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
Contents
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(String account_number, double amount) :
call(public void UserInfo.depositTo(String, double)) && args(uid, account_number, amount);
Trace Statistics
| Event | Occurrences |
|---|---|
| greylistUser | 1 |
| whitelistUser | 1 |
| depositTo | 2 |
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
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
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.
