ProTL (Probabilistic-CCSL TransLator) is a tool that provides a push-button transformation from PrCCSL* (probabilistic extension of clock constraint specification language) specifications to UPPAAL-SMC models (stored in .xml files), and provides the support for formal analysis of requirements specified as probabilistic temporal and casual constraints in PrCCSL*.
23 May 2019
New features of ProTL version 3.1 compared to ProTL version 3.1 includes:
1. Support specifications of relations among multiple clocks, called n-ary relations;
2. Support translation of n-ary relations into STA;
3. Generate counter-example for violated n-ary clock relations;
22 Mar 2019
New features of ProTL version 3.0 compared to ProTL version 2.0 includes:
1. Support for analysis of clock action, probabilistic clock action and interval-based delayFor operator;
2. Allowing users to edit/embed C code in the input PrCCSL* specifications;
3. Refining the translation pattern of ITE expression;
4. Support for comment block.
15 Jan 2019
New features of ProTL version 2.0 compared to ProTL version 1.0 includes:
1. Generation of full set of probabilistic queries;
2. Support for conductig veirifcation/simulation is provided, which allows users to perform formal analysis on PrCCSL specifications using ProTL directly.
3. Automatic generation of UPPAAL-SMC models of keyword DenseClockType, which is used to define new dense clock types for specification of continuous dynamic behaviors (e.g., energy consumption, temperature variation) described by Ordinary Differential Equations (ODE);
4. Based on the verification results, the correctness/incorrectness of requirements can be traced back to corresponding PrCCSL specifications and counter-examples are generated for diagnosis information and further refinement of PrCCSL specifications.
5. Visualization of verification results, e.g., simulation graph, time, CPU, Memory etc.
6. The verification efficiency is improved by 40%-50%.
19 Nov 2018
ProTL version 1.0 supports:
1. Automatic translation from PrCCSL specifications into UPPAAL-SMC models for formal verification;
2. Generation of three types of probabilistic queries: Hypothesis Testing, Probability Estimation, Simulation.
If you have comments or questions on our tool, you can contact any of us: