Tool to provide a Excel-based frontend to configure and validate Real-Time system specified in UPPAAL.
Uppex is a tool that help to parameterizing and instantiating different UPPAAL models. UPPAAL is a widely used model-checking tool for real-time systems based on timed automata and CTL temporal logic.
Uppex uses: (1) an original UPPAAL model enriched with annotations and (2) a MS Excel file with configurations on how to instantiate the UPPAAL model. It produces instances of the original UPPAAL model, and if UPPAAL is installed it will also check if all available properties hold for their respective UPPAAL instance.

This tool is a contribution of VALU3S, and it improves the traditional usage of UPPAAL by facilitating its configuration when a family of models is desirable

José Proença, Sina Borrami, Jorge Sanchez de Nova, David Pereira, and Giann Spilere Nandi. "Verification of Multiple Models of a Safety-Critical Motor Controller in Railway Systems", in 4th International Conference, RSSRail 2022, Paris, France, June 1-2, 2022, Proceedings

Relationships with other web-repo artefacts
Improvement Classification
Reduced cost and time for work on certification process and functional safety
Open source - Goals
Safety, Functional Requirements

There are currently no items in this folder.