Multi Domain Development guide

1. Multi Domain Specification

Multidomain Specification is supported via the AssetBasedSystem (ABS) language.

1.1. ABS Metamodel

1.1.1. Overview

The AssetBasedSystem language is defined in fr.irisa.atsyra.absystem.model

Figure 1. ATSyRA ABS specification Model plugins

An AssetBasedSystem defines 5 main sets of elements:

UserDomain : define the accepted concepts allowed in the user model.
UserModel : the model contain the assets of the user.
Behavior : the behavior of the domain.
Contracts : static and dynamic contracts that the model should consider.
Goal : definition of scenario the user whant the ensure or prevent on his model.

The top of figure ABS Main class diagram shows the main concepts of UserDomain: AssetType, AssetTypeAspect, AssetTypeAtribute, AssetTypeReference.

The bottom of figure ABS Main class diagram shows the main concept of the UserModel: Asset, AssetLink, AssetAttributeValue

Figure 2. ABS Main class diagram

Figure ABS GuardedActionDefinition class diagram shows that a GuardedAction uses parameters and is mainly composed of a guard (Expression) and an Action.

Figure 3. ABS GuardedActionDefinition class diagram

Figure ABS Contract class diagram shows that similarly to GuardedAction, a Contract uses parameters and is mainly composed of an Expression.

Figure 4. ABS Contract class diagram

Figure ABS Contract class diagram shows that a GuardedAction is mainly composed of a precondition and a postcondition Expressions.

Figure 5. ABS Goal class diagram

1.1.2. ABS Expressions

In the metamodel, Expressions are defined in a generic way, but additional constraints restricts what kind of Expression can exists, so that Expressions are properly typed.

Preliminary

In this section, we introduce concepts that refers to elements present in the ABS metamodel, but are more concise and more convenient to handle ABS models.

We may use shorter versions of the name of some elements when there is no ambiguity. For example, feature instead of AssetTypeFeature, reference instead of AssetTypeReference. We will however not shorten AssetType, since we also consider other notions of types, which we will define in the next section.

We say that a feature is a simple feature if its multiplicity is either One or ZeroOrOne. Similarly, we say that a feature is a collection feature if its multiplicity is either OneOrMany or ZeroOrMany.

The container type of a feature is the AssetType that either contains directly the feature, of that is aspectized by the AssetTypeAspect containing the feature. For example, if the feature "location" is contained in an AssetTypeAspect of "Attacker", then the AssetType "Attacker" is the container type of "location".

Given an AssetType T, the subtypes are defined recursively: T is a subtype of itself, and any type that extends a subtype of T is also a subtype of T. Supertypes of T are all types T' such that T is a subtype of T'.

We define MemberType to be a type that can be either an AssetType or a PrimitiveDataType. For the sake of simplicity, we extends the notion of subtype and supertype to MemberTypes, by saying that each PrimitiveDataType has a single subtype and a single supertype, which is itself. We refer as the MemberType of a feature (or the type of a feature i, short) for either its referenceType is the feature is a reference, or its attributeType if the feature is an attribute.

Typed expressions

Originally, ABS do not define types for Expressions. But in practice, depending on the context, an expression may be expected to be of a certain type. For example, an Expression in a guard is expected to be Boolean, and an Expression on the left of an assign is expected to refer to some simple feature of a given asset.

Depending of the context, a single Expression can be interpreted as of different types, but some Expression can never be interpreted of a given type.

In the rest of the section, we define the following types of Expressions: Boolean Expression, Value Expression, AssetRef Expression, FeatureRef Expression, Collection Expression and CollectionRef Expression.

In addition to Expression types, Value Expressions and Collection Expressions can also be typed with either an AssetType or a PrimitiveDataType. Thus, Value Expression (resp. Collection Expression) does not refer to a single type of Expression, but to the set of Value Expressions of all types (resp. the set of Collection Expressions of all types). The types of Value Expressions and Collection Expression ranges over all AssetTypes, all PrimitiveDataTypes, and the null type (which is the type that only has the constant expression "undefined").

Boolean Expressions are Expressions that evaluate to a Boolean value. Boolean Expressions are also Value Expressions, since Boolean is also a PrimitiveDataType in ABS, but they are also used where Boolean logic is needed, for example in guards or in filters. Boolean Expression are of the form:

Boolean constants true, false
any Value Expression of type Boolean
e1 && e2, e1 || e2, e1 ⇒ e2, !e1, where e1 and e2 are Boolean Expressions
e1 == e2, e1 > e2, e1 < e2, e1 >= e2, e1 <= e2, where e1 and e2 are Value Expression of the same type.
e1.contains(e2), e1.containsAll(e3), e1.containsAny(e3), e1.isEmpty(), where e1 and e3 are Collection Expression, the type of e3 is a supertype of the type of e1, and e2 is a Value Expression of a type which is a supertype of the type of e1.

