Specification Synthesis for Deontic Input-Output Automata

This page contains supplementary material to our paper:

E. Letier and W. Heaven, Requirements Modelling by Synthesis of Deontic Input-Output Automata, Proc. 35th International Conference on Software Engineering 2013 (ICSE 2013).

The following zipped file contains a version of LTSA extended to perform specfication synthesis over deontic IO LTS.
ltsa-ctrl.zip

Unizipping the file generates a folder containing the following files:

LTSA-Synthesis.jar -- a prototype extension of LTSA for synthesis of deontic IO LTS
SimpleExample.lts -- a small example showing the syntax of the commands to use to perfrom specification synthesis
tv-controller.lts -- the models for the TV control systems used as example in the paper
Turnstile.lts -- specification syntesis applied to the classic zoo trunstile problem of Jackson and Zave ICSE 95 paper
MinePump - original LTSA demo.lts -- spec synthesis applied to the classic mine pump problem as specified in the LTSA demo model
MinePump - abstract version.lts -- spec synthesis for a more abstract version of the mine pump problem
Proton Therapy-Logging.lts -- spec synthesis for the logging problem of a radiation therapy system by Robert Seater, Daniel Jackson, and Rohit Gheyi
Proton Therapy-Radiation Delivery.lts -- spec synthesis for the radiation delivery problem for the same radiation therapy system

There's no user manual. The above examples show the new LTSA commands to use to generate the weakest deontic IO LTS realising a goal in a domain as described in the paper. Use of our extension assumes familiarity with LTSA.

Acknowledgement

LTSA is a tool developed by Jeff Kramer and Jeff Magee's group at Imperial College London. The standard version of the tool is available here.
http://www.doc.ic.ac.uk/~jnm/book/