Quasimodo Tool Components

The following is a list of tools and tool components that have been developed or extended in Quasimodo (Countinously Updated)

Overview of Quasimodo Tools
Tool Description
MoToR Tool Environment for MoDeST, the Modeling and Description Language for Stochastic and Timed Systems
MRMC Model-checker for discrete-time and continuous-time Markov Reward Models
MCPTA Probabilistic Timed Automata model checker for MoDeST - maps on PRISM
PASS CEGAR model checker for infinite-state probabilistic models, MDPs
INFAMY CSL Model Checker for infinite-state Markov chains - CTMCs
PARAM Reachability probability computation for parametric Markov chains - DTMCs
TorX, JTorX Testing tool for conformance testing of reactive software
TorXakis Symbolic (data) testing based on the formalism of Symbolic Transition Systems.
Uppaal Tool Suite
  • Uppaal  Model-Checker (Editor, Modelling, Simulation, Verification of Timed Automata)
  • Uppaal-TIGA (Uppaal branch for solving timed games, controller synthesis, robustness check, refinement check)
  • Uppaal-TRON (Uppaal branch for Testing Real-time Systems Online)
  • Uppaal-CORA (Uppaal Branch for Cost Optimal Reachability Analysis)
  • Uppaal-PRO (Uppaal branch which supports probabilistic reachability for probabilistic timed automata)
  • Uppaal-TIGA-Interface:  version of Uppaal-TIGA implementing the timed interface theory
    •
    FORTUNA Model checker (cost-bound maximal probabilistic reachability) for priced probabilistic timed automata
    P2J Promela-to-java compiler
    SARTS Schedulability analysis of Safety Critical Hard Real-Time Java
    Metamoc WCET Analysis of ARM Processors using Real-Time model-checking
    Ygdrasil Translator for a (subset) of UML to Uppaal-Timed automata  - intended for test generation.
      Timen Automata Templates for Schedulability Analysis
    libalf A comprehensive, open-source library for learning finite-state automata.