modelwriter / wp3 Goto Github PK

View Code? Open in Web Editor NEW

4.0 9.0 1.0 182.45 MB

A Platform for Automated Analysis of Traceability (WP3)

Home Page: https://modelwriter.github.io/WP3/

License: Eclipse Public License 1.0

Java 94.36% Alloy 4.63% Lex 0.25% Shell 0.06% ANTLR 0.48% CSS 0.19% JavaScript 0.03%

automated-analysis emf traceability alloy kodkod z verification

wp3's Introduction

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.

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

Management of first-order relational model

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

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.

By user-visible models is meant those models that have been explicitly created by a Technical Author, using e.g. a spreadsheet, a kind of UML diagram, a block diagram, a mind map, etc. or any modelling tool (part of the “Model” side of ModelWriter) he has found the most appropriate for authoring his technical information.
By KB-stored model is meant a part of the Knowledge Base devoted to storing pieces of related information, disregarding whether it is represented in user-visible models, in natural-language documents, or in both.

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

WP3.1, for transforming a user-visible model to a KB-stored model (this "mirrors" WP2.1).
WP3.2, for transforming a KB-stored model into a user-visible model (this "mirrors" WP2.2).

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:

Transformation Manager: provides the infrastructure to register and launch transformations.
Configuration Manager: for personalizing the behaviour of the framework to meet the needs of a specific standard / organization / project / individual.
Traceability Manage: keeps links between elements of user-visible models and elements of the KB.
Synchronization Manager: triggering transformations when synchronization is needed.

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:

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

final version

wp3's People

Contributors

Stargazers

Watchers

Forkers

waffle-iron

wp3's Issues

Investigate Java Collection Package in the context of sets and lists

It is important to approximate ECore Type System with Java Types while translating into Java compilation units.

Transformation of Ecore Models into Java Compilation Units for type checking and various semantic errors of language constructs

This may provide us a way of semantic analysis of types, generic types and type parameters. We can promote stringtemplate to generate a Java program files from AlloyInEcore AST.

We will exploit the Java Compiler Interface in javax.tools. The approach that I propose is to transform each class type constructs into interface and employ the java's type inheritance mechanism using interfaces to simulate state inheritance of ECore or MOF. To enable this approach, every structural elements should be rephrased as methods (getters and setters); every nested package definitions are flattened, and each class definition are converted into a compilation unit.