Value Expressions are Expressions that evaluate to a value, which may be either an asset, an attribute value, or "undefined". A Value Expression may be used for comparisons, containment and modifications of the value of a feature. Value Expressions are of the form:

Any Boolean Expression
Any AssetRef Expression
Any FeatureRef Expression
Any ConstantExpression (including "undefined")
Any SymbolRef which is a reference to an EnumLiteral

Except for ConstantExpressions, the type of a Value Expression is defined depending of which other type of Expression it is. For each subclass of ConstantExpression, their type is the type of their "value" attribute: IntConstants are of type Integer, StringConstants are of type String, VersionConstants are of type Version, etc. UndefinedConstants however are of the null type.

AssetRef Expressions are Expressions that evaluate to a reference to an asset. An AssetRef Expression may be used for references values, or as the receiver of a MemberSelection. AssetRef Expressions are of the form:

Any SymbolRef which is a reference to either an asset, a guard parameter or a lambda parameter.
e1.member, where e1 is an AssetRef Expression, and member is a simple reference of a supertype of the type of e1.

The type of an AssetRef Expression is defined by:

The type of a SymbolRef is, depending on the symbol:
- for an asset, the type of the asset
- for a guard parameter, the parameter type
- for a lambda parameter, the type is inferred from the context, from the collection that the LambdaExpression that defined this parameter is filtering through.
The type of e1.member is the type of member

FeatureRef Expressions are Expressions that refers to a simple feature of an asset. A FeatureRef Expression is of the form:

e1.member, where e1 is an AssetRef Expression, and member is a simple feature of a supertype of the type of e1.

The type of a FeatureRef Expression of the form e1.member is the type of member.

Collection Expressions are Expressions that evaluate to a collection, or a reference to a collection. Collection Expressions are of the form:

Any CollectionRef Expression
e1.filter(lambda), where e1 is a Collection Expression, and lambda is a LambdaExpression.

The type of a Collection Expression is either its type as a CollectionRef if it is one, or the type of e1 if it is of the form e1.filter(lambda).

CollectionRef Expressions are Expressions that refers to a collection feature of an asset. A CollectionRef Expression is of the form:

e1.member, where e1 is an AssetRef Expression, and member is a collection feature of a supertype of the type of e1.

The type of a CollectionRef Expression of the form e1.member is the type of member.

Expressions in Actions

Actions are Expression as their target and args. The types of these expressions follows the following constraints:

in e1.assign(e2), e1 is a FeatureRef Expression, and e2 is a Value Expression, and the type of e2 is a subtype of the type of e1
in e1.add(e2) and e1.remove(e2), e1 is a CollectionRef Expression and e2 is a Value Expression, and the type of e2 is a subtype of the type of e1
in e1.addAll(e2) and e1.removeAll(e2), e1 is a CollectionRef Expression and e2 is a Collection Expression, and the type of e2 is a subtype of the type of e1
in e1.clear(), e1 is a CollectionRef Expression
in e1.forAll(lambda), e1 is a Collection Expression, of which the type is an AssetType.

1.2. ABS Editors

The AssetBasedSystem offer several editors:

fr.irisa.atsyra.absystem.model.editor a tree editor
fr.irisa.atsyra.absystem.design a graphical editor (based on Sirius)
fr.irisa.atsyra.absystem.xtext a textual editor (based on xText)

Figure 6. ATSyRA ABS editors plugins

1.2.1. Plantuml output

In addition to editors, ABS provides some plantuml generators allowing to have an overview of some of its contents.

The plantuml generator is currently located in the fr.irisa.atsyra.absystem.xtext plugin.

2. Multi Domain Analysis

2.1. ABS modelchecking-based Reachability analysis and Scenario generator

Using goal specification, ATSyRA provides :

goal reachability analysis.
scenario generation.

Figure 7. ATSyRA ABS reachability plugins

TODO describe the process

TODO describe the slicer (based on Read/Write/Control analysis of the behavior for the goal)

2.2. ABS Checker

ATSyRA contains contract checkers for ABS models. The following components are involved in the checking of contracts in ABS.

The checker reuse parts of the plugins of the ABS Interpreter.

Figure 8. ATSyRA ABS checker plugins

2.3. Reporting

ATSyRA stores analysis result of ABS model in ABSReport model. This model allows keeping track of results regardless of the tool used to produce the result (ITSTool or planner).

Its main purpose is to store the witness scenario for goals applied to a given asset model.

Figure 9. ATSyRA ABS Report plugins

3. ABS Simulation/Debug

3.1. ABS Interpreter

AtSyRA contains an interpreter for ABS model.

Thanks to GEMOC, the interpreter can run interactively and provides a debugger allowing to analyze the model memory during breakpoints.

Figure 10. ATSyRA ABS interpreter plugins