From 0fd86801fd8f28e0700be13316595fba532e2f06 Mon Sep 17 00:00:00 2001
From: Ludovic Apvrille <ludovic.apvrille@telecom-paristech.fr>
Date: Thu, 16 Dec 2010 15:55:26 +0000
Subject: [PATCH] UPDATE ib AVATAR: ProVerif analysis of Authenticity
---
src/Main.java | 5 +-
.../AvatarActionOnSignal.java | 2 +-
.../AvatarSpecificationSimulation.java | 85 +++-
src/proverifspec/ProVerifOutputAnalyzer.java | 33 ++
.../JDialogAvatarSimulationGeneration.java | 375 +++++++++---------
src/ui/window/JDialogProVerifGeneration.java | 14 +-
6 files changed, 321 insertions(+), 193 deletions(-)
diff --git a/src/Main.java b/src/Main.java
index b6a2daa18c..8fb4898176 100755
--- a/src/Main.java
+++ b/src/Main.java
@@ -148,6 +148,7 @@ public class Main implements ActionListener {
// Analyzing arguments
String config = "config.xml";
+ startLauncher = true;
for(int i=0; i<args.length; i++) {
if (args[i].compareTo("-systemc") == 0) {
systemc = true;
@@ -163,7 +164,9 @@ public class Main implements ActionListener {
}
if (args[i].compareTo("-launcher") == 0) {
startLauncher = true;
-
+ }
+ if (args[i].compareTo("-nolauncher") == 0) {
+ startLauncher = false;
}
if (args[i].compareTo("-diplodocus") == 0) {
systemc = true;
diff --git a/src/avatartranslator/AvatarActionOnSignal.java b/src/avatartranslator/AvatarActionOnSignal.java
index 28309be48b..53a13f4b55 100644
--- a/src/avatartranslator/AvatarActionOnSignal.java
+++ b/src/avatartranslator/AvatarActionOnSignal.java
@@ -91,7 +91,7 @@ public class AvatarActionOnSignal extends AvatarStateMachineElement {
}
public AvatarActionOnSignal basicCloneMe() {
- TraceManager.addDev("I HAVE BEEN CLONED: " + this);
+ //TraceManager.addDev("I HAVE BEEN CLONED: " + this);
AvatarActionOnSignal aaos = new AvatarActionOnSignal(getName() + "__clone", getSignal(), getReferenceObject(), isCheckable());
for(int i=0; i<getNbOfValues(); i++) {
aaos.addValue(getValue(i));
diff --git a/src/avatartranslator/directsimulation/AvatarSpecificationSimulation.java b/src/avatartranslator/directsimulation/AvatarSpecificationSimulation.java
index a84e2a9b41..09ac7c6c3b 100644
--- a/src/avatartranslator/directsimulation/AvatarSpecificationSimulation.java
+++ b/src/avatartranslator/directsimulation/AvatarSpecificationSimulation.java
@@ -49,29 +49,104 @@ package avatartranslator.directsimulation;
import java.util.*;
+import avatartranslator.*;
import myutil.*;
+
public class AvatarSpecificationSimulation {
+
+ private static int MAX_TRANSACTION_IN_A_ROW = 1000;
- private AvatarSpecification avspc;
+ private AvatarSpecification avspec;
+ private long clockValue;
+ private LinkedList<AvatarSimulationBlock> blocks;
+ private LinkedList<AvatarActionOnSignal> asynchronousMessages;
+ private LinkedList<AvatarSimulationTransaction> pendingTransactions;
+ private LinkedList<AvatarSimulationTransaction> allTransactions;
public AvatarSpecificationSimulation(AvatarSpecification _avspec) {
- avspec = _avpec;
+ avspec = _avspec;
}
public void initialize() {
- // Remove internal states
+ // Remove composite states
+ avspec.removeCompositeStates();
+
+ // Remove timers
+ avspec.removeTimers();
+
+ // Reinit clock
+ clockValue = 0;
- //
+ // Reinit simulation
+ AvatarSimulationTransaction.reinit();
+ // Create all simulation blocks
+ blocks = new LinkedList<AvatarSimulationBlock>();
+ for(AvatarBlock block: avspec.getListOfBlocks()) {
+ AvatarSimulationBlock asb = new AvatarSimulationBlock(block);
+ blocks.add(asb);
+ }
+
+ // Create all simulation asynchronous channels
+ asynchronousMessages = new LinkedList<AvatarActionOnSignal>();
+
+ // Create the structure for pending and executed transactions
+ pendingTransactions = new LinkedList<AvatarSimulationTransaction>();
+ allTransactions = new LinkedList<AvatarSimulationTransaction>();
}
public boolean isInDeadlock() {
return true;
}
- public void goOneStep() {
+ public void runSimulation() {
+ int index[];
+ LinkedList<AvatarSimulationTransaction> selectedTransactions;
+
+ TraceManager.addDev("Simulation started at time: " + clockValue);
+ boolean go = true;
+ while(go == true) {
+ gatherPendingTransactions();
+
+ if (pendingTransactions.size() == 0) {
+ go = false;
+ TraceManager.addDev("No more pending transactions");
+ } else {
+ selectedTransactions = selectTransactions(pendingTransactions);
+
+ if (selectedTransactions.size() == 0) {
+ go = false;
+ TraceManager.addDev("Deadlock: no transaction can be selected");
+ } else {
+ TraceManager.addDev("Nb of selected transactions: " + selectedTransactions.size());
+ }
+
+ }
+ }
+
+ TraceManager.addDev("Simulation finished at time: " + clockValue);
+
+ printExecutedTransactions();
+ }
+
+ public void gatherPendingTransactions() {
+ pendingTransactions.clear();
+ // Gather all pending transactions from blocks
+ for(AvatarSimulationBlock asb: blocks) {
+ pendingTransactions.addAll(asb.getPendingTransactions(allTransactions, clockValue, MAX_TRANSACTION_IN_A_ROW));
+ }
}
+ public LinkedList<AvatarSimulationTransaction> selectTransactions(LinkedList<AvatarSimulationTransaction> _pendingTransactions) {
+ LinkedList<AvatarSimulationTransaction> ll = new LinkedList<AvatarSimulationTransaction>();
+ return ll;
+ }
+
+ public void printExecutedTransactions() {
+ for(AvatarSimulationTransaction ast: allTransactions) {
+ TraceManager.addDev(ast.toString() + "\n");
+ }
+ }
}
\ No newline at end of file
diff --git a/src/proverifspec/ProVerifOutputAnalyzer.java b/src/proverifspec/ProVerifOutputAnalyzer.java
index 05190238d0..fc2a80492a 100644
--- a/src/proverifspec/ProVerifOutputAnalyzer.java
+++ b/src/proverifspec/ProVerifOutputAnalyzer.java
@@ -58,6 +58,8 @@ public class ProVerifOutputAnalyzer {
private LinkedList<String> nonReachableEvents;
private LinkedList<String> secretTerms;
private LinkedList<String> nonSecretTerms;
+ private LinkedList<String> satisfiedAuthenticity;
+ private LinkedList<String> nonSatisfiedAuthenticity;
private LinkedList<String> errors;
private LinkedList<String> notproved;
@@ -68,6 +70,8 @@ public class ProVerifOutputAnalyzer {
nonReachableEvents = new LinkedList<String>();
secretTerms = new LinkedList<String>();
nonSecretTerms = new LinkedList<String>();
+ satisfiedAuthenticity = new LinkedList<String>();
+ nonSatisfiedAuthenticity = new LinkedList<String>();
errors = new LinkedList<String>();
notproved = new LinkedList<String>();
@@ -102,6 +106,27 @@ public class ProVerifOutputAnalyzer {
nonSecretTerms.add(str.substring(index0+20, index1));
}
+ index0 = str.indexOf("RESULT evinj:");
+ index1 = str.indexOf("is true");
+ if ((index0 < index1) && (index0 != -1) && (index1 != -1)) {
+ String tmp = str.substring(index0+27, index1);
+ int index2 = tmp.indexOf('(');
+ if (index2 != -1) {
+ tmp = tmp.substring(0, index2);
+ }
+ index2 = tmp.lastIndexOf("__");
+ if (index2 != -1) {
+ tmp = tmp.substring(0, index2);
+ }
+ satisfiedAuthenticity.add(tmp);
+ }
+
+ index0 = str.indexOf("RESULT evinj:");
+ index1 = str.indexOf("is false");
+ if ((index0 < index1) && (index0 != -1) && (index1 != -1)) {
+ nonSatisfiedAuthenticity.add(str.substring(index0+27, index1));
+ }
+
index0 = str.indexOf("Error:");
if (index0 != -1) {
errors.add(str + ": " + previous);
@@ -137,6 +162,14 @@ public class ProVerifOutputAnalyzer {
return nonSecretTerms;
}
+ public LinkedList<String> getSatisfiedAuthenticity() {
+ return satisfiedAuthenticity;
+ }
+
+ public LinkedList<String> getNonSatisfiedAuthenticity() {
+ return nonSatisfiedAuthenticity;
+ }
+
public LinkedList<String> getErrors() {
return errors;
}
diff --git a/src/ui/window/JDialogAvatarSimulationGeneration.java b/src/ui/window/JDialogAvatarSimulationGeneration.java
index 78a22a8f9b..c75f08f283 100644
--- a/src/ui/window/JDialogAvatarSimulationGeneration.java
+++ b/src/ui/window/JDialogAvatarSimulationGeneration.java
@@ -1,48 +1,48 @@
/**Copyright or (C) or Copr. GET / ENST, Telecom-Paris, Ludovic Apvrille
- *
- * ludovic.apvrille AT enst.fr
- *
- * This software is a computer program whose purpose is to allow the
- * edition of TURTLE analysis, design and deployment diagrams, to
- * allow the generation of RT-LOTOS or Java code from this diagram,
- * and at last to allow the analysis of formal validation traces
- * obtained from external tools, e.g. RTL from LAAS-CNRS and CADP
- * from INRIA Rhone-Alpes.
- *
- * This software is governed by the CeCILL license under French law and
- * abiding by the rules of distribution of free software. You can use,
- * modify and/ or redistribute the software under the terms of the CeCILL
- * license as circulated by CEA, CNRS and INRIA at the following URL
- * "http://www.cecill.info".
- *
- * As a counterpart to the access to the source code and rights to copy,
- * modify and redistribute granted by the license, users are provided only
- * with a limited warranty and the software's author, the holder of the
- * economic rights, and the successive licensors have only limited
- * liability.
- *
- * In this respect, the user's attention is drawn to the risks associated
- * with loading, using, modifying and/or developing or reproducing the
- * software by the user in light of its specific status of free software,
- * that may mean that it is complicated to manipulate, and that also
- * therefore means that it is reserved for developers and experienced
- * professionals having in-depth computer knowledge. Users are therefore
- * encouraged to load and test the software's suitability as regards their
- * requirements in conditions enabling the security of their systems and/or
- * data to be ensured and, more generally, to use and operate it in the
- * same conditions as regards security.
- *
- * The fact that you are presently reading this means that you have had
- * knowledge of the CeCILL license and that you accept its terms.
- *
- * /**
- * Class JDialogAvatarSimulationGeneration
- * Dialog for managing the generation and compilation of AVATAR simulation code
- * Creation: 10/12/2010
- * @version 1.1 10/12/2010
- * @author Ludovic APVRILLE
- * @see
- */
+*
+* ludovic.apvrille AT enst.fr
+*
+* This software is a computer program whose purpose is to allow the
+* edition of TURTLE analysis, design and deployment diagrams, to
+* allow the generation of RT-LOTOS or Java code from this diagram,
+* and at last to allow the analysis of formal validation traces
+* obtained from external tools, e.g. RTL from LAAS-CNRS and CADP
+* from INRIA Rhone-Alpes.
+*
+* This software is governed by the CeCILL license under French law and
+* abiding by the rules of distribution of free software. You can use,
+* modify and/ or redistribute the software under the terms of the CeCILL
+* license as circulated by CEA, CNRS and INRIA at the following URL
+* "http://www.cecill.info".
+*
+* As a counterpart to the access to the source code and rights to copy,
+* modify and redistribute granted by the license, users are provided only
+* with a limited warranty and the software's author, the holder of the
+* economic rights, and the successive licensors have only limited
+* liability.
+*
+* In this respect, the user's attention is drawn to the risks associated
+* with loading, using, modifying and/or developing or reproducing the
+* software by the user in light of its specific status of free software,
+* that may mean that it is complicated to manipulate, and that also
+* therefore means that it is reserved for developers and experienced
+* professionals having in-depth computer knowledge. Users are therefore
+* encouraged to load and test the software's suitability as regards their
+* requirements in conditions enabling the security of their systems and/or
+* data to be ensured and, more generally, to use and operate it in the
+* same conditions as regards security.
+*
+* The fact that you are presently reading this means that you have had
+* knowledge of the CeCILL license and that you accept its terms.
+*
+* /**
+* Class JDialogAvatarSimulationGeneration
+* Dialog for managing the generation and compilation of AVATAR simulation code
+* Creation: 10/12/2010
+* @version 1.1 10/12/2010
+* @author Ludovic APVRILLE
+* @see
+*/
package ui.window;
@@ -59,6 +59,7 @@ import ui.*;
import avatartranslator.*;
import avatartranslator.tocppsim.*;
+import avatartranslator.directsimulation.*;
import launcher.*;
@@ -74,7 +75,7 @@ public class JDialogAvatarSimulationGeneration extends javax.swing.JDialog imple
private static String unitCycle = "1";
- private static String[] simus = {"AVATAR Simulator - c++ version"};
+ private static String[] simus = {"AVATAR Simulator - c++ version", "AVATAR Simulation - internal version"};
private static int selectedItem = 0;
protected static String pathCode;
@@ -402,127 +403,133 @@ public class JDialogAvatarSimulationGeneration extends javax.swing.JDialog imple
hasError = false;
try {
-
- // Code generation
- if (jp1.getSelectedIndex() == 0) {
- jta.append("Generating Simulation code (c++, LabSoC version)\n");
-
- if (removeCppFiles.isSelected()) {
- jta.append("Removing all .h files\n");
- list = FileUtils.deleteFiles(code1.getText(), ".h");
- if (list.length() == 0) {
- jta.append("No files were deleted\n");
- } else {
- jta.append("Files deleted:\n" + list + "\n");
- }
- jta.append("Removing all .cpp files\n");
- list = FileUtils.deleteFiles(code1.getText(), ".cpp");
- if (list.length() == 0) {
- jta.append("No files were deleted\n");
- } else {
- jta.append("Files deleted:\n" + list + "\n");
- }
- }
-
- if (removeXFiles.isSelected()) {
- jta.append("Removing all .x files\n");
- list = FileUtils.deleteFiles(code1.getText(), ".x");
- if (list.length() == 0) {
- jta.append("No files were deleted\n");
- } else {
- jta.append("Files deleted:\n" + list + "\n");
- }
- }
-
- testGo();
-
- selectedItem = versionSimulator.getSelectedIndex();
- //System.out.println("Selected item=" + selectedItem);
- if (selectedItem == 0) {
- AvatarSpecification avspec = mgui.gtm.getAvatarSpecification();
+ if (versionSimulator.getSelectedIndex() == 0) {
+ // Code generation
+ if (jp1.getSelectedIndex() == 0) {
+ jta.append("Generating Simulation code (c++, LabSoC version)\n");
+
+ if (removeCppFiles.isSelected()) {
+ jta.append("Removing all .h files\n");
+ list = FileUtils.deleteFiles(code1.getText(), ".h");
+ if (list.length() == 0) {
+ jta.append("No files were deleted\n");
+ } else {
+ jta.append("Files deleted:\n" + list + "\n");
+ }
+ jta.append("Removing all .cpp files\n");
+ list = FileUtils.deleteFiles(code1.getText(), ".cpp");
+ if (list.length() == 0) {
+ jta.append("No files were deleted\n");
+ } else {
+ jta.append("Files deleted:\n" + list + "\n");
+ }
+ }
+
+ if (removeXFiles.isSelected()) {
+ jta.append("Removing all .x files\n");
+ list = FileUtils.deleteFiles(code1.getText(), ".x");
+ if (list.length() == 0) {
+ jta.append("No files were deleted\n");
+ } else {
+ jta.append("Files deleted:\n" + list + "\n");
+ }
+ }
+
+ testGo();
- // Generating code
- if (avspec == null) {
- jta.append("Error: No AVATAR specification\n");
- } else {
- AVATAR2CPPSIM avatartocppsim = new AVATAR2CPPSIM(avspec);
- avatartocppsim.generateCPPSIM(debugmode.isSelected(), optimizemode.isSelected());
- //tml2systc.generateSystemC(debugmode.isSelected(), optimizemode.isSelected());
- testGo();
- jta.append("Generation of Simulation code in c++: done\n");
- //t2j.printJavaClasses();
- try {
- jta.append("Saving code in files\n");
- pathCode = code1.getText();
- avatartocppsim.saveFile(pathCode, "");
- //tml2systc.saveFile(pathCode, "appmodel");
- jta.append("Code saved\n");
- } catch (Exception e) {
- jta.append("Could not generate files\n");
+ selectedItem = versionSimulator.getSelectedIndex();
+ //System.out.println("Selected item=" + selectedItem);
+ if (selectedItem == 0) {
+ AvatarSpecification avspec = mgui.gtm.getAvatarSpecification();
+
+ // Generating code
+ if (avspec == null) {
+ jta.append("Error: No AVATAR specification\n");
+ } else {
+ AVATAR2CPPSIM avatartocppsim = new AVATAR2CPPSIM(avspec);
+ avatartocppsim.generateCPPSIM(debugmode.isSelected(), optimizemode.isSelected());
+ //tml2systc.generateSystemC(debugmode.isSelected(), optimizemode.isSelected());
+ testGo();
+ jta.append("Generation of Simulation code in c++: done\n");
+ //t2j.printJavaClasses();
+ try {
+ jta.append("Saving code in files\n");
+ pathCode = code1.getText();
+ avatartocppsim.saveFile(pathCode, "");
+ //tml2systc.saveFile(pathCode, "appmodel");
+ jta.append("Code saved\n");
+ } catch (Exception e) {
+ jta.append("Could not generate files\n");
+ }
}
}
+
+
}
-
-
- }
-
- testGo();
-
-
- // Compilation
- if (jp1.getSelectedIndex() == 1) {
-
- cmd = compiler1.getText();
-
- jta.append("Compiling simulation code with command: \n" + cmd + "\n");
-
- rshc = new RshClient(hostSimu);
- // Assuma data are on the remote host
- // Command
- try {
- data = processCmd(cmd);
- jta.append(data);
- jta.append("Compilation done\n");
- } catch (LauncherException le) {
- jta.append("Error: " + le.getMessage() + "\n");
- mode = STOPPED;
- setButtons();
- return;
- } catch (Exception e) {
- mode = STOPPED;
- setButtons();
- return;
- }
- }
-
- if (jp1.getSelectedIndex() == 2) {
- try {
- cmd = exe2.getText();
-
- jta.append("Executing simulation with command: \n" + cmd + "\n");
-
- rshc = new RshClient(hostSimu);
- // Assuma data are on the remote host
- // Command
-
- data = processCmd(cmd);
- jta.append(data);
- jta.append("Execution done\n");
- } catch (LauncherException le) {
- jta.append("Error: " + le.getMessage() + "\n");
- mode = STOPPED;
- setButtons();
- return;
- } catch (Exception e) {
- mode = STOPPED;
- setButtons();
- return;
- }
- }
-
- if ((hasError == false) && (jp1.getSelectedIndex() < 2)) {
- jp1.setSelectedIndex(jp1.getSelectedIndex() + 1);
- }
+
+ testGo();
+
+
+ // Compilation
+ if (jp1.getSelectedIndex() == 1) {
+
+ cmd = compiler1.getText();
+
+ jta.append("Compiling simulation code with command: \n" + cmd + "\n");
+
+ rshc = new RshClient(hostSimu);
+ // Assuma data are on the remote host
+ // Command
+ try {
+ data = processCmd(cmd);
+ jta.append(data);
+ jta.append("Compilation done\n");
+ } catch (LauncherException le) {
+ jta.append("Error: " + le.getMessage() + "\n");
+ mode = STOPPED;
+ setButtons();
+ return;
+ } catch (Exception e) {
+ mode = STOPPED;
+ setButtons();
+ return;
+ }
+ }
+
+ if (jp1.getSelectedIndex() == 2) {
+ try {
+ cmd = exe2.getText();
+
+ jta.append("Executing simulation with command: \n" + cmd + "\n");
+
+ rshc = new RshClient(hostSimu);
+ // Assuma data are on the remote host
+ // Command
+
+ data = processCmd(cmd);
+ jta.append(data);
+ jta.append("Execution done\n");
+ } catch (LauncherException le) {
+ jta.append("Error: " + le.getMessage() + "\n");
+ mode = STOPPED;
+ setButtons();
+ return;
+ } catch (Exception e) {
+ mode = STOPPED;
+ setButtons();
+ return;
+ }
+ }
+
+ if ((hasError == false) && (jp1.getSelectedIndex() < 2)) {
+ jp1.setSelectedIndex(jp1.getSelectedIndex() + 1);
+ }
+ } else {
+ AvatarSpecification avspec = mgui.gtm.getAvatarSpecification();
+ AvatarSpecificationSimulation ass = new AvatarSpecificationSimulation(avspec);
+ ass.initialize();
+ ass.runSimulation();
+ }
} catch (InterruptedException ie) {
jta.append("Interrupted\n");
@@ -550,27 +557,27 @@ public class JDialogAvatarSimulationGeneration extends javax.swing.JDialog imple
protected void setButtons() {
switch(mode) {
- case NOT_STARTED:
- start.setEnabled(true);
- stop.setEnabled(false);
- close.setEnabled(true);
- //setCursor(Cursor.getPredefinedCursor(Cursor.DEFAULT_CURSOR));
- getGlassPane().setVisible(false);
- break;
- case STARTED:
- start.setEnabled(false);
- stop.setEnabled(true);
- close.setEnabled(false);
- getGlassPane().setVisible(true);
- //setCursor(Cursor.getPredefinedCursor(Cursor.WAIT_CURSOR));
- break;
- case STOPPED:
- default:
- start.setEnabled(false);
- stop.setEnabled(false);
- close.setEnabled(true);
- getGlassPane().setVisible(false);
- break;
+ case NOT_STARTED:
+ start.setEnabled(true);
+ stop.setEnabled(false);
+ close.setEnabled(true);
+ //setCursor(Cursor.getPredefinedCursor(Cursor.DEFAULT_CURSOR));
+ getGlassPane().setVisible(false);
+ break;
+ case STARTED:
+ start.setEnabled(false);
+ stop.setEnabled(true);
+ close.setEnabled(false);
+ getGlassPane().setVisible(true);
+ //setCursor(Cursor.getPredefinedCursor(Cursor.WAIT_CURSOR));
+ break;
+ case STOPPED:
+ default:
+ start.setEnabled(false);
+ stop.setEnabled(false);
+ close.setEnabled(true);
+ getGlassPane().setVisible(false);
+ break;
}
}
@@ -594,5 +601,5 @@ public class JDialogAvatarSimulationGeneration extends javax.swing.JDialog imple
return pathInteractiveExecute;
}
-
+
}
diff --git a/src/ui/window/JDialogProVerifGeneration.java b/src/ui/window/JDialogProVerifGeneration.java
index 6686380e96..5aa3079805 100644
--- a/src/ui/window/JDialogProVerifGeneration.java
+++ b/src/ui/window/JDialogProVerifGeneration.java
@@ -373,16 +373,26 @@ public class JDialogProVerifGeneration extends javax.swing.JDialog implements Ac
jta.append(re+"\n");
}
- jta.append("\nConfidential data:\n----------------\n");
+ jta.append("\nConfidential Data:\n----------------\n");
for(String re: pvoa.getSecretTerms()) {
jta.append(re+"\n");
}
- jta.append("\nNon confidential data:\n----------------\n");
+ jta.append("\nNon Confidential Data:\n----------------\n");
for(String re: pvoa.getNonSecretTerms()) {
jta.append(re+"\n");
}
+ jta.append("\nSatisfied Authenticity:\n----------------\n");
+ for(String re: pvoa.getSatisfiedAuthenticity()) {
+ jta.append(re+"\n");
+ }
+
+ jta.append("\nNon Satisfied Authenticity:\n----------------\n");
+ for(String re: pvoa.getNonSatisfiedAuthenticity()) {
+ jta.append(re+"\n");
+ }
+
jta.append("\nNon proved queries:\n----------------\n");
for(String re: pvoa.getNotProved()) {
jta.append(re+"\n");
--
GitLab