FASR: Formalizing and Automating STPA with Robustness

This repository holds code to support the partial automation of the System Theoretic Process Analysis.

Building

The STPA Guideword Classifier

This compares two traces through a system -- one safe and one unsafe -- and creates an unsafe control action for the unsafe trace. Fortis can be used to generate the traces from a TLA+ or FSP model of a system and its environment.

The classifier code

After cloning the repository, use maven to build the project:

% pwd
/Users/sprocter/git/fasr/UCAClassification_EditDistance
% mvn clean verify
[INFO] Scanning for projects...
[INFO]
[INFO] -----------------------------< FASR:FASR >------------------------------
[INFO] Building Formalization and Automation of STPA using Robustness 0.0.1-SNAPSHOT
[INFO]   from pom.xml
[INFO] --------------------------------[ jar ]---------------------------------
[INFO]
[INFO] --- clean:3.2.0:clean (default-clean) @ FASR ---
[...]

Fortis

You will also need the FASR branch of Fortis. After cloning and switching to the FASR branch, make sure you can run the "Water Tank" example using the --stpa flag:

% pwd
/Users/sprocter/git/fortis-core/examples/water_tank
% java -jar ../../out/artifacts/fortis_core_jar/fortis-core.jar robustness --stpa --tla-sys WaterTank.tla --cfg-sys WaterTank.cfg --tla-env WaterTankEnv.tla --cfg-env WaterTankEnv.cfg | tail -2 | head -1 | jq

[
  {
    "goodTrace": [
      "TurnPumpOn",
      "Wait",
      "Wait",
      "TurnPumpOff"
    ],
    "badTrace": [
      "TurnPumpOn",
      "Wait",
      "Wait",
      "Wait"
    ]
  },
  [...]
]

Classifying Fortis Output

You can now pipe the output from Fortis to the UCA Classifier:

% pwd
% java -jar ../../out/artifacts/fortis_core_jar/fortis-core.jar robustness --stpa --tla-sys WaterTank.tla --cfg-sys WaterTank.cfg --tla-env WaterTankEnv.tla --cfg-env WaterTankEnv.cfg | java -jar ~/git/fasr/UCAClassification_EditDistance/target/FASR-0.0.1-SNAPSHOT-jar-with-dependencies.jar | jq

[
  {
    "source": "##PLACEHOLDER##",
    "guideword": "NotProviding",
    "controlAction": "TurnPumpOff",
    "context": [
      "TurnPumpOn",
      "Wait",
      "Wait"
    ],
    [...]
]