[Impressum] [Datenschutz] [E-Mail] [Back to the main project page]

Modeling a toy bank service with IFlow

  1. Component Diagram

  2. Sequence Diagram

  3. Properties

  4. Policy

  5. Message Diagram

  6. 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:

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.


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.


The User domain is parameterized with an identifier, i.e. User(a), and there is no interference between different domains.