Uppex

Tool to provide a Excel-based frontend to configure and validate Real-Time system specified in UPPAAL.

Logo

Main partner/Developer Tool developer

Tool Link Link to website/github (URL) with more detailed information (optional)

Tool partners Non-owner organizations associated with the tool (partners/distributors)

Improved/Developed Tool Select if it is a new tool (developed) or an improved tool

Tool description A detailed description of the tool

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.

Technical toolchains Technical connection of tools with their supporting tools. Example: for running a specific tool, you need to run/install this other tool(s) (e.g., CHESS-FLA CHESS, MoMuT Enterprise Architect, etc)

Description of the improvements Description of the improvements and novelties added during VALU3S/Baseline

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

Improvement date

New Improvements To be filled in the future (after VALU3S)

References Related papers, journals, articles, and so on

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

Related V&V Methods A tool could be based on several V&V methods.

Standards A method can be linked with standards.

Use cases Use cases where the tool has been used

Functional Toolchain Functional connection of tools for the implementation of a specific evaluation scenario/workflow. Example: the output of one tool can be used by the other tool(s) in order to obtain a different information (e.g., CIROS FERAL, MARVER >-> SRVT, etc)

Improvement Classification

Evaluation Criteria for Safety, Cybersecurity, and Privacy (SCP)

Evaluation Criteria for V&V Processes

Open source - Goals

open Source

Goals Tool goals

Contents

There are currently no items in this folder.