From 45a221786be859d583e616c47d0e26556df865b0 Mon Sep 17 00:00:00 2001 From: danielratiu Date: Fri, 17 Nov 2023 15:04:55 +0100 Subject: [PATCH] safety.stpa: initial language for deriving monitors --- .../com.mbeddr.formal.safety/.mps/modules.xml | 1 + .../com.mbeddr.formal.safety.stamp.ops.mpl | 125 ++++ ...tamp.ops.generator.templates@generator.mps | 24 + ...beddr.formal.safety.stamp.ops.behavior.mps | 12 + ...dr.formal.safety.stamp.ops.constraints.mps | 19 + ....mbeddr.formal.safety.stamp.ops.editor.mps | 162 +++++ ...eddr.formal.safety.stamp.ops.structure.mps | 116 ++++ ...ddr.formal.safety.stamp.ops.typesystem.mps | 11 + .../com.mbeddr.formal.safety.stamp.mpl | 2 + .../com.mbeddr.formal.safety.stamp.editor.mps | 13 + ...m.mbeddr.formal.safety.stamp.structure.mps | 14 + ...com.mbeddr.formal.safety.stamp.sandbox.msd | 9 + .../models/_020_stamp_ext_sandbox.mps | 554 +++++++++++++++--- 13 files changed, 986 insertions(+), 76 deletions(-) create mode 100644 code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.stamp.ops/com.mbeddr.formal.safety.stamp.ops.mpl create mode 100644 code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.stamp.ops/generator/templates/com.mbeddr.formal.safety.stamp.ops.generator.templates@generator.mps create mode 100644 code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.stamp.ops/models/com.mbeddr.formal.safety.stamp.ops.behavior.mps create mode 100644 code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.stamp.ops/models/com.mbeddr.formal.safety.stamp.ops.constraints.mps create mode 100644 code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.stamp.ops/models/com.mbeddr.formal.safety.stamp.ops.editor.mps create mode 100644 code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.stamp.ops/models/com.mbeddr.formal.safety.stamp.ops.structure.mps create mode 100644 code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.stamp.ops/models/com.mbeddr.formal.safety.stamp.ops.typesystem.mps diff --git a/code/languages/com.mbeddr.formal.safety/.mps/modules.xml b/code/languages/com.mbeddr.formal.safety/.mps/modules.xml index 733b4b3ed..5ca8cef1a 100644 --- a/code/languages/com.mbeddr.formal.safety/.mps/modules.xml +++ b/code/languages/com.mbeddr.formal.safety/.mps/modules.xml @@ -48,6 +48,7 @@ + diff --git a/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.stamp.ops/com.mbeddr.formal.safety.stamp.ops.mpl b/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.stamp.ops/com.mbeddr.formal.safety.stamp.ops.mpl new file mode 100644 index 000000000..742b78e9f --- /dev/null +++ b/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.stamp.ops/com.mbeddr.formal.safety.stamp.ops.mpl @@ -0,0 +1,125 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + b0b65429-cd22-4e2a-83e7-cd58bc6dd72f(com.mbeddr.formal.base.expressions) + 83ed2dfe-f724-46cc-852a-dce086daee3f(com.mbeddr.formal.base) + 7e777b53-0a6b-4719-b36d-10475788d49f(com.mbeddr.formal.safety.stamp) + d3a0fd26-445a-466c-900e-10444ddfed52(com.mbeddr.mpsutil.filepicker) + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + b0b65429-cd22-4e2a-83e7-cd58bc6dd72f(com.mbeddr.formal.base.expressions) + + + diff --git a/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.stamp.ops/generator/templates/com.mbeddr.formal.safety.stamp.ops.generator.templates@generator.mps b/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.stamp.ops/generator/templates/com.mbeddr.formal.safety.stamp.ops.generator.templates@generator.mps new file mode 100644 index 000000000..d98d5e771 --- /dev/null +++ b/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.stamp.ops/generator/templates/com.mbeddr.formal.safety.stamp.ops.generator.templates@generator.mps @@ -0,0 +1,24 @@ + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.stamp.ops/models/com.mbeddr.formal.safety.stamp.ops.behavior.mps b/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.stamp.ops/models/com.mbeddr.formal.safety.stamp.ops.behavior.mps new file mode 100644 index 000000000..56c23c972 --- /dev/null +++ b/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.stamp.ops/models/com.mbeddr.formal.safety.stamp.ops.behavior.mps @@ -0,0 +1,12 @@ + + + + + + + + + + + + diff --git a/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.stamp.ops/models/com.mbeddr.formal.safety.stamp.ops.constraints.mps b/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.stamp.ops/models/com.mbeddr.formal.safety.stamp.ops.constraints.mps new file mode 100644 index 000000000..c97380774 --- /dev/null +++ b/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.stamp.ops/models/com.mbeddr.formal.safety.stamp.ops.constraints.mps @@ -0,0 +1,19 @@ + + + + + + + + + + + + + + + + + + + diff --git a/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.stamp.ops/models/com.mbeddr.formal.safety.stamp.ops.editor.mps b/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.stamp.ops/models/com.mbeddr.formal.safety.stamp.ops.editor.mps new file mode 100644 index 000000000..d5c21e168 --- /dev/null +++ b/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.stamp.ops/models/com.mbeddr.formal.safety.stamp.ops.editor.mps @@ -0,0 +1,162 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.stamp.ops/models/com.mbeddr.formal.safety.stamp.ops.structure.mps b/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.stamp.ops/models/com.mbeddr.formal.safety.stamp.ops.structure.mps new file mode 100644 index 000000000..ec81f4be3 --- /dev/null +++ b/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.stamp.ops/models/com.mbeddr.formal.safety.stamp.ops.structure.mps @@ -0,0 +1,116 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.stamp.ops/models/com.mbeddr.formal.safety.stamp.ops.typesystem.mps b/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.stamp.ops/models/com.mbeddr.formal.safety.stamp.ops.typesystem.mps new file mode 100644 index 000000000..0895a05a2 --- /dev/null +++ b/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.stamp.ops/models/com.mbeddr.formal.safety.stamp.ops.typesystem.mps @@ -0,0 +1,11 @@ + + + + + + + + + + + diff --git a/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.stamp/com.mbeddr.formal.safety.stamp.mpl b/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.stamp/com.mbeddr.formal.safety.stamp.mpl index eca1b707a..88373f9df 100644 --- a/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.stamp/com.mbeddr.formal.safety.stamp.mpl +++ b/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.stamp/com.mbeddr.formal.safety.stamp.mpl @@ -23,6 +23,7 @@ e9ce245b-3106-45ed-8e5b-aff820d09b85(com.mbeddr.formal.base.tooling) 1ed103c3-3aa6-49b7-9c21-6765ee11f224(MPS.Editor) 8865b7a8-5271-43d3-884c-6fd1d9cfdd34(MPS.OpenAPI) + b0b65429-cd22-4e2a-83e7-cd58bc6dd72f(com.mbeddr.formal.base.expressions) @@ -81,6 +82,7 @@ + diff --git a/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.stamp/models/com.mbeddr.formal.safety.stamp.editor.mps b/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.stamp/models/com.mbeddr.formal.safety.stamp.editor.mps index 6ed187953..dbae573d6 100644 --- a/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.stamp/models/com.mbeddr.formal.safety.stamp.editor.mps +++ b/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.stamp/models/com.mbeddr.formal.safety.stamp.editor.mps @@ -2945,5 +2945,18 @@ + + + + + + + + + + + + + diff --git a/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.stamp/models/com.mbeddr.formal.safety.stamp.structure.mps b/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.stamp/models/com.mbeddr.formal.safety.stamp.structure.mps index f8a85e9b5..49cbfa274 100644 --- a/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.stamp/models/com.mbeddr.formal.safety.stamp.structure.mps +++ b/code/languages/com.mbeddr.formal.safety/languages/com.mbeddr.formal.safety.stamp/models/com.mbeddr.formal.safety.stamp.structure.mps @@ -9,6 +9,7 @@ + @@ -630,5 +631,18 @@ + + + + + + + + + + + + + diff --git a/code/languages/com.mbeddr.formal.safety/solutions/com.mbeddr.formal.safety.stamp.sandbox/com.mbeddr.formal.safety.stamp.sandbox.msd b/code/languages/com.mbeddr.formal.safety/solutions/com.mbeddr.formal.safety.stamp.sandbox/com.mbeddr.formal.safety.stamp.sandbox.msd index 9ca30818c..dd2e9cf06 100644 --- a/code/languages/com.mbeddr.formal.safety/solutions/com.mbeddr.formal.safety.stamp.sandbox/com.mbeddr.formal.safety.stamp.sandbox.msd +++ b/code/languages/com.mbeddr.formal.safety/solutions/com.mbeddr.formal.safety.stamp.sandbox/com.mbeddr.formal.safety.stamp.sandbox.msd @@ -12,14 +12,23 @@ + + + + + + + + + diff --git a/code/languages/com.mbeddr.formal.safety/solutions/com.mbeddr.formal.safety.stamp.sandbox/models/_020_stamp_ext_sandbox.mps b/code/languages/com.mbeddr.formal.safety/solutions/com.mbeddr.formal.safety.stamp.sandbox/models/_020_stamp_ext_sandbox.mps index cc3e60df5..b79d7af2f 100644 --- a/code/languages/com.mbeddr.formal.safety/solutions/com.mbeddr.formal.safety.stamp.sandbox/models/_020_stamp_ext_sandbox.mps +++ b/code/languages/com.mbeddr.formal.safety/solutions/com.mbeddr.formal.safety.stamp.sandbox/models/_020_stamp_ext_sandbox.mps @@ -4,16 +4,69 @@ + + + + + + + + + + - - - + - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + @@ -23,28 +76,74 @@ - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - + + - - + + + + - - - - - - + + - - - + + + + + + + + @@ -61,6 +160,14 @@ + + + + + + + + @@ -68,72 +175,367 @@ - - - - - + + + - - + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +