Skip to main content
University of Oxford Department of Computer Science
  Contact Us     Search  
  1. Home
  2. Our Students
  3. Online Resources, Handbooks & Library
  4. Student projects - Development of software for the verification of MPL models

Development of software for the verification of MPL models

Supervisor

Alessandro Abate

Suitable for

MSc in Advanced Computer Science
Computer Science, Part C

Abstract

This project is targeted to enhance the software tollbox VeriSiMPL (''very simple''), which has been developed to enable the abstraction of Max-Plus-Linear (MPL) models. MPL models are specified in MATLAB, and abstracted to Labeled Transition Systems (LTS). The LTS abstraction is formally put in relationship with its MPL counterpart via a (bi)simulation relation. The abstraction procedure runs in MATLAB and leverages sparse representations, fast manipulations based on vector calculus, and optimized data structures such as Difference-Bound Matrices. LTS can be pictorially represented via the Graphviz tool and exported to PROMELA language. This enables the verification of MPL models against temporal specifications within the SPIN model checker.

Courses: Computer-Aided Formal Verification, Numerical Solution of Differential Equations

Prerequisites: Some familiarity with dynamical systems, working knowledge of MATLAB and C

Our Students

Back to Top