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

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

- Component Diagram
- Sequence Diagram
- Properties
- Policy
- Message Diagram
- Filter function calcDist (computes the distance from a list of GPS positions, uses the Haversine formula)
- 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