Tarski in Action

Stories in Implementation Stories in Research Stories in State-of-the-Art

Introduction

In this work package, we introduce a new approach with its supporting platform which enables the user to interactively configure traceable elements and trace links. The specification is supported by formalizing the semantics of traceability in first-order relational logic in order to perform automated analysis such as consistency checking, reasoning on trace relations and trace element discovery. The usefulness of the approach is demonstrated in the context of application life-cycle platform in software industry and safety critical sofware development in automative industry and being tested in a use case in aviation industry.

For an example workspace, you can clone this source code repository Demonstrations and an example configuration file, you can directly get from HAVELSAN use case.

roject Poster presented in SAT/SMT/AR Summer School 2016

Type Hierarchy after loading an Alloy specification to the system (included several annotations)

Type Hierarchy

Management of first-order relational model

Management of first-order relational model

Assigning type to a unary relation while creating a trace element on a text file

Assigning type to a unary relation while creating a trace element on a text file

Selecting a binary relation to create link

Selecting a range from existing trace elements for the binary relation

Selecting a range from existing trace elements for the binary relation

Automated Analysis

Automated Analysis

Work Package Objectives (from the Final Project Propsal)

The primary objective of this WP is to provide the synchronization mechanism of the ModelWriter platform that will keep the user-visible models consistent with the KB-stored models and vice versa. This work package addresses all problems related to the “model-to-model transformations” in ModelWriter.

This mechanism will be based on model-to-model (M2M) transformations of two complementary categories:

Expected Results

An Eclipse-based M2M Transformation Framework, extensible so as to accommodate an increasing number of types of (user-visible) models. This will consist of the following main envisioned plug-in components:

Approach for the Work Package

The main goal of this WP is to develop a M2M Transformation Framework that supports the synchronization mechanisms for the ModelWriter tool.

These mechanisms will be based on a requirements synchronization framework that can be extended to support different requirements models (based on both textual and/or visual notations). The framework is made up of three main components:

  1. A meta-modelling infrastructure,
  2. A DSL for model transformation specifications, and
  3. A model synchronization API.

final version