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

Modeling the Distance Tracker Application with a complex filter function with IFlow

  1. Component Diagram

  2. Sequence Diagram

  3. Properties

  4. Policy

  5. Message Diagram

  6. Filter function calcDist (computes the distance from a list of GPS positions, uses the Haversine formula)

  7. formal specification (proofs for the filter function are contained in the filterProperties specification, the main theorem is Main-property)

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






Filter function calcDist and auxiliary functions