This page includes accompanying material for the ASE20 paper "Scalable Multiple-View Analysis of Reactive Systems via Bidirectional Model Transformations", by Christos Tsigkanos, Nianyu Li, Zhi Jin, Zhenjiang Hu, and Carlo Ghezzi. In particular, one can find here tool support implementing the synchronizations, specifications and models presented in the paper, as well as an experiment reproduction kit. Tool support has been developed by Nianyu Li.

Preliminaries

We adopt the putback-based bidirectional programming language BiGUL, which is implemented as an embedded domain-specific language in Haskell. To use it, one has to be sure that they have the Haskell environment. It is recommended to install the Haskell Platform . BiGUL has been released to Hackage, and the latest version can be installed using Cabal in the usual way:

  cabal install BiGUL

The implementation of view generation and synchronization through bidirectional model transformations is available in the following link. Note that the implementation corresponds to Sections 4 and 5 of the paper.

Property-driven View Generation and Views Synchronization

Having installed BiGUL and the BX implementation we can run the commands below to generate views and propagate changes as described in the paper. We highlight the following workflow, to demonstrate the view-based reasoning advocated in the paper - the example refers to the case study presented.
  1. The source in the analysis experiment of our paper is city100.txt. The result.txt will record source and view, and the generated view will be stored in requirement1.txt and requirement2.txt accordingly.
  2. The designer who is analyzing the system under a specific viewpoint might decide to change part of the view model due to e.g., requirement violations found.
  3. Changes can be propagated to source. The updated source will be stored in city100.txt. File result.txt will record the original source, the view as well as the updated source information.

  >ghci BXRequirement1.hs    //entering the file dealing with view1
  >main_get_requirement1     //generating view1
  >main_put_requirement1     //updating source with changed view1
  >ghci BXRequirement2.hs    //entering the file dealing with view2
  >main_get_requirement2     //generating view2
  >main_put_requirement2     //updating source with changed view2

Experiment Setup

Source models used for the experiments are in CityGML format, representing three cities. The CityGML-to-bigraph step can be performed automatically and is out of the scope of the present paper: city1.citygml, city2.citygml and city3.citygml. Those correspond to the following bigraphical models, which are used for the experiments of Table 1 of the paper:

BRS Specification. Reactions reflect primitives of change in the system. The reactive system specification encodes rules for "dl" - sink downloads data from crossroad when colocated with a sensor containing a data token; "rs2cr" - sink moves from road segment to crossroad; 3) "cr2rs" - sink moves from crossroad to road segment; "locate" - UAV locates victim when it is near, "bg2bg" - UAV moves from building to building in the same block, and "bg2bg2" - UAV moves from building to building across city blocks. The rules specification is parametric utilizing the sites facility of the bigraphical formalism. Moreover, it uses variables that are rule-scoped, to predicate about the different port names occuring in the model.

The following syntax is used for specification:


  P | Q       Juxtaposition of nodes.
  $i          Site numbered i.
  K[w].(U)    Node with control K and ports with names in w. K contains U.
  @x          Port variable specification (locally scoped).
  R->R'       Reaction redex -> reactum.

Rules used are the following. Notice that variables range over names of Buildings (and Crossroads, RoadSegments etc). The UAV set of rules is considered for every UAV (4 in our case) and the WSN set of rules for each sink, so the actual ruleset is bigger.


  dl
    Road[@w].( Crossroad[@b].(Sensor.(DataToken) | Sink |$4)  |$3 )       |$9 ->
            Road[@w].( Crossroad[@b].(Sensor | Sink |$4)   |$3 )      |$9
  rs2cr
    Road[@w].( RoadSegment[@a].(Sink | Rs2Cr.(ConnCR[@b]|$1) |$5) | Crossroad[@b].(Cr2Rs.(ConnCR[@a]|$4)         |$3 ) | $2 ) |$9 ->
            Road[@w].( RoadSegment[@a].(Rs2Cr.(ConnCR[@b]|$1)         |$5) | Crossroad[@b].(Sink | Cr2Rs.(ConnCR[@a]|$4) |$3 ) | $2 ) |$9
  cr2rs
    Road[@w].( RoadSegment[@a].(Rs2Cr.(ConnCR[@b] |$1)         |$5) | Crossroad[@b].(Sink | Cr2Rs.(ConnCR[@a]|$4) |$3 ) | $2 ) |$9 ->
            Road[@w].( RoadSegment[@a].(Sink | Rs2Cr.(ConnCR[@b] |$1) |$5) | Crossroad[@b].(Cr2Rs.(ConnCR[@a]|$4)         |$3 ) | $2 ) |$9

  locate
    Block[@w].( Building[@b].(Victim | UAV |$4)  |$3 )       |$9 ->
            Block[@w].( Building[@b].(UAV |$4)   |$3 )      |$9
  bg2bg
    Block[@w].(Building[@a].(UAV | Bg2Bg.(ConnBB[@b]|$1) |$5) | Building[@b].( Bg2Bg.(ConnBB[@a]|$4)            |$3 ) | $2 ) |$9 ->
             Block[@w].(Building[@a].(Bg2Bg.(ConnBB[@b]|$1)         |$5) | Building[@b].(UAV | Bg2Bg.(ConnBB[@a]|$4)    |$3 ) | $2 ) |$9
  bg2bg2
    Block[@w].(Building[@a].(UAV | Bg2Bg.(ConnBB[@b]|$1) |$5) |$3 ) | Block[@another].( Building[@b].(Bg2Bg.(ConnBB[@a]|$4) |$8 ) |$11 ) |$9 ->
                      Block[@w].(Building[@a].(Bg2Bg.(ConnBB[@b]|$1) |$5) |$3 )  | Block[@another].(UAV | Building[@b].(Bg2Bg.(ConnBB[@a]|$4) |$8 ) |$11 ) |$9  

In WSN scenarios, a requirement captures correct data collection by data sinks.

   Property = " ⟡ (◻ ¬  DataToken)"
   PropTypes = {DataToken, Sensor, Sink, Crossroad, Road, RoadSegment, Rs2Cr, ConnCR,Cr2Rs}
   Rp = {"dl", "rs2cr", "cr2rs"}

In UAV scenarios a requirement ensures that victim are located by UAVs.

   Property = " ◻ (Victim → ⟡ ¬  Building_?.(Victim~|~-_0))"
   PropTypes = {UAV, Building,Victim, Block, Bg2Bg, ConnBB}
   Rp = {"locate", "bg2bg", "bg2bg2"}

Reproduction Kit

To reproduce the results of Table 1 in the paper, a VirtualBox image is provided. The program hosted inside will compute the dLTS's for the source and views of the first evaluation case presented in the paper. In principle, any tool can be used, as BRS interpretation is outside the scope of the paper. A mapping to Graph Transformation Systems could also be used.

The provided image can be imported to VirtualBox. When it is started, icons on the desktop can be used to run the experiments. Right click the icon and select 'Execute'. A terminal will open, running the experiment and interpreting the BRS (source or one of the views). Note that the dLTS models used in the paper take several minutes (or hours) to be calculated, and that due to the virtualization, performance timings will differ. After the interpretation, the dLTS model will be saved on the Desktop.

Resulting state-transition models produced can then be verified with explicit-state model checkers, e.g., SPOT, PRISM etc.