author: Casper Plentinger
title: GUI for FIG: Visualising simulation results
keywords: Statistical model checking, GUI, visualisation, front-end technology
topics: Creative , Other
committee: Raúl Monti ,
Carlos Esteban Budde
started: November 2019
end: January 2020

Description

Model checking marries the marvels of modern algorithms to the power and elegance of mathematics, allowing users of software tools to compute sound, complete, and exact properties of complex systems: smart grids, self-driving cars, satellites, you name it.

One tiny little detail though: the mad scientists who design these tools expect users to understand and specify models like this, where the best aid you can hope for is syntax highlighting. That right there is a power management system to switch the power-mode of a computer device (but you knew that from reading the file...)
To make matters worsebetter, the reply to a property query of those systems typically looks like this. That is telling us that in 100 time units (seconds), roughly 1 power-switch request is queued in the processing unit (elementary my dear Watson)

So, see, you may have something to do about that.

Final paper: https://drive.google.com/file/d/1XvOQRLMY_dwdmr_iN6Muva-8TPW2dd3k/view


Assignment

Design a GUI for fig, a Statistical Model Checker specialised in Rare Event Simulation.
Challenges include:

  • Choosing a suitable programming language and framework
    [ Python? Sure! C++? I dare you! Other? Convince me :p ]
  • Designing a look & fell that brings the best out of the tool
    • Model specification: graphical? textual?
    • Property queries: templates, parametrisation
    • Results display: scatter plots, performance bar plots
  • Implementing core (extensible) functionality of your creation
    [ Impress the world with the shiny outcome of your brainchild ]

Final paper: https://drive.google.com/file/d/1XvOQRLMY_dwdmr_iN6Muva-8TPW2dd3k/view

References

  1. Statistical Model Checking (survey) (Digital version available here)

Additional Resources

  1. SMC
  2. PRISM sp model
  3. PRISM output
  4. Scatter plot