From ea0cc3b668157ee4af1cc40bdcb12066c0289c44 Mon Sep 17 00:00:00 2001
From: dontenvi <pierre.dontenville@eurecom.fr>
Date: Tue, 9 Jan 2024 12:12:36 -0500
Subject: [PATCH] random id solution in test
---
.../tmltranslator/toavatarsec/TML2Avatar.java | 18 +-
.../tmltranslator/DiplodocusSecurityTest.java | 106 +++---
.../Models/ITA01_v5/mapAtt/golden | 5 +
.../Models/ITA01_v5/mapAtt/spec.tarchi | 335 +++++++++++++++++
.../Models/ITA01_v5/mapAtt/spec.tmap | 110 ++++++
.../Models/ITA01_v5/mapAtt/spec.tml | 338 +++++++++++++++++
.../Models/ITA01_v5/mapNoProtection/golden | 0
.../ITA01_v5/mapNoProtection/spec.tarchi | 354 ++++++++++++++++++
.../Models/ITA01_v5/mapNoProtection/spec.tmap | 36 ++
.../Models/ITA01_v5/mapNoProtection/spec.tml | 338 +++++++++++++++++
10 files changed, 1582 insertions(+), 58 deletions(-)
create mode 100644 ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITA01_v5/mapAtt/golden
create mode 100644 ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITA01_v5/mapAtt/spec.tarchi
create mode 100644 ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITA01_v5/mapAtt/spec.tmap
create mode 100644 ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITA01_v5/mapAtt/spec.tml
create mode 100644 ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITA01_v5/mapNoProtection/golden
create mode 100644 ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITA01_v5/mapNoProtection/spec.tarchi
create mode 100644 ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITA01_v5/mapNoProtection/spec.tmap
create mode 100644 ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITA01_v5/mapNoProtection/spec.tml
diff --git a/src/main/java/tmltranslator/toavatarsec/TML2Avatar.java b/src/main/java/tmltranslator/toavatarsec/TML2Avatar.java
index 54912cb5ae..b7b29a887b 100644
--- a/src/main/java/tmltranslator/toavatarsec/TML2Avatar.java
+++ b/src/main/java/tmltranslator/toavatarsec/TML2Avatar.java
@@ -2480,15 +2480,17 @@ public class TML2Avatar {
}
for (SecurityPattern sp : keysPublicBus) {
- for (TMLTask taskPattern : tmlmodel.securityTaskMap.get(sp)) {
- AvatarBlock b = taskBlockMap.get(taskPattern);
- AvatarAttribute attrib = b.getAvatarAttributeWithName("key_"+sp.getName());
- if (attrib!=null) {
- LinkedList<AvatarAttribute> arguments = new LinkedList<AvatarAttribute>();
- arguments.add(attrib);
- avspec.addPragma(new AvatarPragmaPublic("#Public " + b.getName() + "." + attrib.getName(), null, arguments));
+ if (tmlmodel.securityTaskMap.get(sp) != null) {
+ for (TMLTask taskPattern : tmlmodel.securityTaskMap.get(sp)) {
+ AvatarBlock b = taskBlockMap.get(taskPattern);
+ AvatarAttribute attrib = b.getAvatarAttributeWithName("key_" + sp.getName());
+ if (attrib != null) {
+ LinkedList<AvatarAttribute> arguments = new LinkedList<AvatarAttribute>();
+ arguments.add(attrib);
+ avspec.addPragma(new AvatarPragmaPublic("#Public " + b.getName() + "." + attrib.getName(), null, arguments));
+ }
+
}
-
}
}
for (SecurityPattern sp : pubKeys.keySet()) {
diff --git a/ttool/src/test/java/tmltranslator/DiplodocusSecurityTest.java b/ttool/src/test/java/tmltranslator/DiplodocusSecurityTest.java
index 99edab6c39..106e59acde 100644
--- a/ttool/src/test/java/tmltranslator/DiplodocusSecurityTest.java
+++ b/ttool/src/test/java/tmltranslator/DiplodocusSecurityTest.java
@@ -40,11 +40,10 @@ public class DiplodocusSecurityTest extends AbstractTest {
private static final String PROVERIF_QUERY = "Query";
static String PROVERIF_DIR;
static String MODELS_DIR;
- private static HashMap<String, Pair<String, Boolean>> seenCommMap;
- //Comm id as Key. String value is for left or right. Boolean value is for
- // checking if this comm id as already been map or not.
- //Hypothesis : Comm id cant be both left and right.
- private static HashMap<String, String> commMap;
+ private static HashMap<String, String> alreadyMapComm;
+ //Map id in Proverif result with id in golden queries
+ final static String LEFT ="left";
+ final static String RIGHT ="right";
@@ -67,15 +66,15 @@ public class DiplodocusSecurityTest extends AbstractTest {
currentModel = model;
currentTabs = tabs;
goldenMap = new HashMap<>();
- seenCommMap = new HashMap<>();
- commMap = new HashMap<>();
+ alreadyMapComm = new HashMap<>();
}
@Parameterized.Parameters(name = "{index}: {0}")
public static Collection models(){
return Arrays.asList(new Object[][] {
+// {"AliceAndBobHW", new ArrayList<>(Arrays.asList("KeyExchange"))}, //the tab which include ID issue in golden
{"AliceAndBobHW", new ArrayList<>(Arrays.asList("SymmetricExchange", "Nonce", "KeyExchange", "Mac", "SampleAutoSec"))},
- {"AliceAndBobHW", new ArrayList<>(Arrays.asList("SymmetricExchange", "Nonce", "KeyExchange", "Mac", "SampleAutoSec"))}
+ {"ITA01_v5", new ArrayList<>(Arrays.asList("mapAtt", "mapNoProtection"))}
});
}
@@ -137,7 +136,6 @@ public class DiplodocusSecurityTest extends AbstractTest {
for (TMLError error: syntax.getErrors()) {
System.out.println("Error: " + error.toString());
}
-
}
assertTrue(syntax.hasErrors() == 0);
@@ -165,23 +163,27 @@ public class DiplodocusSecurityTest extends AbstractTest {
String cmd = "proverif -in pitype " + PROVERIF_DIR + pvspecFilename;
boolean summaryFound = false;
- commMap.clear();
- seenCommMap.clear();
- buildCommMap(tab);
+ alreadyMapComm.clear();
try {
proc = Runtime.getRuntime().exec(cmd);
proc_in = new BufferedReader(new InputStreamReader(proc.getInputStream()));
int nbLines =0;
+
+ if (goldenMap.get(tab) == null){
+ TraceManager.addDev("The golden for : " + tab + " is null");
+ fail();
+ }
+
while ((str = proc_in.readLine()) != null) {
// TraceManager.addDev( "Sending " + str + " from " + port + " to client..." );
System.out.println("Output from ProVerif: " + str);
if (summaryFound && (str.contains(PROVERIF_QUERY))) {
+ assertTrue(goldenMap.get(tab).length > nbLines);
+ assertTrue(equals(goldenMap.get(tab)[nbLines], str));
nbLines++;
- str = changeCommId(str);
- assertTrue(contains(tab, str));
}
if (str.contains(PROVERIF_SUMMARY)) {
@@ -199,53 +201,56 @@ public class DiplodocusSecurityTest extends AbstractTest {
TraceManager.addDev("Test for " + currentModel + " model is ended");
}
- private boolean contains(String tab, String str) {
+ private boolean equals(String line, String str) {
str = str.trim();
- if (goldenMap.get(tab) == null){
- TraceManager.addDev("The golden for : " + tab + " is null");
- return false;
+
+ if (str.startsWith(line.trim()) && !line.trim().isEmpty()) {
+ TraceManager.addDev( "\"" + str + "\"" + " is in golden");
+ return true;
}
- for(String s: goldenMap.get(tab)) {
+ String cleanStr = str.replaceAll("comm[0-9]+","comm");
+ String cleanLine = line.replaceAll("comm[0-9]+","comm");
- if (str.startsWith(s.trim())&& !s.trim().isEmpty()) {
- TraceManager.addDev( "\"" + str + "\"" + " is in golden");
- return true;
- }
+ if (!cleanStr.startsWith(cleanLine.trim()) || cleanLine.trim().isEmpty()){
+ TraceManager.addDev("\"" + str + "\"" + " not in golden");
+ return false;
+ }
+
+ String changedStr = replaceCommId(line, str);
+ if (changedStr.startsWith(line.trim()) && !line.trim().isEmpty()) {
+ TraceManager.addDev( "\"" + changedStr + "\"" + " is in golden");
+ return true;
}
+
TraceManager.addDev("\"" + str + "\"" + " not in golden");
return false;
}
- private void buildCommMap(String tab){
- for(String query: goldenMap.get(tab)) {
- TraceManager.addDev(String.valueOf(query.matches(".*comm[0-9]+.*")));
- for (Pair<String,Pair<String,Boolean>> comm: getComms(query)) {
- seenCommMap.put(comm.getFirst(),comm.getSecond());
- }
+ private String replaceCommId(String line, String str) {
+ String newStr = str;
+ ArrayList<Pair<String, String>> lineComms = findComms(line);
+ ArrayList<Pair<String, String>> strComms = findComms(str);
+ if (lineComms.size()!=strComms.size()){
+ return newStr;
}
- TraceManager.addDev("seenCommMap for " + tab +" :" + seenCommMap.toString());
- }
- private String changeCommId(String query) {
- for (Pair<String,Pair<String,Boolean>> comm: getComms(query)) {
- if (!commMap.containsKey(comm.getFirst())){ //comm id of the query generated by proverif
- String position = comm.getSecond().getFirst(); //left or right
- for (String goldenId : seenCommMap.keySet()){
- if (position.equals(seenCommMap.get(goldenId).getFirst()) && !seenCommMap.get(goldenId).getSecond()){
- seenCommMap.put(goldenId,new Pair<>(position,true));
- commMap.put(comm.getFirst(),goldenId);
- }
- }
+ for (int i = 0; i < lineComms.size(); i++) {
+ String currentIdStr = strComms.get(i).getFirst();
+ if (alreadyMapComm.containsKey(currentIdStr)){
+ newStr = newStr.replaceAll(currentIdStr,alreadyMapComm.get(currentIdStr));
+ }else{
+ newStr = newStr.replaceAll(currentIdStr,lineComms.get(i).getFirst());
+ alreadyMapComm.put(currentIdStr,lineComms.get(i).getFirst());
}
- query = query.replaceAll(comm.getFirst(),commMap.get(comm.getFirst()));
- TraceManager.addDev(comm.getFirst() + " has been replaced by " + commMap.get(comm.getFirst()));
+ TraceManager.addDev("\"" + currentIdStr + "\"" + " has been replaced by " + "\"" + alreadyMapComm.get(currentIdStr) + "\"");
}
- return query;
+ return newStr;
}
- private ArrayList<Pair<String,
- Pair<String, Boolean>>> getComms(String query){
- ArrayList<Pair<String, Pair<String, Boolean>>> comms = new ArrayList<>();
+
+
+ private ArrayList<Pair<String, String>> findComms(String query){
+ ArrayList<Pair<String, String>> comms = new ArrayList<>();
if (query.contains("==>") && query.matches(".*comm[0-9]+.*")) {
int index = query.indexOf("==>");
int lookingIndex = 0; //current query substring index
@@ -265,11 +270,11 @@ public class DiplodocusSecurityTest extends AbstractTest {
idUnit = "" + query.charAt(queryIndex + incr);
incr += 1;
}
- String position = "left";
+ String position = LEFT;
if (queryIndex > index) {
- position = "right";
+ position = RIGHT;
}
- comms.add(new Pair<>(id.toString(), new Pair<>(position, false)));
+ comms.add(new Pair<>(id.toString(), position));
m = p.matcher(query.substring(queryIndex));
}
@@ -277,4 +282,5 @@ public class DiplodocusSecurityTest extends AbstractTest {
}
return comms;
}
+
}
diff --git a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITA01_v5/mapAtt/golden b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITA01_v5/mapAtt/golden
new file mode 100644
index 0000000000..f549761872
--- /dev/null
+++ b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITA01_v5/mapAtt/golden
@@ -0,0 +1,5 @@
+Query not attacker(BatterySensor___Application__battery_chData[!1 = v]) is true.
+Query not attacker(PumpController___Application__feedback4App_chData[!1 = v]) is true.
+Query not attacker(SmartphoneAppController___Application__emergencySign_chData[!1 = v]) is true.
+Query inj-event(authenticity___MedicalInformationSystem___emergencySign_chData___aftersignalstate_Application_emergencySign_Application_emergencySign(dummyM)) ==> inj-event(authenticity___SmartphoneAppController___emergencySign_chData___signalstate_Application_emergencySign_Application_emergencySign(dummyM)) is true.
+Query inj-event(authenticity___SmartphoneAppController___feedback4App_chData___aftersignalstate_Application_feedback4App_Application_feedback4App(dummyM)) ==> inj-event(authenticity___PumpController___feedback4App_chData___signalstate_Application_feedback4App_Application_feedback4App(dummyM)) is false.
diff --git a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITA01_v5/mapAtt/spec.tarchi b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITA01_v5/mapAtt/spec.tarchi
new file mode 100644
index 0000000000..a40efcbba4
--- /dev/null
+++ b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITA01_v5/mapAtt/spec.tarchi
@@ -0,0 +1,335 @@
+// Master clock frequency - in MHz
+MASTERCLOCKFREQUENCY 200
+
+NODE CPU PumpActuatorMCU
+SET PumpActuatorMCU nbOfCores 1
+SET PumpActuatorMCU byteDataSize 4
+SET PumpActuatorMCU pipelineSize 5
+SET PumpActuatorMCU goIdleTime 10
+SET PumpActuatorMCU maxConsecutiveIdleCycles 10
+SET PumpActuatorMCU taskSwitchingTime 20
+SET PumpActuatorMCU branchingPredictionPenalty 2
+SET PumpActuatorMCU cacheMiss 5
+SET PumpActuatorMCU schedulingPolicy 0
+SET PumpActuatorMCU sliceTime 10000
+SET PumpActuatorMCU execiTime 1
+SET PumpActuatorMCU execcTime 1
+SET PumpActuatorMCU clockDivider 1
+
+NODE BUS BT
+SET BT byteDataSize 4
+SET BT pipelineSize 1
+SET BT arbitration 0
+SET BT sliceTime 10000
+SET BT burstSize 100
+SET BT privacy private
+SET BT clockDivider 1
+
+NODE MEMORY MedicalMemory
+SET MedicalMemory byteDataSize 4
+SET MedicalMemory clockDivider 1
+
+NODE CPU MedicalCPU
+SET MedicalCPU nbOfCores 1
+SET MedicalCPU byteDataSize 4
+SET MedicalCPU pipelineSize 5
+SET MedicalCPU goIdleTime 10
+SET MedicalCPU maxConsecutiveIdleCycles 10
+SET MedicalCPU taskSwitchingTime 20
+SET MedicalCPU branchingPredictionPenalty 2
+SET MedicalCPU cacheMiss 5
+SET MedicalCPU schedulingPolicy 0
+SET MedicalCPU sliceTime 10000
+SET MedicalCPU execiTime 1
+SET MedicalCPU execcTime 1
+SET MedicalCPU clockDivider 1
+
+NODE BUS MedicalBus
+SET MedicalBus byteDataSize 4
+SET MedicalBus pipelineSize 1
+SET MedicalBus arbitration 0
+SET MedicalBus sliceTime 10000
+SET MedicalBus burstSize 100
+SET MedicalBus privacy private
+SET MedicalBus clockDivider 1
+
+NODE BRIDGE MedicalBridge
+SET MedicalBridge bufferByteSize 4
+SET MedicalBridge clockDivider 1
+
+NODE BUS MedicalIOBus
+SET MedicalIOBus byteDataSize 4
+SET MedicalIOBus pipelineSize 1
+SET MedicalIOBus arbitration 0
+SET MedicalIOBus sliceTime 10000
+SET MedicalIOBus burstSize 100
+SET MedicalIOBus privacy private
+SET MedicalIOBus clockDivider 1
+
+NODE BRIDGE MedicalNetwork
+SET MedicalNetwork bufferByteSize 4
+SET MedicalNetwork clockDivider 1
+
+NODE MEMORY SmartphoneMemory
+SET SmartphoneMemory byteDataSize 4
+SET SmartphoneMemory clockDivider 1
+
+NODE BUS SmartphoneBus
+SET SmartphoneBus byteDataSize 4
+SET SmartphoneBus pipelineSize 1
+SET SmartphoneBus arbitration 0
+SET SmartphoneBus sliceTime 10000
+SET SmartphoneBus burstSize 100
+SET SmartphoneBus privacy private
+SET SmartphoneBus clockDivider 1
+
+NODE BRIDGE SmartphoneBridge
+SET SmartphoneBridge bufferByteSize 4
+SET SmartphoneBridge clockDivider 1
+
+NODE BRIDGE SmartphoneNetwork
+SET SmartphoneNetwork bufferByteSize 4
+SET SmartphoneNetwork clockDivider 1
+
+NODE BUS SmartphoneIOBus
+SET SmartphoneIOBus byteDataSize 4
+SET SmartphoneIOBus pipelineSize 1
+SET SmartphoneIOBus arbitration 0
+SET SmartphoneIOBus sliceTime 10000
+SET SmartphoneIOBus burstSize 100
+SET SmartphoneIOBus privacy private
+SET SmartphoneIOBus clockDivider 1
+
+NODE BRIDGE PumpNetwork
+SET PumpNetwork bufferByteSize 4
+SET PumpNetwork clockDivider 1
+
+NODE CPU ReservoirSensorMCU
+SET ReservoirSensorMCU nbOfCores 1
+SET ReservoirSensorMCU byteDataSize 4
+SET ReservoirSensorMCU pipelineSize 5
+SET ReservoirSensorMCU goIdleTime 10
+SET ReservoirSensorMCU maxConsecutiveIdleCycles 10
+SET ReservoirSensorMCU taskSwitchingTime 20
+SET ReservoirSensorMCU branchingPredictionPenalty 2
+SET ReservoirSensorMCU cacheMiss 5
+SET ReservoirSensorMCU schedulingPolicy 0
+SET ReservoirSensorMCU sliceTime 10000
+SET ReservoirSensorMCU execiTime 1
+SET ReservoirSensorMCU execcTime 1
+SET ReservoirSensorMCU clockDivider 1
+
+NODE CPU BatterySensorMCU
+SET BatterySensorMCU nbOfCores 1
+SET BatterySensorMCU byteDataSize 4
+SET BatterySensorMCU pipelineSize 5
+SET BatterySensorMCU goIdleTime 10
+SET BatterySensorMCU maxConsecutiveIdleCycles 10
+SET BatterySensorMCU taskSwitchingTime 20
+SET BatterySensorMCU branchingPredictionPenalty 2
+SET BatterySensorMCU cacheMiss 5
+SET BatterySensorMCU schedulingPolicy 0
+SET BatterySensorMCU sliceTime 10000
+SET BatterySensorMCU execiTime 1
+SET BatterySensorMCU execcTime 1
+SET BatterySensorMCU clockDivider 1
+
+NODE MEMORY PumpMemory
+SET PumpMemory byteDataSize 4
+SET PumpMemory clockDivider 1
+
+NODE CPU PumpProcessor
+SET PumpProcessor nbOfCores 1
+SET PumpProcessor byteDataSize 4
+SET PumpProcessor pipelineSize 5
+SET PumpProcessor goIdleTime 10
+SET PumpProcessor maxConsecutiveIdleCycles 10
+SET PumpProcessor taskSwitchingTime 20
+SET PumpProcessor branchingPredictionPenalty 2
+SET PumpProcessor cacheMiss 5
+SET PumpProcessor schedulingPolicy 0
+SET PumpProcessor sliceTime 10000
+SET PumpProcessor execiTime 1
+SET PumpProcessor execcTime 1
+SET PumpProcessor clockDivider 1
+
+NODE CPU GlucoseSensorMCU
+SET GlucoseSensorMCU nbOfCores 1
+SET GlucoseSensorMCU byteDataSize 4
+SET GlucoseSensorMCU pipelineSize 5
+SET GlucoseSensorMCU goIdleTime 10
+SET GlucoseSensorMCU maxConsecutiveIdleCycles 10
+SET GlucoseSensorMCU taskSwitchingTime 20
+SET GlucoseSensorMCU branchingPredictionPenalty 2
+SET GlucoseSensorMCU cacheMiss 5
+SET GlucoseSensorMCU schedulingPolicy 0
+SET GlucoseSensorMCU sliceTime 10000
+SET GlucoseSensorMCU execiTime 1
+SET GlucoseSensorMCU execcTime 1
+SET GlucoseSensorMCU clockDivider 1
+
+NODE BUS InterconnectionNetwork
+SET InterconnectionNetwork byteDataSize 4
+SET InterconnectionNetwork pipelineSize 1
+SET InterconnectionNetwork arbitration 0
+SET InterconnectionNetwork sliceTime 10000
+SET InterconnectionNetwork burstSize 100
+SET InterconnectionNetwork privacy public
+SET InterconnectionNetwork clockDivider 1
+
+NODE CPU SmartphoneCPU
+SET SmartphoneCPU nbOfCores 1
+SET SmartphoneCPU byteDataSize 4
+SET SmartphoneCPU pipelineSize 5
+SET SmartphoneCPU goIdleTime 10
+SET SmartphoneCPU maxConsecutiveIdleCycles 10
+SET SmartphoneCPU taskSwitchingTime 20
+SET SmartphoneCPU branchingPredictionPenalty 2
+SET SmartphoneCPU cacheMiss 5
+SET SmartphoneCPU schedulingPolicy 0
+SET SmartphoneCPU sliceTime 10000
+SET SmartphoneCPU execiTime 1
+SET SmartphoneCPU execcTime 1
+SET SmartphoneCPU clockDivider 1
+
+NODE BUS PumpBus
+SET PumpBus byteDataSize 4
+SET PumpBus pipelineSize 1
+SET PumpBus arbitration 0
+SET PumpBus sliceTime 10000
+SET PumpBus burstSize 100
+SET PumpBus privacy private
+SET PumpBus clockDivider 1
+
+NODE BRIDGE toPumpIOBus
+SET toPumpIOBus bufferByteSize 4
+SET toPumpIOBus clockDivider 1
+
+NODE BUS PumpIOBus
+SET PumpIOBus byteDataSize 1
+SET PumpIOBus pipelineSize 1
+SET PumpIOBus arbitration 0
+SET PumpIOBus sliceTime 10000
+SET PumpIOBus burstSize 100
+SET PumpIOBus privacy private
+SET PumpIOBus clockDivider 1
+
+NODE BRIDGE SmartphoneBTInterface
+SET SmartphoneBTInterface bufferByteSize 4
+SET SmartphoneBTInterface clockDivider 1
+
+NODE CPU DisplayMCU
+SET DisplayMCU nbOfCores 1
+SET DisplayMCU byteDataSize 4
+SET DisplayMCU pipelineSize 5
+SET DisplayMCU goIdleTime 10
+SET DisplayMCU maxConsecutiveIdleCycles 10
+SET DisplayMCU taskSwitchingTime 20
+SET DisplayMCU branchingPredictionPenalty 2
+SET DisplayMCU cacheMiss 5
+SET DisplayMCU schedulingPolicy 0
+SET DisplayMCU sliceTime 10000
+SET DisplayMCU execiTime 1
+SET DisplayMCU execcTime 1
+SET DisplayMCU clockDivider 1
+
+NODE LINK link_SmartphoneNetwork_to_InterconnectionNetwork
+SET link_SmartphoneNetwork_to_InterconnectionNetwork node SmartphoneNetwork
+SET link_SmartphoneNetwork_to_InterconnectionNetwork bus InterconnectionNetwork
+SET link_SmartphoneNetwork_to_InterconnectionNetwork priority 0
+NODE LINK link_PumpNetwork_to_InterconnectionNetwork
+SET link_PumpNetwork_to_InterconnectionNetwork node PumpNetwork
+SET link_PumpNetwork_to_InterconnectionNetwork bus InterconnectionNetwork
+SET link_PumpNetwork_to_InterconnectionNetwork priority 0
+NODE LINK link_PumpNetwork_to_PumpIOBus
+SET link_PumpNetwork_to_PumpIOBus node PumpNetwork
+SET link_PumpNetwork_to_PumpIOBus bus PumpIOBus
+SET link_PumpNetwork_to_PumpIOBus priority 0
+NODE LINK link_ReservoirSensorMCU_to_PumpIOBus
+SET link_ReservoirSensorMCU_to_PumpIOBus node ReservoirSensorMCU
+SET link_ReservoirSensorMCU_to_PumpIOBus bus PumpIOBus
+SET link_ReservoirSensorMCU_to_PumpIOBus priority 0
+NODE LINK link_BatterySensorMCU_to_PumpIOBus
+SET link_BatterySensorMCU_to_PumpIOBus node BatterySensorMCU
+SET link_BatterySensorMCU_to_PumpIOBus bus PumpIOBus
+SET link_BatterySensorMCU_to_PumpIOBus priority 0
+NODE LINK link_toPumpIOBus_to_PumpIOBus
+SET link_toPumpIOBus_to_PumpIOBus node toPumpIOBus
+SET link_toPumpIOBus_to_PumpIOBus bus PumpIOBus
+SET link_toPumpIOBus_to_PumpIOBus priority 0
+NODE LINK link_toPumpIOBus_to_PumpBus
+SET link_toPumpIOBus_to_PumpBus node toPumpIOBus
+SET link_toPumpIOBus_to_PumpBus bus PumpBus
+SET link_toPumpIOBus_to_PumpBus priority 0
+NODE LINK link_PumpProcessor_to_PumpBus
+SET link_PumpProcessor_to_PumpBus node PumpProcessor
+SET link_PumpProcessor_to_PumpBus bus PumpBus
+SET link_PumpProcessor_to_PumpBus priority 0
+NODE LINK link_PumpMemory_to_PumpBus
+SET link_PumpMemory_to_PumpBus node PumpMemory
+SET link_PumpMemory_to_PumpBus bus PumpBus
+SET link_PumpMemory_to_PumpBus priority 0
+NODE LINK link_SmartphoneNetwork_to_SmartphoneIOBus
+SET link_SmartphoneNetwork_to_SmartphoneIOBus node SmartphoneNetwork
+SET link_SmartphoneNetwork_to_SmartphoneIOBus bus SmartphoneIOBus
+SET link_SmartphoneNetwork_to_SmartphoneIOBus priority 0
+NODE LINK link_DisplayMCU_to_SmartphoneIOBus
+SET link_DisplayMCU_to_SmartphoneIOBus node DisplayMCU
+SET link_DisplayMCU_to_SmartphoneIOBus bus SmartphoneIOBus
+SET link_DisplayMCU_to_SmartphoneIOBus priority 0
+NODE LINK link_SmartphoneBridge_to_SmartphoneIOBus
+SET link_SmartphoneBridge_to_SmartphoneIOBus node SmartphoneBridge
+SET link_SmartphoneBridge_to_SmartphoneIOBus bus SmartphoneIOBus
+SET link_SmartphoneBridge_to_SmartphoneIOBus priority 0
+NODE LINK link_SmartphoneBridge_to_SmartphoneBus
+SET link_SmartphoneBridge_to_SmartphoneBus node SmartphoneBridge
+SET link_SmartphoneBridge_to_SmartphoneBus bus SmartphoneBus
+SET link_SmartphoneBridge_to_SmartphoneBus priority 0
+NODE LINK link_SmartphoneCPU_to_SmartphoneBus
+SET link_SmartphoneCPU_to_SmartphoneBus node SmartphoneCPU
+SET link_SmartphoneCPU_to_SmartphoneBus bus SmartphoneBus
+SET link_SmartphoneCPU_to_SmartphoneBus priority 0
+NODE LINK link_SmartphoneMemory_to_SmartphoneBus
+SET link_SmartphoneMemory_to_SmartphoneBus node SmartphoneMemory
+SET link_SmartphoneMemory_to_SmartphoneBus bus SmartphoneBus
+SET link_SmartphoneMemory_to_SmartphoneBus priority 0
+NODE LINK link_MedicalNetwork_to_InterconnectionNetwork
+SET link_MedicalNetwork_to_InterconnectionNetwork node MedicalNetwork
+SET link_MedicalNetwork_to_InterconnectionNetwork bus InterconnectionNetwork
+SET link_MedicalNetwork_to_InterconnectionNetwork priority 0
+NODE LINK link_MedicalNetwork_to_MedicalIOBus
+SET link_MedicalNetwork_to_MedicalIOBus node MedicalNetwork
+SET link_MedicalNetwork_to_MedicalIOBus bus MedicalIOBus
+SET link_MedicalNetwork_to_MedicalIOBus priority 0
+NODE LINK link_MedicalBridge_to_MedicalIOBus
+SET link_MedicalBridge_to_MedicalIOBus node MedicalBridge
+SET link_MedicalBridge_to_MedicalIOBus bus MedicalIOBus
+SET link_MedicalBridge_to_MedicalIOBus priority 0
+NODE LINK link_MedicalBridge_to_MedicalBus
+SET link_MedicalBridge_to_MedicalBus node MedicalBridge
+SET link_MedicalBridge_to_MedicalBus bus MedicalBus
+SET link_MedicalBridge_to_MedicalBus priority 0
+NODE LINK link_MedicalCPU_to_MedicalBus
+SET link_MedicalCPU_to_MedicalBus node MedicalCPU
+SET link_MedicalCPU_to_MedicalBus bus MedicalBus
+SET link_MedicalCPU_to_MedicalBus priority 0
+NODE LINK link_MedicalMemory_to_MedicalBus
+SET link_MedicalMemory_to_MedicalBus node MedicalMemory
+SET link_MedicalMemory_to_MedicalBus bus MedicalBus
+SET link_MedicalMemory_to_MedicalBus priority 0
+NODE LINK link_SmartphoneBTInterface_to_BT
+SET link_SmartphoneBTInterface_to_BT node SmartphoneBTInterface
+SET link_SmartphoneBTInterface_to_BT bus BT
+SET link_SmartphoneBTInterface_to_BT priority 0
+NODE LINK link_PumpActuatorMCU_to_PumpIOBus
+SET link_PumpActuatorMCU_to_PumpIOBus node PumpActuatorMCU
+SET link_PumpActuatorMCU_to_PumpIOBus bus PumpIOBus
+SET link_PumpActuatorMCU_to_PumpIOBus priority 0
+NODE LINK link_GlucoseSensorMCU_to_BT
+SET link_GlucoseSensorMCU_to_BT node GlucoseSensorMCU
+SET link_GlucoseSensorMCU_to_BT bus BT
+SET link_GlucoseSensorMCU_to_BT priority 0
+NODE LINK link_SmartphoneBTInterface_to_SmartphoneIOBus
+SET link_SmartphoneBTInterface_to_SmartphoneIOBus node SmartphoneBTInterface
+SET link_SmartphoneBTInterface_to_SmartphoneIOBus bus SmartphoneIOBus
+SET link_SmartphoneBTInterface_to_SmartphoneIOBus priority 0
diff --git a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITA01_v5/mapAtt/spec.tmap b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITA01_v5/mapAtt/spec.tmap
new file mode 100644
index 0000000000..02086a63ad
--- /dev/null
+++ b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITA01_v5/mapAtt/spec.tmap
@@ -0,0 +1,110 @@
+TMLSPEC
+ #include "spec.tml"
+ENDTMLSPEC
+
+TMLARCHI
+ #include "spec.tarchi"
+ENDTMLARCHI
+
+TMLMAPPING
+ MAP PumpActuatorMCU Application__PumpActuator
+ SET Application__PumpActuator priority 0
+ MAP MedicalCPU Application__MedicalInformationSystem
+ SET Application__MedicalInformationSystem priority 0
+ MAP ReservoirSensorMCU Application__ReservoirSensor
+ SET Application__ReservoirSensor priority 0
+ MAP BatterySensorMCU Application__BatterySensor
+ SET Application__BatterySensor priority 0
+ MAP PumpProcessor Application__PumpController
+ SET Application__PumpController priority 0
+ MAP PumpProcessor Application__PumpControllerTimer
+ SET Application__PumpControllerTimer priority 0
+ MAP GlucoseSensorMCU Application__GlucoseLevelSensor
+ SET Application__GlucoseLevelSensor priority 0
+ MAP SmartphoneCPU Application__SmartphoneAppController
+ SET Application__SmartphoneAppController priority 0
+ MAP SmartphoneCPU Application__AppControllerTimerBasal
+ SET Application__AppControllerTimerBasal priority 0
+ MAP SmartphoneCPU Application__AppControllerTimer
+ SET Application__AppControllerTimer priority 0
+ MAP DisplayMCU Application__SmartphoneAppInterface
+ SET Application__SmartphoneAppInterface priority 0
+ MAP DisplayMCU Application__AppInterfaceTimer
+ SET Application__AppInterfaceTimer priority 0
+ MAP MedicalMemory Application__emergencySign
+ SET Application__emergencySign priority 0
+ MAP SmartphoneBus Application__emergencySign
+ SET Application__emergencySign priority 0
+ MAP SmartphoneIOBus Application__emergencySign
+ SET Application__emergencySign priority 0
+ MAP InterconnectionNetwork Application__emergencySign
+ SET Application__emergencySign priority 0
+ MAP MedicalIOBus Application__emergencySign
+ SET Application__emergencySign priority 0
+ MAP MedicalBus Application__emergencySign
+ SET Application__emergencySign priority 0
+ MAP SmartphoneMemory Application__glucose
+ SET Application__glucose priority 0
+ MAP SmartphoneBus Application__glucose
+ SET Application__glucose priority 0
+ MAP SmartphoneIOBus Application__glucose
+ SET Application__glucose priority 0
+ MAP BT Application__glucose
+ SET Application__glucose priority 0
+ MAP SmartphoneMemory Application__feedback4Interface
+ SET Application__feedback4Interface priority 0
+ MAP SmartphoneBus Application__feedback4Interface
+ SET Application__feedback4Interface priority 0
+ MAP SmartphoneMemory Application__inputCalories
+ SET Application__inputCalories priority 0
+ MAP SmartphoneBus Application__inputCalories
+ SET Application__inputCalories priority 0
+ MAP PumpMemory Application__battery
+ SET Application__battery priority 0
+ MAP PumpBus Application__battery
+ SET Application__battery priority 0
+ MAP PumpIOBus Application__battery
+ SET Application__battery priority 0
+ MAP PumpMemory Application__reservoir
+ SET Application__reservoir priority 0
+ MAP PumpBus Application__reservoir
+ SET Application__reservoir priority 0
+ MAP PumpIOBus Application__reservoir
+ SET Application__reservoir priority 0
+ MAP PumpMemory Application__pumpBasal
+ SET Application__pumpBasal priority 0
+ MAP SmartphoneBus Application__pumpBasal
+ SET Application__pumpBasal priority 0
+ MAP SmartphoneIOBus Application__pumpBasal
+ SET Application__pumpBasal priority 0
+ MAP InterconnectionNetwork Application__pumpBasal
+ SET Application__pumpBasal priority 0
+ MAP PumpBus Application__pumpBasal
+ SET Application__pumpBasal priority 0
+ MAP PumpIOBus Application__pumpBasal
+ SET Application__pumpBasal priority 0
+ MAP PumpMemory Application__pumpBolus
+ SET Application__pumpBolus priority 0
+ MAP SmartphoneBus Application__pumpBolus
+ SET Application__pumpBolus priority 0
+ MAP SmartphoneIOBus Application__pumpBolus
+ SET Application__pumpBolus priority 0
+ MAP InterconnectionNetwork Application__pumpBolus
+ SET Application__pumpBolus priority 0
+ MAP PumpBus Application__pumpBolus
+ SET Application__pumpBolus priority 0
+ MAP PumpIOBus Application__pumpBolus
+ SET Application__pumpBolus priority 0
+ MAP PumpMemory Application__feedback4App
+ SET Application__feedback4App priority 0
+ MAP PumpBus Application__feedback4App
+ SET Application__feedback4App priority 0
+ MAP PumpIOBus Application__feedback4App
+ SET Application__feedback4App priority 0
+ MAP InterconnectionNetwork Application__feedback4App
+ SET Application__feedback4App priority 0
+ MAP SmartphoneIOBus Application__feedback4App
+ SET Application__feedback4App priority 0
+ MAP SmartphoneBus Application__feedback4App
+ SET Application__feedback4App priority 0
+ENDTMLMAPPING
diff --git a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITA01_v5/mapAtt/spec.tml b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITA01_v5/mapAtt/spec.tml
new file mode 100644
index 0000000000..c763c0423a
--- /dev/null
+++ b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITA01_v5/mapAtt/spec.tml
@@ -0,0 +1,338 @@
+// TML Application - FORMAT 0.2
+// Application: /media/sf_vbox_shared/ITA01_v5.xml
+// Generated: Wed Dec 27 10:10:39 EST 2023
+
+// PRAGMAS
+
+// Channels
+CHANNEL Application__battery BRBW 40 8 OUT Application__BatterySensor IN Application__PumpController
+VCCHANNEL Application__battery 0
+CONFCHANNEL Application__battery
+CHANNEL Application__emergencySign BRBW 40 8 OUT Application__SmartphoneAppController IN Application__MedicalInformationSystem
+VCCHANNEL Application__emergencySign 0
+CONFCHANNEL Application__emergencySign
+AUTHCHANNEL Application__emergencySign
+CHANNEL Application__feedback4App BRBW 40 8 OUT Application__PumpController IN Application__SmartphoneAppController
+VCCHANNEL Application__feedback4App 0
+CONFCHANNEL Application__feedback4App
+AUTHCHANNEL Application__feedback4App
+CHANNEL Application__feedback4Interface BRBW 40 8 OUT Application__SmartphoneAppController IN Application__SmartphoneAppInterface
+VCCHANNEL Application__feedback4Interface 0
+CHANNEL Application__glucose BRBW 40 8 OUT Application__GlucoseLevelSensor IN Application__SmartphoneAppController
+VCCHANNEL Application__glucose 0
+CHANNEL Application__inputCalories BRBW 40 1 OUT Application__SmartphoneAppInterface IN Application__SmartphoneAppController
+VCCHANNEL Application__inputCalories 0
+CHANNEL Application__pumpBasal BRBW 40 8 OUT Application__SmartphoneAppController IN Application__PumpController
+VCCHANNEL Application__pumpBasal 0
+CHANNEL Application__pumpBolus BRBW 40 8 OUT Application__SmartphoneAppController IN Application__PumpController
+VCCHANNEL Application__pumpBolus 0
+CHANNEL Application__reservoir BRNBW 40 OUT Application__ReservoirSensor IN Application__PumpController
+VCCHANNEL Application__reservoir 0
+
+// Events
+EVENT Application__batteryE__Application__batteryE(int) NIB 8 Application__BatterySensor Application__PumpController
+EVENT Application__emergencyResponseE__Application__emergencyResponseE() NIB 8 Application__MedicalInformationSystem Application__SmartphoneAppController
+EVENT Application__emergencySignE__Application__emergencySignE() NIB 8 Application__SmartphoneAppController Application__MedicalInformationSystem
+EVENT Application__feedback4AppE__Application__feedback4AppE(int, int, int) NIB 8 Application__PumpController Application__SmartphoneAppController
+EVENT Application__feedback4InterfaceE__Application__feedback4InterfaceE(int, int, int) NIB 8 Application__SmartphoneAppController Application__SmartphoneAppInterface
+EVENT Application__glucoseE__Application__glucoseE(int) NIB 8 Application__GlucoseLevelSensor Application__SmartphoneAppController
+EVENT Application__inputCaloriesE__Application__inputCaloriesE(int) NIB 8 Application__SmartphoneAppInterface Application__SmartphoneAppController
+EVENT Application__pumpBasalE__Application__pumpBasalE(int) NIB 8 Application__SmartphoneAppController Application__PumpController
+EVENT Application__pumpBolusE__Application__pumpBolusE(int) NIB 8 Application__SmartphoneAppController Application__PumpController
+EVENT Application__reservoirE__Application__reservoirE(int) NIB 8 Application__ReservoirSensor Application__PumpController
+EVENT Application__resetAppTimerBasal__Application__resetAppTimerBasal() NIB 8 Application__SmartphoneAppController Application__AppControllerTimerBasal
+EVENT Application__resetAppTimer__Application__resetAppTimer() NIB 8 Application__SmartphoneAppController Application__AppControllerTimer
+EVENT Application__resetInterfaceTimer__Application__resetInterfaceTimer() NIB 8 Application__SmartphoneAppInterface Application__AppInterfaceTimer
+EVENT Application__resetTimer__Application__resetTimer() NIB 8 Application__PumpController Application__PumpControllerTimer
+EVENT Application__startPumping__Application__startPumping() NIB 8 Application__PumpController Application__PumpActuator
+EVENT Application__stopPumping__Application__stopPumping() NIB 8 Application__PumpController Application__PumpActuator
+EVENT Application__timeout4Basal__Application__timeout4Basal() NIB 8 Application__AppControllerTimerBasal Application__SmartphoneAppController
+EVENT Application__timeout4CtrlFeedback__Application__timeout4CtrlFeeback() NIB 8 Application__PumpControllerTimer Application__PumpController
+EVENT Application__timeout4Eat__Application__timeout4Eat() NIB 8 Application__AppInterfaceTimer Application__SmartphoneAppInterface
+EVENT Application__timeout4Feedback__Application__timeout4Feedback() NIB 8 Application__AppControllerTimer Application__SmartphoneAppController
+
+// Requests
+
+TASK Application__AppControllerTimer
+ TASKOP
+ //Local variables
+ int loop_0 = 0
+
+ //Behavior
+ FOR(loop_0 = 0; loop_0<1; loop_0 = loop_0 + 1)
+ WAIT Application__resetAppTimer__Application__resetAppTimer
+ DELAY 10 ms isActiveDelay false
+ NOTIFY Application__timeout4Feedback__Application__timeout4Feedback
+ ENDFOR
+ENDTASK
+
+TASK Application__AppControllerTimerBasal
+ TASKOP
+ //Local variables
+ int loop_0 = 0
+
+ //Behavior
+ FOR(loop_0 = 0; loop_0<1; loop_0 = loop_0 + 1)
+ WAIT Application__resetAppTimerBasal__Application__resetAppTimerBasal
+ DELAY 10 ms isActiveDelay false
+ NOTIFY Application__timeout4Basal__Application__timeout4Basal
+ ENDFOR
+ENDTASK
+
+TASK Application__AppInterfaceTimer
+ TASKOP
+ //Local variables
+ int loop_0 = 0
+
+ //Behavior
+ FOR(loop_0 = 0; loop_0<1; loop_0 = loop_0 + 1)
+ WAIT Application__resetInterfaceTimer__Application__resetInterfaceTimer
+ DELAY 100 ms isActiveDelay false
+ NOTIFY Application__timeout4Eat__Application__timeout4Eat
+ ENDFOR
+ENDTASK
+
+TASK Application__BatterySensor
+ TASKOP
+ //Local variables
+ int level
+ int loop_0 = 0
+
+ //Behavior
+ FOR(loop_0 = 0; loop_0<1; loop_0 = loop_0 + 1)
+ DELAY 10 ms isActiveDelay false
+ RANDOM 0 level 0 2
+ NOTIFY Application__batteryE__Application__batteryE level
+ WRITE Application__battery 1
+ ENDFOR
+ENDTASK
+
+TASK Application__GlucoseLevelSensor
+ TASKOP
+ //Local variables
+ int level
+ int loop_0 = 0
+
+ //Behavior
+ FOR(loop_0 = 0; loop_0<1; loop_0 = loop_0 + 1)
+ DELAY 10 ms isActiveDelay false
+ RANDOM 0 level 1 3
+ NOTIFY Application__glucoseE__Application__glucoseE level
+ WRITE Application__glucose 1
+ ENDFOR
+ENDTASK
+
+TASK Application__MedicalInformationSystem
+ TASKOP
+ //Local variables
+ int loop_0 = 0
+
+ //Behavior
+ FOR(loop_0 = 0; loop_0<1; loop_0 = loop_0 + 1)
+ WAIT Application__emergencySignE__Application__emergencySignE
+ EXECC 100 AES_Emergency SE 100 100 0 0 - - 2
+ READ Application__emergencySign 1+0 AES_Emergency
+ EXECI 5000
+ NOTIFY Application__emergencyResponseE__Application__emergencyResponseE
+ ENDFOR
+ENDTASK
+
+TASK Application__PumpActuator
+ TASKOP
+ //Local variables
+ int loop_0 = 0
+
+ //Behavior
+ FOR(loop_0 = 0; loop_0<1; loop_0 = loop_0 + 1)
+ SELECTEVT
+ CASE Application__startPumping__Application__startPumping
+ EXECI 10000
+ ENDCASE
+ CASE Application__stopPumping__Application__stopPumping
+ EXECI 10000
+ ENDCASE
+ ENDSELECTEVT
+ ENDFOR
+ENDTASK
+
+TASK Application__PumpController
+ TASKOP
+ //Local variables
+ int batteryLevel = 2
+ int reservoirLevel = 2
+ int pumpingStatus = 0
+ int basal
+ int bolus
+ int insulineToPump = 0
+ int i
+ int x
+ int loop_0 = 0
+
+ //Behavior
+ NOTIFY Application__resetTimer__Application__resetTimer
+ FOR(loop_0 = 0; loop_0<10; loop_0 = loop_0 + 1)
+ SELECTEVT
+ CASE Application__timeout4CtrlFeedback__Application__timeout4CtrlFeeback
+ NOTIFY Application__feedback4AppE__Application__feedback4AppE batteryLevel reservoirLevel pumpingStatus
+ EXECC 100 AES_CTRL SE 100 100 0 0 - - 1
+ WRITE Application__feedback4App 1+0 AES_CTRL
+ ENDCASE
+ CASE Application__reservoirE__Application__reservoirE reservoirLevel
+ READ Application__reservoir 1
+ ENDCASE
+ CASE Application__batteryE__Application__batteryE batteryLevel
+ READ Application__battery 1
+ ENDCASE
+ CASE Application__pumpBolusE__Application__pumpBolusE bolus
+ READ Application__pumpBolus 1
+ IF (pumpingStatus==1)
+ NOTIFY Application__stopPumping__Application__stopPumping
+ pumpingStatus=0
+ ELSE
+ ENDIF
+ insulineToPump=insulineToPump+bolus*10
+ NOTIFY Application__startPumping__Application__startPumping
+ pumpingStatus=1
+ FOR(i=insulineToPump; i>0; i=i-1)
+ DELAY 1 ms isActiveDelay false
+ ENDFOR
+ NOTIFY Application__stopPumping__Application__stopPumping
+ pumpingStatus=0
+ ENDCASE
+ CASE Application__pumpBasalE__Application__pumpBasalE basal
+ READ Application__pumpBasal 1
+ IF (pumpingStatus==0)
+ insulineToPump=5
+ NOTIFY Application__startPumping__Application__startPumping
+ pumpingStatus=1
+ FOR(i=insulineToPump; i>0; i=i-1)
+ DELAY 1 ms isActiveDelay false
+ ENDFOR
+ NOTIFY Application__stopPumping__Application__stopPumping
+ pumpingStatus=0
+ ELSE
+ ENDIF
+ ENDCASE
+ ENDSELECTEVT
+ ENDFOR
+ENDTASK
+
+TASK Application__PumpControllerTimer
+ TASKOP
+ //Local variables
+ int loop_0 = 0
+
+ //Behavior
+ FOR(loop_0 = 0; loop_0<1; loop_0 = loop_0 + 1)
+ WAIT Application__resetTimer__Application__resetTimer
+ DELAY 10 ms isActiveDelay false
+ NOTIFY Application__timeout4CtrlFeedback__Application__timeout4CtrlFeeback
+ ENDFOR
+ENDTASK
+
+TASK Application__ReservoirSensor
+ TASKOP
+ //Local variables
+ int level
+ int loop_0 = 0
+
+ //Behavior
+ FOR(loop_0 = 0; loop_0<1; loop_0 = loop_0 + 1)
+ DELAY 10 ms isActiveDelay false
+ RANDOM 0 level 0 2
+ NOTIFY Application__reservoirE__Application__reservoirE level
+ WRITE Application__reservoir 1
+ ENDFOR
+ENDTASK
+
+TASK Application__SmartphoneAppController
+ TASKOP
+ //Local variables
+ int calories
+ int glucoseLevel
+ int batteryLevel
+ int reservoirLevel
+ int pumpingStatus
+ int insulinToPump
+ int basal
+ int bolus
+ int contCriticalLevel
+ int x
+ int criticalSituation = 0
+ int i
+
+ //Behavior
+ calories=0
+ bolus=0
+ contCriticalLevel=0
+ NOTIFY Application__resetAppTimer__Application__resetAppTimer
+ FOR(i=0; i<1; i = i+1)
+ SELECTEVT
+ CASE Application__feedback4AppE__Application__feedback4AppE batteryLevel reservoirLevel pumpingStatus
+ READ Application__feedback4App 1+0 AES_CTRL
+ EXECC 100 AES_CTRL SE 100 100 0 0 - - 2
+ ENDCASE
+ CASE Application__timeout4Basal__Application__timeout4Basal
+ NOTIFY Application__pumpBasalE__Application__pumpBasalE basal
+ WRITE Application__pumpBasal 1
+ ENDCASE
+ CASE Application__timeout4Feedback__Application__timeout4Feedback
+ NOTIFY Application__feedback4InterfaceE__Application__feedback4InterfaceE glucoseLevel batteryLevel reservoirLevel
+ WRITE Application__feedback4Interface 1
+ ENDCASE
+ CASE Application__glucoseE__Application__glucoseE glucoseLevel
+ READ Application__glucose 1
+ IF (glucoseLevel==1)
+ contCriticalLevel=contCriticalLevel+1
+ IF (contCriticalLevel==10)
+ criticalSituation=1
+ NOTIFY Application__emergencySignE__Application__emergencySignE
+ EXECC 100 AES_Emergency SE 100 100 0 0 - - 1
+ WRITE Application__emergencySign 1+0 AES_Emergency
+ WAIT Application__emergencyResponseE__Application__emergencyResponseE
+ ELSE
+ ENDIF
+ ELSE
+ contCriticalLevel=0
+ criticalSituation=0
+ ENDIF
+ ENDCASE
+ CASE Application__inputCaloriesE__Application__inputCaloriesE calories
+ READ Application__inputCalories 1
+ bolus=calories
+ NOTIFY Application__pumpBolusE__Application__pumpBolusE bolus
+ WRITE Application__pumpBolus 1
+ ENDCASE
+ ENDSELECTEVT
+ ENDFOR
+ENDTASK
+
+TASK Application__SmartphoneAppInterface
+ TASKOP
+ //Local variables
+ int calories
+ int glucoseLevel
+ int batteryLevel
+ int reservoirLevel
+ int pumpingStatus
+ int loop_0 = 0
+
+ //Behavior
+ calories=0
+ NOTIFY Application__resetInterfaceTimer__Application__resetInterfaceTimer
+ FOR(loop_0 = 0; loop_0<1; loop_0 = loop_0 + 1)
+ SELECTEVT
+ CASE Application__timeout4Eat__Application__timeout4Eat
+ RANDOM 0 calories 1 3
+ NOTIFY Application__inputCaloriesE__Application__inputCaloriesE calories
+ WRITE Application__inputCalories 1
+ NOTIFY Application__resetInterfaceTimer__Application__resetInterfaceTimer
+ calories=0
+ ENDCASE
+ CASE Application__feedback4InterfaceE__Application__feedback4InterfaceE glucoseLevel batteryLevel reservoirLevel
+ READ Application__feedback4Interface 1
+ ENDCASE
+ ENDSELECTEVT
+ ENDFOR
+ENDTASK
+
diff --git a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITA01_v5/mapNoProtection/golden b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITA01_v5/mapNoProtection/golden
new file mode 100644
index 0000000000..e69de29bb2
diff --git a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITA01_v5/mapNoProtection/spec.tarchi b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITA01_v5/mapNoProtection/spec.tarchi
new file mode 100644
index 0000000000..05519c971a
--- /dev/null
+++ b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITA01_v5/mapNoProtection/spec.tarchi
@@ -0,0 +1,354 @@
+// Master clock frequency - in MHz
+MASTERCLOCKFREQUENCY 200
+
+NODE CPU PumpActuatorMCU
+SET PumpActuatorMCU nbOfCores 1
+SET PumpActuatorMCU byteDataSize 4
+SET PumpActuatorMCU pipelineSize 5
+SET PumpActuatorMCU goIdleTime 10
+SET PumpActuatorMCU maxConsecutiveIdleCycles 10
+SET PumpActuatorMCU taskSwitchingTime 20
+SET PumpActuatorMCU branchingPredictionPenalty 2
+SET PumpActuatorMCU cacheMiss 5
+SET PumpActuatorMCU schedulingPolicy 0
+SET PumpActuatorMCU sliceTime 10000
+SET PumpActuatorMCU execiTime 1
+SET PumpActuatorMCU execcTime 1
+SET PumpActuatorMCU clockDivider 1
+
+NODE BUS BT
+SET BT byteDataSize 4
+SET BT pipelineSize 1
+SET BT arbitration 0
+SET BT sliceTime 10000
+SET BT burstSize 100
+SET BT privacy public
+SET BT clockDivider 1
+
+NODE MEMORY MedicalMemory
+SET MedicalMemory byteDataSize 4
+SET MedicalMemory clockDivider 1
+
+NODE BRIDGE SmartphoneBTInterface
+SET SmartphoneBTInterface bufferByteSize 4
+SET SmartphoneBTInterface clockDivider 1
+
+NODE CPU MedicalCPU
+SET MedicalCPU nbOfCores 1
+SET MedicalCPU byteDataSize 4
+SET MedicalCPU pipelineSize 5
+SET MedicalCPU goIdleTime 10
+SET MedicalCPU maxConsecutiveIdleCycles 10
+SET MedicalCPU taskSwitchingTime 20
+SET MedicalCPU branchingPredictionPenalty 2
+SET MedicalCPU cacheMiss 5
+SET MedicalCPU schedulingPolicy 0
+SET MedicalCPU sliceTime 10000
+SET MedicalCPU execiTime 1
+SET MedicalCPU execcTime 1
+SET MedicalCPU clockDivider 1
+
+NODE BUS MedicalBus
+SET MedicalBus byteDataSize 4
+SET MedicalBus pipelineSize 1
+SET MedicalBus arbitration 0
+SET MedicalBus sliceTime 10000
+SET MedicalBus burstSize 100
+SET MedicalBus privacy public
+SET MedicalBus clockDivider 1
+
+NODE BRIDGE MedicalBridge
+SET MedicalBridge bufferByteSize 4
+SET MedicalBridge clockDivider 1
+
+NODE CPU MedicalGUIMCU
+SET MedicalGUIMCU nbOfCores 1
+SET MedicalGUIMCU byteDataSize 4
+SET MedicalGUIMCU pipelineSize 5
+SET MedicalGUIMCU goIdleTime 10
+SET MedicalGUIMCU maxConsecutiveIdleCycles 10
+SET MedicalGUIMCU taskSwitchingTime 20
+SET MedicalGUIMCU branchingPredictionPenalty 2
+SET MedicalGUIMCU cacheMiss 5
+SET MedicalGUIMCU schedulingPolicy 0
+SET MedicalGUIMCU sliceTime 10000
+SET MedicalGUIMCU execiTime 1
+SET MedicalGUIMCU execcTime 1
+SET MedicalGUIMCU clockDivider 1
+
+NODE BUS MedicalIOBus
+SET MedicalIOBus byteDataSize 4
+SET MedicalIOBus pipelineSize 1
+SET MedicalIOBus arbitration 0
+SET MedicalIOBus sliceTime 10000
+SET MedicalIOBus burstSize 100
+SET MedicalIOBus privacy public
+SET MedicalIOBus clockDivider 1
+
+NODE BRIDGE MedicalNetwork
+SET MedicalNetwork bufferByteSize 4
+SET MedicalNetwork clockDivider 1
+
+NODE MEMORY SmartphoneMemory
+SET SmartphoneMemory byteDataSize 4
+SET SmartphoneMemory clockDivider 1
+
+NODE CPU SmartphoneCPU
+SET SmartphoneCPU nbOfCores 1
+SET SmartphoneCPU byteDataSize 4
+SET SmartphoneCPU pipelineSize 5
+SET SmartphoneCPU goIdleTime 10
+SET SmartphoneCPU maxConsecutiveIdleCycles 10
+SET SmartphoneCPU taskSwitchingTime 20
+SET SmartphoneCPU branchingPredictionPenalty 2
+SET SmartphoneCPU cacheMiss 5
+SET SmartphoneCPU schedulingPolicy 0
+SET SmartphoneCPU sliceTime 10000
+SET SmartphoneCPU execiTime 1
+SET SmartphoneCPU execcTime 1
+SET SmartphoneCPU clockDivider 1
+
+NODE BUS SmartphoneBus
+SET SmartphoneBus byteDataSize 4
+SET SmartphoneBus pipelineSize 1
+SET SmartphoneBus arbitration 0
+SET SmartphoneBus sliceTime 10000
+SET SmartphoneBus burstSize 100
+SET SmartphoneBus privacy public
+SET SmartphoneBus clockDivider 1
+
+NODE BRIDGE SmartphoneBridge
+SET SmartphoneBridge bufferByteSize 4
+SET SmartphoneBridge clockDivider 1
+
+NODE CPU DisplayMCU
+SET DisplayMCU nbOfCores 1
+SET DisplayMCU byteDataSize 4
+SET DisplayMCU pipelineSize 5
+SET DisplayMCU goIdleTime 10
+SET DisplayMCU maxConsecutiveIdleCycles 10
+SET DisplayMCU taskSwitchingTime 20
+SET DisplayMCU branchingPredictionPenalty 2
+SET DisplayMCU cacheMiss 5
+SET DisplayMCU schedulingPolicy 0
+SET DisplayMCU sliceTime 10000
+SET DisplayMCU execiTime 1
+SET DisplayMCU execcTime 1
+SET DisplayMCU clockDivider 1
+
+NODE BRIDGE SmartphoneNetwork
+SET SmartphoneNetwork bufferByteSize 4
+SET SmartphoneNetwork clockDivider 1
+
+NODE BUS SmartphoneIOBus
+SET SmartphoneIOBus byteDataSize 4
+SET SmartphoneIOBus pipelineSize 1
+SET SmartphoneIOBus arbitration 0
+SET SmartphoneIOBus sliceTime 10000
+SET SmartphoneIOBus burstSize 100
+SET SmartphoneIOBus privacy public
+SET SmartphoneIOBus clockDivider 1
+
+NODE BRIDGE PumpNetwork
+SET PumpNetwork bufferByteSize 4
+SET PumpNetwork clockDivider 1
+
+NODE CPU ReservoirSensorMCU
+SET ReservoirSensorMCU nbOfCores 1
+SET ReservoirSensorMCU byteDataSize 4
+SET ReservoirSensorMCU pipelineSize 5
+SET ReservoirSensorMCU goIdleTime 10
+SET ReservoirSensorMCU maxConsecutiveIdleCycles 10
+SET ReservoirSensorMCU taskSwitchingTime 20
+SET ReservoirSensorMCU branchingPredictionPenalty 2
+SET ReservoirSensorMCU cacheMiss 5
+SET ReservoirSensorMCU schedulingPolicy 0
+SET ReservoirSensorMCU sliceTime 10000
+SET ReservoirSensorMCU execiTime 1
+SET ReservoirSensorMCU execcTime 1
+SET ReservoirSensorMCU clockDivider 1
+
+NODE CPU BatterySensorMCU
+SET BatterySensorMCU nbOfCores 1
+SET BatterySensorMCU byteDataSize 4
+SET BatterySensorMCU pipelineSize 5
+SET BatterySensorMCU goIdleTime 10
+SET BatterySensorMCU maxConsecutiveIdleCycles 10
+SET BatterySensorMCU taskSwitchingTime 20
+SET BatterySensorMCU branchingPredictionPenalty 2
+SET BatterySensorMCU cacheMiss 5
+SET BatterySensorMCU schedulingPolicy 0
+SET BatterySensorMCU sliceTime 10000
+SET BatterySensorMCU execiTime 1
+SET BatterySensorMCU execcTime 1
+SET BatterySensorMCU clockDivider 1
+
+NODE BRIDGE toPumpIOBus
+SET toPumpIOBus bufferByteSize 4
+SET toPumpIOBus clockDivider 1
+
+NODE MEMORY PumpMemory
+SET PumpMemory byteDataSize 4
+SET PumpMemory clockDivider 1
+
+NODE BUS PumpBus
+SET PumpBus byteDataSize 4
+SET PumpBus pipelineSize 1
+SET PumpBus arbitration 0
+SET PumpBus sliceTime 10000
+SET PumpBus burstSize 100
+SET PumpBus privacy public
+SET PumpBus clockDivider 1
+
+NODE CPU PumpProcessor
+SET PumpProcessor nbOfCores 1
+SET PumpProcessor byteDataSize 4
+SET PumpProcessor pipelineSize 5
+SET PumpProcessor goIdleTime 10
+SET PumpProcessor maxConsecutiveIdleCycles 10
+SET PumpProcessor taskSwitchingTime 20
+SET PumpProcessor branchingPredictionPenalty 2
+SET PumpProcessor cacheMiss 5
+SET PumpProcessor schedulingPolicy 0
+SET PumpProcessor sliceTime 10000
+SET PumpProcessor execiTime 1
+SET PumpProcessor execcTime 1
+SET PumpProcessor clockDivider 1
+
+NODE CPU GlucoseSensorMCU
+SET GlucoseSensorMCU nbOfCores 1
+SET GlucoseSensorMCU byteDataSize 4
+SET GlucoseSensorMCU pipelineSize 5
+SET GlucoseSensorMCU goIdleTime 10
+SET GlucoseSensorMCU maxConsecutiveIdleCycles 10
+SET GlucoseSensorMCU taskSwitchingTime 20
+SET GlucoseSensorMCU branchingPredictionPenalty 2
+SET GlucoseSensorMCU cacheMiss 5
+SET GlucoseSensorMCU schedulingPolicy 0
+SET GlucoseSensorMCU sliceTime 10000
+SET GlucoseSensorMCU execiTime 1
+SET GlucoseSensorMCU execcTime 1
+SET GlucoseSensorMCU clockDivider 1
+
+NODE BUS InterconnectionNetwork
+SET InterconnectionNetwork byteDataSize 4
+SET InterconnectionNetwork pipelineSize 1
+SET InterconnectionNetwork arbitration 0
+SET InterconnectionNetwork sliceTime 10000
+SET InterconnectionNetwork burstSize 100
+SET InterconnectionNetwork privacy public
+SET InterconnectionNetwork clockDivider 1
+
+NODE BUS PumpIOBus
+SET PumpIOBus byteDataSize 1
+SET PumpIOBus pipelineSize 1
+SET PumpIOBus arbitration 0
+SET PumpIOBus sliceTime 10000
+SET PumpIOBus burstSize 100
+SET PumpIOBus privacy public
+SET PumpIOBus clockDivider 1
+
+NODE LINK link_SmartphoneBTInterface_to_SmartphoneIOBus
+SET link_SmartphoneBTInterface_to_SmartphoneIOBus node SmartphoneBTInterface
+SET link_SmartphoneBTInterface_to_SmartphoneIOBus bus SmartphoneIOBus
+SET link_SmartphoneBTInterface_to_SmartphoneIOBus priority 0
+NODE LINK link_GlucoseSensorMCU_to_BT
+SET link_GlucoseSensorMCU_to_BT node GlucoseSensorMCU
+SET link_GlucoseSensorMCU_to_BT bus BT
+SET link_GlucoseSensorMCU_to_BT priority 0
+NODE LINK link_PumpActuatorMCU_to_PumpIOBus
+SET link_PumpActuatorMCU_to_PumpIOBus node PumpActuatorMCU
+SET link_PumpActuatorMCU_to_PumpIOBus bus PumpIOBus
+SET link_PumpActuatorMCU_to_PumpIOBus priority 0
+NODE LINK link_SmartphoneBTInterface_to_BT
+SET link_SmartphoneBTInterface_to_BT node SmartphoneBTInterface
+SET link_SmartphoneBTInterface_to_BT bus BT
+SET link_SmartphoneBTInterface_to_BT priority 0
+NODE LINK link_MedicalMemory_to_MedicalBus
+SET link_MedicalMemory_to_MedicalBus node MedicalMemory
+SET link_MedicalMemory_to_MedicalBus bus MedicalBus
+SET link_MedicalMemory_to_MedicalBus priority 0
+NODE LINK link_MedicalCPU_to_MedicalBus
+SET link_MedicalCPU_to_MedicalBus node MedicalCPU
+SET link_MedicalCPU_to_MedicalBus bus MedicalBus
+SET link_MedicalCPU_to_MedicalBus priority 0
+NODE LINK link_MedicalBridge_to_MedicalBus
+SET link_MedicalBridge_to_MedicalBus node MedicalBridge
+SET link_MedicalBridge_to_MedicalBus bus MedicalBus
+SET link_MedicalBridge_to_MedicalBus priority 0
+NODE LINK link_MedicalBridge_to_MedicalIOBus
+SET link_MedicalBridge_to_MedicalIOBus node MedicalBridge
+SET link_MedicalBridge_to_MedicalIOBus bus MedicalIOBus
+SET link_MedicalBridge_to_MedicalIOBus priority 0
+NODE LINK link_MedicalGUIMCU_to_MedicalIOBus
+SET link_MedicalGUIMCU_to_MedicalIOBus node MedicalGUIMCU
+SET link_MedicalGUIMCU_to_MedicalIOBus bus MedicalIOBus
+SET link_MedicalGUIMCU_to_MedicalIOBus priority 0
+NODE LINK link_MedicalNetwork_to_MedicalIOBus
+SET link_MedicalNetwork_to_MedicalIOBus node MedicalNetwork
+SET link_MedicalNetwork_to_MedicalIOBus bus MedicalIOBus
+SET link_MedicalNetwork_to_MedicalIOBus priority 0
+NODE LINK link_MedicalNetwork_to_InterconnectionNetwork
+SET link_MedicalNetwork_to_InterconnectionNetwork node MedicalNetwork
+SET link_MedicalNetwork_to_InterconnectionNetwork bus InterconnectionNetwork
+SET link_MedicalNetwork_to_InterconnectionNetwork priority 0
+NODE LINK link_SmartphoneMemory_to_SmartphoneBus
+SET link_SmartphoneMemory_to_SmartphoneBus node SmartphoneMemory
+SET link_SmartphoneMemory_to_SmartphoneBus bus SmartphoneBus
+SET link_SmartphoneMemory_to_SmartphoneBus priority 0
+NODE LINK link_SmartphoneCPU_to_SmartphoneBus
+SET link_SmartphoneCPU_to_SmartphoneBus node SmartphoneCPU
+SET link_SmartphoneCPU_to_SmartphoneBus bus SmartphoneBus
+SET link_SmartphoneCPU_to_SmartphoneBus priority 0
+NODE LINK link_SmartphoneBridge_to_SmartphoneBus
+SET link_SmartphoneBridge_to_SmartphoneBus node SmartphoneBridge
+SET link_SmartphoneBridge_to_SmartphoneBus bus SmartphoneBus
+SET link_SmartphoneBridge_to_SmartphoneBus priority 0
+NODE LINK link_SmartphoneBridge_to_SmartphoneIOBus
+SET link_SmartphoneBridge_to_SmartphoneIOBus node SmartphoneBridge
+SET link_SmartphoneBridge_to_SmartphoneIOBus bus SmartphoneIOBus
+SET link_SmartphoneBridge_to_SmartphoneIOBus priority 0
+NODE LINK link_DisplayMCU_to_SmartphoneIOBus
+SET link_DisplayMCU_to_SmartphoneIOBus node DisplayMCU
+SET link_DisplayMCU_to_SmartphoneIOBus bus SmartphoneIOBus
+SET link_DisplayMCU_to_SmartphoneIOBus priority 0
+NODE LINK link_SmartphoneNetwork_to_SmartphoneIOBus
+SET link_SmartphoneNetwork_to_SmartphoneIOBus node SmartphoneNetwork
+SET link_SmartphoneNetwork_to_SmartphoneIOBus bus SmartphoneIOBus
+SET link_SmartphoneNetwork_to_SmartphoneIOBus priority 0
+NODE LINK link_PumpMemory_to_PumpBus
+SET link_PumpMemory_to_PumpBus node PumpMemory
+SET link_PumpMemory_to_PumpBus bus PumpBus
+SET link_PumpMemory_to_PumpBus priority 0
+NODE LINK link_PumpProcessor_to_PumpBus
+SET link_PumpProcessor_to_PumpBus node PumpProcessor
+SET link_PumpProcessor_to_PumpBus bus PumpBus
+SET link_PumpProcessor_to_PumpBus priority 0
+NODE LINK link_toPumpIOBus_to_PumpBus
+SET link_toPumpIOBus_to_PumpBus node toPumpIOBus
+SET link_toPumpIOBus_to_PumpBus bus PumpBus
+SET link_toPumpIOBus_to_PumpBus priority 0
+NODE LINK link_toPumpIOBus_to_PumpIOBus
+SET link_toPumpIOBus_to_PumpIOBus node toPumpIOBus
+SET link_toPumpIOBus_to_PumpIOBus bus PumpIOBus
+SET link_toPumpIOBus_to_PumpIOBus priority 0
+NODE LINK link_BatterySensorMCU_to_PumpIOBus
+SET link_BatterySensorMCU_to_PumpIOBus node BatterySensorMCU
+SET link_BatterySensorMCU_to_PumpIOBus bus PumpIOBus
+SET link_BatterySensorMCU_to_PumpIOBus priority 0
+NODE LINK link_ReservoirSensorMCU_to_PumpIOBus
+SET link_ReservoirSensorMCU_to_PumpIOBus node ReservoirSensorMCU
+SET link_ReservoirSensorMCU_to_PumpIOBus bus PumpIOBus
+SET link_ReservoirSensorMCU_to_PumpIOBus priority 0
+NODE LINK link_PumpNetwork_to_PumpIOBus
+SET link_PumpNetwork_to_PumpIOBus node PumpNetwork
+SET link_PumpNetwork_to_PumpIOBus bus PumpIOBus
+SET link_PumpNetwork_to_PumpIOBus priority 0
+NODE LINK link_PumpNetwork_to_InterconnectionNetwork
+SET link_PumpNetwork_to_InterconnectionNetwork node PumpNetwork
+SET link_PumpNetwork_to_InterconnectionNetwork bus InterconnectionNetwork
+SET link_PumpNetwork_to_InterconnectionNetwork priority 0
+NODE LINK link_SmartphoneNetwork_to_InterconnectionNetwork
+SET link_SmartphoneNetwork_to_InterconnectionNetwork node SmartphoneNetwork
+SET link_SmartphoneNetwork_to_InterconnectionNetwork bus InterconnectionNetwork
+SET link_SmartphoneNetwork_to_InterconnectionNetwork priority 0
diff --git a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITA01_v5/mapNoProtection/spec.tmap b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITA01_v5/mapNoProtection/spec.tmap
new file mode 100644
index 0000000000..d7362175aa
--- /dev/null
+++ b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITA01_v5/mapNoProtection/spec.tmap
@@ -0,0 +1,36 @@
+TMLSPEC
+ #include "spec.tml"
+ENDTMLSPEC
+
+TMLARCHI
+ #include "spec.tarchi"
+ENDTMLARCHI
+
+TMLMAPPING
+ MAP PumpActuatorMCU Application__PumpActuator
+ SET Application__PumpActuator priority 0
+ MAP PumpActuatorMCU Application__AppControllerTimer
+ SET Application__AppControllerTimer priority 0
+ MAP PumpActuatorMCU Application__AppControllerTimerBasal
+ SET Application__AppControllerTimerBasal priority 0
+ MAP MedicalCPU Application__MedicalInformationSystem
+ SET Application__MedicalInformationSystem priority 0
+ MAP SmartphoneCPU Application__SmartphoneAppController
+ SET Application__SmartphoneAppController priority 0
+ MAP SmartphoneCPU Application__AppInterfaceTimer
+ SET Application__AppInterfaceTimer priority 0
+ MAP DisplayMCU Application__SmartphoneAppInterface
+ SET Application__SmartphoneAppInterface priority 0
+ MAP ReservoirSensorMCU Application__ReservoirSensor
+ SET Application__ReservoirSensor priority 0
+ MAP BatterySensorMCU Application__BatterySensor
+ SET Application__BatterySensor priority 0
+ MAP PumpProcessor Application__PumpController
+ SET Application__PumpController priority 0
+ MAP PumpProcessor Application__PumpControllerTimer
+ SET Application__PumpControllerTimer priority 0
+ MAP GlucoseSensorMCU Application__GlucoseLevelSensor
+ SET Application__GlucoseLevelSensor priority 0
+ MAPSEC SmartphoneMemory AES_CTRL
+ MAPSEC MedicalMemory AES_Emergency
+ENDTMLMAPPING
diff --git a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITA01_v5/mapNoProtection/spec.tml b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITA01_v5/mapNoProtection/spec.tml
new file mode 100644
index 0000000000..e21f9ea3a3
--- /dev/null
+++ b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/Models/ITA01_v5/mapNoProtection/spec.tml
@@ -0,0 +1,338 @@
+// TML Application - FORMAT 0.2
+// Application: /media/sf_vbox_shared/ITA01_v5.xml
+// Generated: Wed Dec 27 10:01:13 EST 2023
+
+// PRAGMAS
+
+// Channels
+CHANNEL Application__battery BRBW 40 8 OUT Application__BatterySensor IN Application__PumpController
+VCCHANNEL Application__battery 0
+CONFCHANNEL Application__battery
+CHANNEL Application__emergencySign BRBW 40 8 OUT Application__SmartphoneAppController IN Application__MedicalInformationSystem
+VCCHANNEL Application__emergencySign 0
+CONFCHANNEL Application__emergencySign
+AUTHCHANNEL Application__emergencySign
+CHANNEL Application__feedback4App BRBW 40 8 OUT Application__PumpController IN Application__SmartphoneAppController
+VCCHANNEL Application__feedback4App 0
+CONFCHANNEL Application__feedback4App
+AUTHCHANNEL Application__feedback4App
+CHANNEL Application__feedback4Interface BRBW 40 8 OUT Application__SmartphoneAppController IN Application__SmartphoneAppInterface
+VCCHANNEL Application__feedback4Interface 0
+CHANNEL Application__glucose BRBW 40 8 OUT Application__GlucoseLevelSensor IN Application__SmartphoneAppController
+VCCHANNEL Application__glucose 0
+CHANNEL Application__inputCalories BRBW 40 1 OUT Application__SmartphoneAppInterface IN Application__SmartphoneAppController
+VCCHANNEL Application__inputCalories 0
+CHANNEL Application__pumpBasal BRBW 40 8 OUT Application__SmartphoneAppController IN Application__PumpController
+VCCHANNEL Application__pumpBasal 0
+CHANNEL Application__pumpBolus BRBW 40 8 OUT Application__SmartphoneAppController IN Application__PumpController
+VCCHANNEL Application__pumpBolus 0
+CHANNEL Application__reservoir BRNBW 40 OUT Application__ReservoirSensor IN Application__PumpController
+VCCHANNEL Application__reservoir 0
+
+// Events
+EVENT Application__batteryE__Application__batteryE(int) NIB 8 Application__BatterySensor Application__PumpController
+EVENT Application__emergencyResponseE__Application__emergencyResponseE() NIB 8 Application__MedicalInformationSystem Application__SmartphoneAppController
+EVENT Application__emergencySignE__Application__emergencySignE() NIB 8 Application__SmartphoneAppController Application__MedicalInformationSystem
+EVENT Application__feedback4AppE__Application__feedback4AppE(int, int, int) NIB 8 Application__PumpController Application__SmartphoneAppController
+EVENT Application__feedback4InterfaceE__Application__feedback4InterfaceE(int, int, int) NIB 8 Application__SmartphoneAppController Application__SmartphoneAppInterface
+EVENT Application__glucoseE__Application__glucoseE(int) NIB 8 Application__GlucoseLevelSensor Application__SmartphoneAppController
+EVENT Application__inputCaloriesE__Application__inputCaloriesE(int) NIB 8 Application__SmartphoneAppInterface Application__SmartphoneAppController
+EVENT Application__pumpBasalE__Application__pumpBasalE(int) NIB 8 Application__SmartphoneAppController Application__PumpController
+EVENT Application__pumpBolusE__Application__pumpBolusE(int) NIB 8 Application__SmartphoneAppController Application__PumpController
+EVENT Application__reservoirE__Application__reservoirE(int) NIB 8 Application__ReservoirSensor Application__PumpController
+EVENT Application__resetAppTimerBasal__Application__resetAppTimerBasal() NIB 8 Application__SmartphoneAppController Application__AppControllerTimerBasal
+EVENT Application__resetAppTimer__Application__resetAppTimer() NIB 8 Application__SmartphoneAppController Application__AppControllerTimer
+EVENT Application__resetInterfaceTimer__Application__resetInterfaceTimer() NIB 8 Application__SmartphoneAppInterface Application__AppInterfaceTimer
+EVENT Application__resetTimer__Application__resetTimer() NIB 8 Application__PumpController Application__PumpControllerTimer
+EVENT Application__startPumping__Application__startPumping() NIB 8 Application__PumpController Application__PumpActuator
+EVENT Application__stopPumping__Application__stopPumping() NIB 8 Application__PumpController Application__PumpActuator
+EVENT Application__timeout4Basal__Application__timeout4Basal() NIB 8 Application__AppControllerTimerBasal Application__SmartphoneAppController
+EVENT Application__timeout4CtrlFeedback__Application__timeout4CtrlFeeback() NIB 8 Application__PumpControllerTimer Application__PumpController
+EVENT Application__timeout4Eat__Application__timeout4Eat() NIB 8 Application__AppInterfaceTimer Application__SmartphoneAppInterface
+EVENT Application__timeout4Feedback__Application__timeout4Feedback() NIB 8 Application__AppControllerTimer Application__SmartphoneAppController
+
+// Requests
+
+TASK Application__AppControllerTimer
+ TASKOP
+ //Local variables
+ int loop_0 = 0
+
+ //Behavior
+ FOR(loop_0 = 0; loop_0<1; loop_0 = loop_0 + 1)
+ WAIT Application__resetAppTimer__Application__resetAppTimer
+ DELAY 10 ms isActiveDelay false
+ NOTIFY Application__timeout4Feedback__Application__timeout4Feedback
+ ENDFOR
+ENDTASK
+
+TASK Application__AppControllerTimerBasal
+ TASKOP
+ //Local variables
+ int loop_0 = 0
+
+ //Behavior
+ FOR(loop_0 = 0; loop_0<1; loop_0 = loop_0 + 1)
+ WAIT Application__resetAppTimerBasal__Application__resetAppTimerBasal
+ DELAY 10 ms isActiveDelay false
+ NOTIFY Application__timeout4Basal__Application__timeout4Basal
+ ENDFOR
+ENDTASK
+
+TASK Application__AppInterfaceTimer
+ TASKOP
+ //Local variables
+ int loop_0 = 0
+
+ //Behavior
+ FOR(loop_0 = 0; loop_0<1; loop_0 = loop_0 + 1)
+ WAIT Application__resetInterfaceTimer__Application__resetInterfaceTimer
+ DELAY 100 ms isActiveDelay false
+ NOTIFY Application__timeout4Eat__Application__timeout4Eat
+ ENDFOR
+ENDTASK
+
+TASK Application__BatterySensor
+ TASKOP
+ //Local variables
+ int level
+ int loop_0 = 0
+
+ //Behavior
+ FOR(loop_0 = 0; loop_0<1; loop_0 = loop_0 + 1)
+ DELAY 10 ms isActiveDelay false
+ RANDOM 0 level 0 2
+ NOTIFY Application__batteryE__Application__batteryE level
+ WRITE Application__battery 1
+ ENDFOR
+ENDTASK
+
+TASK Application__GlucoseLevelSensor
+ TASKOP
+ //Local variables
+ int level
+ int loop_0 = 0
+
+ //Behavior
+ FOR(loop_0 = 0; loop_0<1; loop_0 = loop_0 + 1)
+ DELAY 10 ms isActiveDelay false
+ RANDOM 0 level 1 3
+ NOTIFY Application__glucoseE__Application__glucoseE level
+ WRITE Application__glucose 1
+ ENDFOR
+ENDTASK
+
+TASK Application__MedicalInformationSystem
+ TASKOP
+ //Local variables
+ int loop_0 = 0
+
+ //Behavior
+ FOR(loop_0 = 0; loop_0<1; loop_0 = loop_0 + 1)
+ WAIT Application__emergencySignE__Application__emergencySignE
+ EXECC 100 AES_Emergency SE 100 100 0 0 - - 2
+ READ Application__emergencySign 1+0 AES_Emergency
+ EXECI 5000
+ NOTIFY Application__emergencyResponseE__Application__emergencyResponseE
+ ENDFOR
+ENDTASK
+
+TASK Application__PumpActuator
+ TASKOP
+ //Local variables
+ int loop_0 = 0
+
+ //Behavior
+ FOR(loop_0 = 0; loop_0<1; loop_0 = loop_0 + 1)
+ SELECTEVT
+ CASE Application__startPumping__Application__startPumping
+ EXECI 10000
+ ENDCASE
+ CASE Application__stopPumping__Application__stopPumping
+ EXECI 10000
+ ENDCASE
+ ENDSELECTEVT
+ ENDFOR
+ENDTASK
+
+TASK Application__PumpController
+ TASKOP
+ //Local variables
+ int batteryLevel = 2
+ int reservoirLevel = 2
+ int pumpingStatus = 0
+ int basal
+ int bolus
+ int insulineToPump = 0
+ int i
+ int x
+ int loop_0 = 0
+
+ //Behavior
+ NOTIFY Application__resetTimer__Application__resetTimer
+ FOR(loop_0 = 0; loop_0<10; loop_0 = loop_0 + 1)
+ SELECTEVT
+ CASE Application__timeout4CtrlFeedback__Application__timeout4CtrlFeeback
+ NOTIFY Application__feedback4AppE__Application__feedback4AppE batteryLevel reservoirLevel pumpingStatus
+ EXECC 100 AES_CTRL SE 100 100 0 0 - - 1
+ WRITE Application__feedback4App 1+0 AES_CTRL
+ ENDCASE
+ CASE Application__reservoirE__Application__reservoirE reservoirLevel
+ READ Application__reservoir 1
+ ENDCASE
+ CASE Application__batteryE__Application__batteryE batteryLevel
+ READ Application__battery 1
+ ENDCASE
+ CASE Application__pumpBolusE__Application__pumpBolusE bolus
+ READ Application__pumpBolus 1
+ IF (pumpingStatus==1)
+ NOTIFY Application__stopPumping__Application__stopPumping
+ pumpingStatus=0
+ ELSE
+ ENDIF
+ insulineToPump=insulineToPump+bolus*10
+ NOTIFY Application__startPumping__Application__startPumping
+ pumpingStatus=1
+ FOR(i=insulineToPump; i>0; i=i-1)
+ DELAY 1 ms isActiveDelay false
+ ENDFOR
+ NOTIFY Application__stopPumping__Application__stopPumping
+ pumpingStatus=0
+ ENDCASE
+ CASE Application__pumpBasalE__Application__pumpBasalE basal
+ READ Application__pumpBasal 1
+ IF (pumpingStatus==0)
+ insulineToPump=5
+ NOTIFY Application__startPumping__Application__startPumping
+ pumpingStatus=1
+ FOR(i=insulineToPump; i>0; i=i-1)
+ DELAY 1 ms isActiveDelay false
+ ENDFOR
+ NOTIFY Application__stopPumping__Application__stopPumping
+ pumpingStatus=0
+ ELSE
+ ENDIF
+ ENDCASE
+ ENDSELECTEVT
+ ENDFOR
+ENDTASK
+
+TASK Application__PumpControllerTimer
+ TASKOP
+ //Local variables
+ int loop_0 = 0
+
+ //Behavior
+ FOR(loop_0 = 0; loop_0<1; loop_0 = loop_0 + 1)
+ WAIT Application__resetTimer__Application__resetTimer
+ DELAY 10 ms isActiveDelay false
+ NOTIFY Application__timeout4CtrlFeedback__Application__timeout4CtrlFeeback
+ ENDFOR
+ENDTASK
+
+TASK Application__ReservoirSensor
+ TASKOP
+ //Local variables
+ int level
+ int loop_0 = 0
+
+ //Behavior
+ FOR(loop_0 = 0; loop_0<1; loop_0 = loop_0 + 1)
+ DELAY 10 ms isActiveDelay false
+ RANDOM 0 level 0 2
+ NOTIFY Application__reservoirE__Application__reservoirE level
+ WRITE Application__reservoir 1
+ ENDFOR
+ENDTASK
+
+TASK Application__SmartphoneAppController
+ TASKOP
+ //Local variables
+ int calories
+ int glucoseLevel
+ int batteryLevel
+ int reservoirLevel
+ int pumpingStatus
+ int insulinToPump
+ int basal
+ int bolus
+ int contCriticalLevel
+ int x
+ int criticalSituation = 0
+ int i
+
+ //Behavior
+ calories=0
+ bolus=0
+ contCriticalLevel=0
+ NOTIFY Application__resetAppTimer__Application__resetAppTimer
+ FOR(i=0; i<1; i = i+1)
+ SELECTEVT
+ CASE Application__feedback4AppE__Application__feedback4AppE batteryLevel reservoirLevel pumpingStatus
+ READ Application__feedback4App 1+0 AES_CTRL
+ EXECC 100 AES_CTRL SE 100 100 0 0 - - 2
+ ENDCASE
+ CASE Application__timeout4Basal__Application__timeout4Basal
+ NOTIFY Application__pumpBasalE__Application__pumpBasalE basal
+ WRITE Application__pumpBasal 1
+ ENDCASE
+ CASE Application__timeout4Feedback__Application__timeout4Feedback
+ NOTIFY Application__feedback4InterfaceE__Application__feedback4InterfaceE glucoseLevel batteryLevel reservoirLevel
+ WRITE Application__feedback4Interface 1
+ ENDCASE
+ CASE Application__glucoseE__Application__glucoseE glucoseLevel
+ READ Application__glucose 1
+ IF (glucoseLevel==1)
+ contCriticalLevel=contCriticalLevel+1
+ IF (contCriticalLevel==10)
+ criticalSituation=1
+ NOTIFY Application__emergencySignE__Application__emergencySignE
+ EXECC 100 AES_Emergency SE 100 100 0 0 - - 1
+ WRITE Application__emergencySign 1+0 AES_Emergency
+ WAIT Application__emergencyResponseE__Application__emergencyResponseE
+ ELSE
+ ENDIF
+ ELSE
+ contCriticalLevel=0
+ criticalSituation=0
+ ENDIF
+ ENDCASE
+ CASE Application__inputCaloriesE__Application__inputCaloriesE calories
+ READ Application__inputCalories 1
+ bolus=calories
+ NOTIFY Application__pumpBolusE__Application__pumpBolusE bolus
+ WRITE Application__pumpBolus 1
+ ENDCASE
+ ENDSELECTEVT
+ ENDFOR
+ENDTASK
+
+TASK Application__SmartphoneAppInterface
+ TASKOP
+ //Local variables
+ int calories
+ int glucoseLevel
+ int batteryLevel
+ int reservoirLevel
+ int pumpingStatus
+ int loop_0 = 0
+
+ //Behavior
+ calories=0
+ NOTIFY Application__resetInterfaceTimer__Application__resetInterfaceTimer
+ FOR(loop_0 = 0; loop_0<1; loop_0 = loop_0 + 1)
+ SELECTEVT
+ CASE Application__timeout4Eat__Application__timeout4Eat
+ RANDOM 0 calories 1 3
+ NOTIFY Application__inputCaloriesE__Application__inputCaloriesE calories
+ WRITE Application__inputCalories 1
+ NOTIFY Application__resetInterfaceTimer__Application__resetInterfaceTimer
+ calories=0
+ ENDCASE
+ CASE Application__feedback4InterfaceE__Application__feedback4InterfaceE glucoseLevel batteryLevel reservoirLevel
+ READ Application__feedback4Interface 1
+ ENDCASE
+ ENDSELECTEVT
+ ENDFOR
+ENDTASK
+
--
GitLab