Modelling and Analysis of Normative Documents

John J. Camilleri, Gerardo Schneider.

This page accompanies our submission to the Journal of Logical and Algebraic Methods in Programming (JLAMP) special issue with the proceedings of the 27th Nordic Workshop on Programming Theory (NWPT 2015). It contains details about the case study and the source code for the back end of the system.

This source code is released under the GNU GPL License v3.0.

Last updated: 2016-09-19

Case study

Natural language text

Source: LeaseWeb USA Inc.

1.3 Customer may initiate a request for Standard Support via the technical helpdesk. A Support Request must include the following information: (i) type of service, (ii) details for contacting the Customer, and (iii) a clear description of Support required. Company may refuse a Support Request if it is unable to establish that the Support Request is made by an authorised person.

1.4 The table below sets forth the Response Time for any request for Support made in accordance with Section 1.3 above. The Response Time Target depends on the SLA level that the Customer has chosen.

SLA level Response time target
Basic24 hours
Bronze4 hours

1.5 In the event Company does not respond within the applicable Response Time Target, Customer shall be eligible to receive a Service Credit. If Customer does not pay a Monthly Recurring Charge then Customer shall not be eligible to any Response Time Credit.

1.6 Customer shall ensure that it will at all times be reachable on Customer's emergency numbers, specified in the Customer Details Form. No Credit shall be due if the Customer is not reachable. % on Customer’s emergency number.

Contract model and UPPAAL system

The model files used in this case study are as follows:

The output logs from the verification with UPPAAL are provided here: Full, Reduced

Usage

Compilation instructions

  1. Tested with GHC 7.8, 7.10. You may need to install some Haskell libraries, e.g. using cabal install.
  2. Download all the source code here (or browse it here).
  3. Compile everything with make all.

Translation to timed automata

Translation is from COML format (extended C-O diagram, as XML) to UPPAAL NTA (also XML). Usage is as follows: 

$ bin/comltouppaal leaseweb.coml leaseweb.xml
Parsed CO-XML file: leaseweb.coml
Wrote UPPAAL file: leaseweb.xml
You can then open the resulting XML file in the UPPAAL tool.

Syntactic query tool

We have a command-line tool for building and running syntactic queries on COML files. Usage is as follows: 

$ bin/comlquery leaseweb.coml
Then follow the prompts.