Bachelor and Master Theses
To apply for conducting this thesis, please contact the thesis supervisor(s).
| Title: | Formal Verification and Validation of the Flow Management System of Automated Construction Machines |
| Subject: | Computer science, Embedded systems, Software engineering |
| Level: | Advanced |
| Description: |
Volvo CE (VCE) simulators at MDH can simulate construction machines working in different environments and they are originally used to train operators. Later, VCE simulators were used to test, validate, and demonstrate the applicability of different control and mission planning algorithms in production sites [1]. However, there is a need to formally verify these algorithms in order to ensure their dependability. Model checkers are suitable tools that can be used to formally verify models against formal properties. Rebeca (Reactive Objects Language) is an open-source actor-based modelling language with a supported model checking toolset that is used to model distributed and concurrent systems with timing constraints [2]. Using Timed Rebeca, we can model the dynamic behaviour and timing properties of the system. Moreover, AdaptiveFlow framework is a Rebeca-based framework for modelling and analysing track-based flow management systems [3]. In a previous master thesis [4], the student developed the VMAP tool that maps the models designed and verified in the AdaptiveFlow to scenarios in the VCE simulator. However, the mapping is not fully automated and there is a need to map the VCE scenarios (which are not necessarily track-based scenarios) to AdaptiveFlow. The objectives of this master thesis are: • Develop a mapping tool for the VCE scenarios to AdaptiveFlow. • Fully automate the VMAP tool. • Prove the applicability of the developed tools on a real VCE scenario. References [1] Muhammad Atif Javed, Faiz Ul Muram, Anas Fattouh, Sasikumar Punnekkat “Enforcing Geofences for Managing Automated Transportation Risks in Production Sites”, Workshop on Dynamic Risk Management for Autonomous Systems (2020). [2] Marjan Sirjani: Rebeca: Theory, Applications, and Tools. FMCO 2006: 102-126. [3] Giorgio Forcina, Ehsan Khamespanah, Ali Jafari, Ali Sedaghatbaf, Stephan Baumgart, Marjan Sirjani “AdaptiveFlow: An Actor-based Eulerian Framework for Track-based Flow Management”, Technical Report (2018). [4] Pavle Mrvaljevic “Tool Orchestration for Modeling, Verification and Analysis of Collaborating Autonomous Machines”, Master Thesis (2020). Supervisor(s): Marjan Sirjani and Anas Fattouh Examiner: Sasikumar Punnekkat |
| Start date: | |
| End date: | |
| Prerequisites: | |
| IDT supervisors: | |
| Examiner: | |
| Comments: | |
| Company contact: |