Skip to content

Latest commit

 

History

History

code

README.md

This is the artifact for paper "Automated Verification for Real-Time Systems via Implicit Clocks and an Extended Antimirov Algorithm"

Automated Timed Temporal Verification

The correctness of real-time systems depends both on the correct functionalities and the realtime constraints. To go beyond the existing Timed Automata based techniques, we propose a novel solution that integrates a modular Hoare-style forward verifier with a term rewriting system (TRS) on Timed Effects (TimEffs). The main purposes are to increase the expressiveness, dynamically create clocks, and efficiently solve constraints on the clocks. We formally define a core language Ct, generalizing the real-time systems, modeled using mutable variables and timed behavioral patterns, such as delay, timeout, interrupt, deadline. Secondly, to capture real-time specifications, we introduce TimEffs, a new effects logic, that extends regular expressions with dependent values and arithmetic constraints. Thirdly, the forward verifier reasons tempo- ral behaviors – expressed in TimEffs – of target C^t programs. Lastly, we present a purely algebraic TRS, i.e., an extended Antimirov algorithm, to efficiently prove language inclusions between TimEffs. To demonstrate the feasibility of our proposals, we prototype the verification system; prove its soundness; report on case studies and experimental results.

Build from source (tested on Ubuntu 18)

  • Dependencies:

Install opam: (cf. https://opam.ocaml.org/doc/Install.html)

sudo apt install git
sudo apt install curl
bash -c "sh <(curl -fsSL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh)"
opam init
sudo apt install make 
sudo apt install gcc

Install ocaml and libraries:

opam switch create 4.13.1
eval $(opam env)
opam install menhir

Install z3 and dune:

opam init
eval `opam config env`
opam update
opam switch create 4.13.1
eval `opam config env`
opam install z3
sudo apt-get install whitedune
  • Get the source code and build
https://github.com/songyahui/AlgebraicEffect
cd AlgebraicEffect 
eval $(opam env)

Examples:

Program Verification

cd code 
dune exec ./Forward.exe src/Validation/1_delay.c

To Clean:

dune clean

Benchmark:

Our benchmark contains three folders:

  • Validation: We manually annotate TimEffs specifications for a set of synthetic examples (for about 54 programs), to test the main contributions, including: computing effects from symbolic timed programs written in C t ; and the inclusion checking for TimEffs with the parallel composition, blok waiting operator and shared global variables.

  • Experiment1: For 16 C^t programs8, and the annotated temporal specifications are in a 1:1 ratio for succeeded/failed cases. We record the evaluation results in Table 3 in the paper

  • Experiment12: comparison with the PAT [16] model checker using real-life Fischer’s mutual exclusion algorithm.