Investigate the possibility of using the type system of Z formal specification language (Spivey's Z).

http://spivey.oriel.ox.ac.uk/mike/zrm/
http://usingz.com/

The fuzz type-checker for Z (2008)
https://bitbucket.org/Spivey/fuzz

https://en.wikipedia.org/wiki/Z_notation
Typechecking Z (2000)

Implement a first version for KodKod Interpretation of ECore Models and Instances

Test Backlog #2: ..

Examine Java Interactive Visualization Environment (JIVE)

http://www.cse.buffalo.edu/jive/

Save a textually defined instance as an ECore instance

Test

Test

Add a context menu item for each element to delete the associated context from the program.

Highlight 'super' keyword in type parameters of class definitions

Test Backlog #1: Collect requirements (user stories) for each use case

please define ...

Improve folding algorithm.

The editor sometimes becomes unstable.

When Ecore is closed without saving action, markers don't revert to old version

Integrate Tarski Visualization panel with AlloyInEcore Instance editor

Closing the visibility of markers

there must be syntax highlighting scheme for keywords of formulas and expressions.

Go to declaration of an element defined in another resource

Double click on an element in the content outline page or click on the context menu of an item on the content outline page fires this action.

When markers are deleted in MarkerView, ProjectExplorer doesn't refresh

Resolve Variables and Relations while parsing using semantic predicates of ANTLR

Algorithm: If a variable is defined in a quantifier, comprehension or let declaration, semantically resolve all identifiers with the same name as variables in the scope of that declaration. Resolve other identifiers in the scope as relations. This approach maintains a good approximation for a semantically valid parse tree since the variables are always declared before using them. Variables may shadow each other, and may shadow field names. Conventional lexical scoping, with the innermost binding taking precedence.

Create a fast fuzzy parser for instance declarations

Test Backlog #3: ...

.... bla bla

Resolve names using the namespace approach that OMG proposed or using JAVA approach

Test Task

ferhat

Test Backlog #4

CountMarkersForFile will be added to Command

Preserve the order of EModelElements while translating them into textual format using possibly ETreeIterator

EcoreTranslator: order of features in a class should be as such EAttribute, EReference and EOperation

Formalize 'subsets' and 'redefines' qualifiers using Ecore annotations. Provide an abstract syntax and concrete syntax appropriately.

{subsets <EReference>}
{redefines <EReference>}

Transformation of Ecore Models into Java Compilation Units using Eclipse JDT (Java Development Tools) to get warnings such as unused types besides type checking and detecting various semantic errors of language constructs

Assess the feasibility and benefits of encoding UML 2.5 abstract syntax and semantics in AlloyInEcore to generate the java implementation automatically.

We can use the UML.xmi and the UML2.x API of Eclipse to generate our own API in which we develop concrete representations of data types from the specification. In fact, this approach also enables us to verify the UML2.5.

Translating between Alloy specifications and UML class diagrams annotated with OCL (SoSym) - 2015

Move ECore and EObject translators to Core project with JUnit tests.

Examine Java Pathfinder (JPF) project of NASA for verification of Java programs.

JPF is a highly customizable execution environment for verification of Java™ bytecode programs

http://babelfish.arc.nasa.gov/trac/jpf

https://en.wikipedia.org/wiki/Java_Pathfinder

Unnecessary dependencies

- 'plugin name'

* 'dependencies that will be removed'

- eu.modelwriter.marker.startup

* org.eclipse.mylyn.wikitext.tests,

* org.eclipse.mylyn.wikitext.markdown.core

-> We have EcoreDropAdapter class to connect IDragAndDropService on startup.
In this class, we are using MarkdownParser to parse markdown text, and it creates dependency on plugins above.

- eu.modelwriter.marker

* org.eclipse.mylyn.wikitext.core

-> In this project, we have MarkdownToReqIfDocumentBuilder which extends org.eclipse.mylyn.wikitext.core.DocumentBuilder

- eu.modelwriter.marker.command

* org.eclipse.mylyn.wikitext.core,

* org.eclipse.mylyn.wikitext.markdown.core.

-> In this project, we have CreateReqifSpecFromMarkdownHandler class. If this handler is triggered, we are creating MarkdownParser instance, setting its document builder as MarkdownToReqIfDocumentBuilder, and running its parser.

In conclusion,

-> Maybe we should create our own parser or any other alternative.

Improve Document Lifecycle in terms of Save Operation

Save operations must preserve the layout of the programs unless it is updated outside the user's editor.

Notify errors of name collisions in the namespace hierarchy

When parent has been removed, check children and if there is a marker, remove it.

Check the first TreeSelection in ChangeListener for first changing

Check whether an instance conforms to its model without using ECore

Add markertype to exist marker

Transformation of Ecore Models and Constraints into Alloy Specifications for type checking and various semantic errors of expressions and formulas

CD2Alloy website
CD2Alloy-- Class Diagrams Analysis Using Alloy Revisited (MODELS) - 2011
On challenges of model transformation from UML to Alloy (SoSym) - 2010
UML2Alloy-- A Challenging Model Transformation (MODELS) - 2007
Translating between Alloy specifications and UML class diagrams annotated with OCL (SoSym) - 2015
From UML and OCL to Relational Logic and Back (MODELS) - 2012

Auto-complete incomplete words when pressed C+space (actually it works when empty)

    abstract class Shape extends Geometry
    {
        attribute Type : Shape| [?];
    }

    enum ShapeType
    {
        literal Arc = 0;
        literal Oval = 1;
        literal Rectangle = 2;
    }

Translation of AlloyInEcore models to Z Specification Language using CZT Corejava

CZT Corejava of CZT: Community Z Tools for developing and reasoning about Z specifications

Corejava is part of the CZT project that aims at providing a framework for building formal methods tools, especially for the Z specification language. This subproject provides AST (Annotated Syntax Tree) classes for Z and its extensions, written in Java.

Translating Z to Alloy
https://sourceforge.net/p/czt/code/ci/master/tree/z2alloy/

Add a context menu item for each slot of an eObject or an eObject on Content Outline of Instance Editor to create the associated context on the program

try to implement without using ECore API

If a model is declared for an instance, resolve the class of each eObject and show in the content outline page

Improve Numeric Parsing Algorithm as similar shown in the followings

NUMBER
          '-'? INT'.'INT EXP? //1.35,1.35E-9,0.3,-4.5
	| '-'? INT EXP //1e10-3e4
	| '-'? INT //-3,45
	;

	fragment INT: '0'|[1-9][0-9]*;  //noleadingzeros
	fragment EXP: [Ee][+\-]? INT;

Prepare D3.2.1 M2M Transformation Framework architectural design document

ModelWriter/Deliverables#34

Keywords such as Class, Enum are not mapped to corresponding tokens

/generics/Shape.java:3: error: duplicate class: generics.Shape
enum Shape
^ 
Mapped to:

/generics/Shape.java:8: error: duplicate class: generics.Shape
interface Shape<V>
^ 
Mapped to: