[Impressum]
[Datenschutz]
[E-Mail]
[Back to the main project page]
Modeling a toy bank service with IFlow
- Component Diagram
- Sequence Diagram
- Properties
- Policy
- Message Diagram
- formal specification (proofs are contained in the Properties specification)
This example uses parameterized domains (every user has his own domain) and establishes that there
is no interference between different users (or different instances of the banking app).
This only works because of two reasons:
- The bank service always sends the answer back to the correct app.
- Handling the accounts is built in: The accounts are modeled as key-value lists with
the account number as key and the Account class as value, and every user has a different
account number. Therefore it is guaranteed that there is no interference between different
accounts. (There is no money transfer in this example.)
Component Diagram
Message Diagram
Sequence Diagrams
The user has two options: deposit money in the account (since this is a toy example there
is no `real' money involved, the account balance is simply increased), or withdraw money
from the account. This may fail if the balance is too low.
Properties
Source and sink are identical, but the domains are parameterized with User(a).
Implicitly the property means that the domain User(a) does not interfere User(b) for a unequal to b.
Policy
The User domain is parameterized with an identifier, i.e. User(a), and there is no interference
between different domains.
