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

Modeling the Distance Tracker Application 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)

  7. Reference implementation

This example was inspired by the group of Heiko Mantel. They invented a malicious distance tracker while we model a benign version. The distance tracker collects the user's GPS positions (for example while running) and uploads the covered distance (but not the actual positions) to a server after user confirmation.

Component Diagram






Message Diagram






Sequence Diagrams




Properties






Policy