uppaal

PyUPPAAL is a python package basically for reflecting UPPAAL's model editing, verification, and counter-example parsing operations into scripts.

LaTeX package to typeset Uppaal timed automata specifications

We propose in this work an approach for the verification of the AADL (Architecture and Analysis Design Language) description. This approach is based in Model Driven Engineering (MDE) and assisted by a toolchain. Indeed, we define a source meta-model for AADL and a target meta-model for the timed automata formalism; we define a transformation proces…

The project set out to showcase real time strategy generation using UPPAAL Stratego for a highly dynamic environment like robocup. This project was created as a bachelors project at Aalborg University. Alongside the program a paper was created and can found in this project.

Property Specification Patterns for UPPAAL

TARTS is a tool to auto generate code for a embedded system by an UPPAAL timed automaton

Official repository for the bachelor thesis "Learning UPPAAL Timed Automata from Network Protocol Traces"

A software program that translates XML-based code into executable python codes.

This repo contains the official UPPAAL documentation published on https://docs.uppaal.org

This repository constitutes the modelling baseline for the WP2 of the PerformingRail EU project.

Visualizing Behavior of Distributed Network Protocols using UPPAAL Simulations

Model Checking For Automated Machine Learning Models

Formal Methods for Concurrent and Real-Time Systems a.y. 23/24 - Homework Project

Homework project developed in the course FORMAL METHODS FOR CONCURRENT AND REAL-TIME SYSTEMS (now FORMAL METHODS FOR SOFTWARE ENGINEERING) of Politecnico di Milano during the academic year 2024/2025. Mark: 30 cum laude

Verification Project @ ENSTA Bretagne

Formula 1 pit stop modelled with Uppaal/Tiga

Final project of the course Formal Methods for Concurrent and Real-Time Systems at Politecnico di Milano

A simple global clock example in UPPAAL.

Switchable stochastic timed automata model of supply chain resilience in UPPAAL SMC, with an automated PRMM maturity-scoring toolchain.

A programming language for Arduino controllers, using UPPAAL for time verification.