[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