-
Notifications
You must be signed in to change notification settings - Fork 2
/
README
41 lines (32 loc) · 1.35 KB
/
README
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
Symrob: timed automata model checker
==========
This is a prototype model checker reading a subset of Uppaal xml files
with the following features:
1) Basic zone-based model checking
2) Robust model checking algorithm of the following paper:
Ocan Sankur. Symbolic Quantitative Robustness Analysis of Timed Automata In TACAS'15 LNCS 9035, pages 484-498. Springer Berlin Heidelberg, 2015.
3) A counter-example guided abstraction refinement algorithm using BDDs (the CUDD library), described in the following paper:
Victor Roussanaly, Ocan Sankur and Nicolas Markey. Abstraction Refinement Algorithms for Timed Automata. CAV 2019.
To reproduce the results of this paper, please see the src/experiments/cav19/cav19-artifact directory.
Installation
============
All packages below are required and can be installed using opam:
- OCaml 4.0+
- ocamlbuild
- ocaml batteries included 2.2+
- xml-light
- mlcuddidl
Compilation
===========
1) Build and install uppaal_parser (make; make install)
2) Build symrob (make)
License
=============
Some of the examples in the src/experiments directory were taken from
the Verifix tool (http://satoss.uni.lu/members/piotr/verifix/)
by Piotr Kordy.
The license for symrob is GNU GPL 3.0
See the file LICENSE or https://www.gnu.org/licenses/gpl-3.0-standalone.html
Author and Contact
============================
Ocan Sankur <[email protected]>