/actario

Verification Framework for Actor Systems on Coq

Primary LanguageOCamlGNU Lesser General Public License v2.1LGPL-2.1

logo Actario

wercker status

Actario is a framework to formalize and verify Actor systems on Coq. This project is under development.

Actario = Actor + Scenario

Requirements

  • coq-8.8
  • mathcomp-1.7

Install

$ cd /path/to/actario
$ ./configure
$ make
$ make install

Examples

See examples.

Current status

  • Formalization of Actor model's syntax and semantics
    • syntax: new, send, self, become (theories/syntax.v, actions)
    • semantics: labelled transition semantics (theories/semantics.v, trans)
  • Convenient notation
    • theories/syntax.v
  • Proof of no duplication of Actor names
    • theories/trans_invariant.v (initial_trans_star_no_dup)
  • Mechanisms/Lemmas for verifying Actor systems
  • Communication between configurations
  • Extraction to Erlang
    • Equivalence between Actario's semantics and Erlang's semantics is not proven
  • Supervisor
  • Practical examples

License

LGPL 2.1

Papers