Reactive synthesis from Promela
Ioannis Filippidis, Richard Murray, Gerard Holzmann

Citation
Ioannis Filippidis, Richard Murray, Gerard Holzmann. "Reactive synthesis from Promela". Talk or presentation, 29, October, 2014.

Abstract
This work extends the modeling language Promela for describing constraints on the behavior of systems reacting to an adversarial environment, together with assumptions on the environment. The aim is to develop an input formalism for temporal logic synthesis tools that is more practical to use and scales better than other existing approaches, as for example directly writing logic formulas or defining graph structures. Promela is an imperative programming language used for verification of closed systems that can represent non-determinism. We extend it in two main directions, by introducing the notions of controllability for variables and integrating imperative with declarative semantics. Uncontrollable processes and variables are used to model assumptions about the environment. Imperative semantics reduce the amount of constraints that need to be explicitly expressed when writing a model. Selected variables can be declared as free for the synthesis tool to specify their behavior, so as to satisfy the given specification. Similarly, non-determinism inside controlled processes can be resolved during synthesis. As a result, open reactive systems can be represented in Promela. The implementation is written in Python and comprises of a Promela parser and translation backend to temporal logic formats accepted by existing Generalized Reactivity-1 synthesis tools.

Electronic downloads

Internal. This publication has been marked by the author for TerraSwarm-only distribution, so electronic downloads are not available without logging in.

Citation formats

• HTML

  Ioannis Filippidis, Richard Murray, Gerard Holzmann. <a
  href="http://www.terraswarm.org/pubs/410.html"
  ><i>Reactive synthesis from
  Promela</i></a>, Talk or presentation,  29,
  October, 2014.

• Plain text

  Ioannis Filippidis, Richard Murray, Gerard Holzmann.
  "Reactive synthesis from Promela". Talk or
  presentation,  29, October, 2014.

• BibTeX

  @presentation{FilippidisMurrayHolzmann14_ReactiveSynthesisFromPromela,
      author = {Ioannis Filippidis and Richard Murray and Gerard
                Holzmann},
      title = {Reactive synthesis from Promela},
      day = {29},
      month = {October},
      year = {2014},
      abstract = {This work extends the modeling language Promela
                for describing constraints on the behavior of
                systems reacting to an adversarial environment,
                together with assumptions on the environment. The
                aim is to develop an input formalism for temporal
                logic synthesis tools that is more practical to
                use and scales better than other existing
                approaches, as for example directly writing logic
                formulas or defining graph structures. Promela is
                an imperative programming language used for
                verification of closed systems that can represent
                non-determinism. We extend it in two main
                directions, by introducing the notions of
                controllability for variables and integrating
                imperative with declarative semantics.
                Uncontrollable processes and variables are used to
                model assumptions about the environment.
                Imperative semantics reduce the amount of
                constraints that need to be explicitly expressed
                when writing a model. Selected variables can be
                declared as free for the synthesis tool to specify
                their behavior, so as to satisfy the given
                specification. Similarly, non-determinism inside
                controlled processes can be resolved during
                synthesis. As a result, open reactive systems can
                be represented in Promela. The implementation is
                written in Python and comprises of a Promela
                parser and translation backend to temporal logic
                formats accepted by existing Generalized
                Reactivity-1 synthesis tools.},
      URL = {http://terraswarm.org/pubs/410.html}
  }
  

Posted by Ioannis Filippidis on 28 Oct 2014.
Groups: tools