[Back to the main project page]
Modeling a Simple Search Service with IFlow
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
- Sequence Diagram
- Message Diagram
- formal specification (proofs are contained in the Properties specification)
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.