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

Modeling a Simple Search 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 search app). This only works because the search service always sends the answer back to the correct app. The implementation guarantees this.

Component Diagram

Message Diagram

Sequence Diagrams


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.