Skip to content

Commit

Permalink
Merge pull request #45 from kieler/jep/utility
Browse files Browse the repository at this point in the history 
Jep/utility
  • Loading branch information
@Drakae
Drakae authored Oct 11, 2024
2 parents a21f20e + 4df67bc commit c218c3c
Show file tree
Hide file tree
Showing 16 changed files with 434 additions and 235 deletions.
28 changes: 23 additions & 5 deletions extension/README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -28,10 +28,11 @@ Alternatively the textual representation can be entered in the diagram snippets

Instead of informal UCA definitions a context table may be used. This is done by using the section `Context-Table` instead of `UCAs`. A context table can then be generated automatically and shown alongside the diagram by selecting `Show Context Tables` in the editor context menu or the corresponding icon right above the editor. Clicking on a UCA in the context table highlights the corresponding node in the diagram and its definition in the editor. In the context table view a control action can be selected in order to inspect it.

### Completion Item
### Automation through Completion Item

Partly information is repeated in STPA e.g. when defining a scenario for a UCA, the UCA itself is written down again.
To reduce the time effort, PASTA offers completion items, which generate text automatically based on the informations already stated in other components.
To reduce the time effort, PASTA offers completion items, which generate text automatically based on the informations already stated in other components.
To access completion items, press `ctrl` + `space`.
The following completion items are provided:
* create system component
* create starting text for a plain text UCA
Expand All @@ -51,7 +52,19 @@ The markdown file can easily be exported to a PDF file.

### Safe Behavioral Model Generation

In the context menu an option to automatically generate a safe behavioral model as an SCChart is provided. For that the defined UCAs are translated to LTL formulas, which are further used to create the SCChart. This guarantees that the identified UCAs cannot occur since the LTL formulas are respected except the ones for the UCA type too early.
In the context menu an option to automatically generate a safe behavioral model as an SCChart is provided.
For that the defined UCAs are translated to LTL formulas, which are further used to create the SCChart.
This guarantees that the identified UCAs cannot occur since the LTL formulas are respected except the ones for the UCA type **too early**.
For the generation you can define ranges for the process model variable values with standard range notation and the keywords `MIN` and `MAX`.
Example process model:
```
processModel {
currentSpeed: [desiredSpeed=[desiredSpeed], lessDesiredSpeed = [MIN, desiredSpeed), greaterDesiredSpeed=(desiredSpeed, MAX]]
}
```
In this case the controller has the process model variable `currentSpeed` which can take the values `desiredSpeed`, `lessDesiredSpeed`, and `greaterDesiredSpeed`.
For each of these values, the range it covers is defined.
`lessDesiredSpeed` covers every speed under the desired one, `greaterDesiredSpeed` every speed above the desired speed, and `desiredSpeed` only the desired speed.

The SCChart language and an automatic visualization is provided by the two KIELER extensions [KLighD Diagrams](https://marketplace.visualstudio.com/items?itemName=kieler.klighd-vscode) and [KIELER VS Code](https://marketplace.visualstudio.com/items?itemName=kieler.keith-vscode).

Expand All @@ -65,7 +78,12 @@ Furthermore, after an STPA is done, a corresponding Fault Tree can be generated

### STPA

To use the extension for an analysis, the file in which the analysis is done must have `.stpa` as its file ending. Each STPA aspect has its own section in the DSL. Components for each aspect are defined with an ID, a description, and a reference list. In order to define a new component, the prefix of the corresponding aspect must be stated, for example "L", and afterwards a string with the description. The numbering of the IDs is adjusted automatically. For Hazards and system-level constraints subcomponents can be defined.
To use the extension for an analysis, the file in which the analysis is done must have `.stpa` as its file ending.
Each STPA aspect has its own section in the DSL. Components for each aspect are defined with an ID, a description, and a reference list.
In order to define a new component, the prefix of the corresponding aspect must be stated, for example "L", and afterwards a string with the description.
The numbering of the IDs is adjusted automatically.
For Hazards and system-level constraints subcomponents can be defined.
For scenarios the causal factor can stated.

In the control structure, system components can be stated, which can contain a process model, input, output, control actions, feedback, and further system components. The visualization of input and output edges is in an experimental state at the moment and will be improved in the future.

Expand Down Expand Up @@ -137,7 +155,7 @@ ControllerConstraints
C1 "ControlCentre must provide the Manual setting control action during VC malfunctioning and vessel too close to No Go Area" [UCA1]
LossScenarios
Scenario1 for UCA1 "Abnormal vessel behavior occurs. Vessel comes too close to a No Go Area and ControlCentre does not manual set the parameters of the engine, causing the entering of a No Go Area." [H1]
Scenario1 <componentFailure> for UCA1 "Abnormal vessel behavior occurs. Vessel comes too close to a No Go Area and ControlCentre does not manual set the parameters of the engine, causing the entering of a No Go Area." [H1]
Scenario2 "Virtual Captain sends the Set parameters command upon coming too close to a No Go Area, but decceleration is not applied due to actuator failure." [H1]
SafetyRequirements
Expand Down
50 changes: 40 additions & 10 deletions extension/package.json
View file
Original file line number Diff line number Diff line change
Expand Up @@ -142,6 +142,16 @@
"title": "✓ Set the safety requirements for UCA check",
"category": "STPA Checks"
},
{
"command": "pasta.stpa.checks.setCheckMissingFeedback",
"title": "Set the missing feedback for system components check",
"category": "STPA Checks"
},
{
"command": "pasta.stpa.checks.unsetCheckMissingFeedback",
"title": "✓ Set the missing feedback for system components check",
"category": "STPA Checks"
},
{
"command": "pasta.IDs.undo",
"title": "Executes the undo action",
Expand Down Expand Up @@ -183,12 +193,12 @@
"category": "STPA Snippets"
},
{
"command": "pasta.stpa.setIDGeneration",
"command": "pasta.stpa.setGenerateIDs",
"title": "Automatic ID Generation",
"category": "STPA ID Enforcement"
},
{
"command": "pasta.stpa.unsetIDGeneration",
"command": "pasta.stpa.unsetGenerateIDs",
"title": "✓ Automatic ID Generation",
"category": "STPA ID Enforcement"
}
Expand Down Expand Up @@ -258,6 +268,14 @@
"command": "pasta.stpa.checks.unsetCheckSafetyRequirementsForUCAs",
"when": "editorLangId == 'stpa' && checkSafetyRequirementsForUCAs == true"
},
{
"command": "pasta.stpa.checks.setCheckMissingFeedback",
"when": "editorLangId == 'stpa' && checkMissingFeedback == false"
},
{
"command": "pasta.stpa.checks.unsetCheckMissingFeedback",
"when": "editorLangId == 'stpa' && checkMissingFeedback == true"
},
{
"command": "pasta.stpa.SBM.generation",
"when": "editorLangId == 'stpa'"
Expand All @@ -275,12 +293,12 @@
"when": "editorLangId == 'stpa'"
},
{
"command": "pasta.stpa.setIDGeneration",
"when": "editorLangId == 'stpa' && pasta.idGeneration == false"
"command": "pasta.stpa.setGenerateIDs",
"when": "editorLangId == 'stpa' && pasta.generateIDs == false"
},
{
"command": "pasta.stpa.unsetIDGeneration",
"when": "editorLangId == 'stpa' && pasta.idGeneration == true"
"command": "pasta.stpa.unsetGenerateIDs",
"when": "editorLangId == 'stpa' && pasta.generateIDs == true"
},
{
"command": "pasta.fta.cutSets",
Expand Down Expand Up @@ -333,13 +351,13 @@
"group": "stpa@4"
},
{
"command": "pasta.stpa.setIDGeneration",
"when": "editorLangId == 'stpa' && pasta.idGeneration == false",
"command": "pasta.stpa.setGenerateIDs",
"when": "editorLangId == 'stpa' && pasta.generateIDs == false",
"group": "stpa@1"
},
{
"command": "pasta.stpa.unsetIDGeneration",
"when": "editorLangId == 'stpa' && pasta.idGeneration == true",
"command": "pasta.stpa.unsetGenerateIDs",
"when": "editorLangId == 'stpa' && pasta.generateIDs == true",
"group": "stpa@1"
},
{
Expand Down Expand Up @@ -401,6 +419,18 @@
"title": "editorLangId == 'stpa'",
"when": "editorLangId == 'stpa' && pasta.checkSafetyRequirementsForUCAs == true",
"group": "checks@4"
},
{
"command": "pasta.stpa.checks.setCheckMissingFeedback",
"title": "editorLangId == 'stpa'",
"when": "editorLangId == 'stpa' && pasta.checkMissingFeedback == false",
"group": "checks@5"
},
{
"command": "pasta.stpa.checks.unsetCheckMissingFeedback",
"title": "editorLangId == 'stpa'",
"when": "editorLangId == 'stpa' && pasta.checkMissingFeedback == true",
"group": "checks@5"
}
],
"editor/title": [
Expand Down
147 changes: 107 additions & 40 deletions extension/src-language-server/stpa/diagram/diagram-controlStructure.ts
View file
Original file line number Diff line number Diff line change
Expand Up @@ -41,13 +41,17 @@ import { getCommonAncestor, setLevelOfCSNodes, sortPorts } from "./utils";
* @param idToSNode The map of IDs to SNodes.
* @param options The synthesis options of the STPA model.
* @param idCache The ID cache of the STPA model.
* @param addMissing Whether missing feedback should be added to the control structure.
* @param missingFeedback The missing feedbacks of the control structure.
* @returns the generated control structure diagram.
*/
export function createControlStructure(
controlStructure: Graph,
idToSNode: Map<string, SNode>,
options: StpaSynthesisOptions,
idCache: IdCache<AstNode>
idCache: IdCache<AstNode>,
addMissing: boolean,
missingFeedback?: Map<string, Node[]>
): ParentNode {
// set the level of the nodes in the control structure automatically
setLevelOfCSNodes(controlStructure.nodes);
Expand All @@ -56,7 +60,7 @@ export function createControlStructure(
// children (nodes and edges) of the control structure
const CSChildren = [
...csNodes,
...generateVerticalCSEdges(controlStructure.nodes, idToSNode, idCache),
...generateVerticalCSEdges(controlStructure.nodes, idToSNode, idCache, addMissing, missingFeedback),
//...this.generateHorizontalCSEdges(filteredModel.controlStructure.edges, idCache)
];
// sort the ports in order to group edges based on the nodes they are connected to
Expand Down Expand Up @@ -179,47 +183,67 @@ export function createProcessModelNodes(variables: Variable[], idCache: IdCache<
* Creates the edges for the control structure.
* @param nodes The nodes of the control structure.
* @param idCache The ID cache of the STPA model.
* @param addMissing Whether missing feedback should be added to the control structure.
* @param missingFeedback The missing feedbacks of the control structure.
* @returns A list of edges for the control structure.
*/
export function generateVerticalCSEdges(
nodes: Node[],
idToSNode: Map<string, SNode>,
idCache: IdCache<AstNode>
idCache: IdCache<AstNode>,
addMissing: boolean,
missingFeedback?: Map<string, Node[]>
): (CSNode | CSEdge)[] {
const edges: (CSNode | CSEdge)[] = [];
// for every control action and feedback of every a node, a edge should be created
for (const node of nodes) {
// create edges representing the control actions
edges.push(...translateCommandsToEdges(node.actions, EdgeType.CONTROL_ACTION, idToSNode, idCache));
edges.push(
...translateCommandsToEdges(
node,
node.actions,
EdgeType.CONTROL_ACTION,
idToSNode,
idCache,
addMissing,
missingFeedback
)
);
// create edges representing feedback
edges.push(...translateCommandsToEdges(node.feedbacks, EdgeType.FEEDBACK, idToSNode, idCache));
edges.push(...translateCommandsToEdges(node, node.feedbacks, EdgeType.FEEDBACK, idToSNode, idCache, false));
// create edges representing the other inputs
edges.push(...translateIOToEdgeAndNode(node.inputs, node, EdgeType.INPUT, idToSNode, idCache));
// create edges representing the other outputs
edges.push(...translateIOToEdgeAndNode(node.outputs, node, EdgeType.OUTPUT, idToSNode, idCache));
// create edges for children and add the ones that must be added at the top level
edges.push(...generateVerticalCSEdges(node.children, idToSNode, idCache));
edges.push(...generateVerticalCSEdges(node.children, idToSNode, idCache, addMissing, missingFeedback));
}
return edges;
}

/**
* Translates the commands (control action or feedback) of a node to (intermediate) edges and adds them to the correct nodes.
* @param node The node of the commands.
* @param commands The control actions or feedback of a node.
* @param edgeType The type of the edge (control action or feedback).
* @param idToSNode The map of IDs to SNodes.
* @param idCache The ID cache of the STPA model.
* @param addMissing Whether missing feedback should be added to the control structure.
* @param missingFeedback The missing feedbacks of the control structure.
* @returns A list of edges representing the commands that should be added at the top level.
*/
export function translateCommandsToEdges(
source: Node,
commands: VerticalEdge[],
edgeType: EdgeType,
idToSNode: Map<string, SNode>,
idCache: IdCache<AstNode>
idCache: IdCache<AstNode>,
addMissing: boolean,
missingFeedback?: Map<string, Node[]>
): CSEdge[] {
const edges: CSEdge[] = [];
for (const edge of commands) {
// create edge id
const source = edge.$container;
const target = edge.target.ref;
const edgeId = idCache.uniqueId(
`${idCache.getId(source)}_${edge.comms[0].name}_${idCache.getId(target)}`,
Expand All @@ -233,44 +257,87 @@ export function translateCommandsToEdges(
const com = edge.comms[i];
label.push(com.label);
}
// edges can be hierachy crossing so we must determine the common ancestor of source and target
const commonAncestor = getCommonAncestor(source, target);
// create the intermediate ports and edges
const ports = generateIntermediateCSEdges(
source,
target,
edgeId,
edgeType,
idToSNode,
idCache,
commonAncestor
);
// add edge between the two ports in the common ancestor
const csEdge = createControlStructureEdge(
idCache.uniqueId(edgeId),
ports.sourcePort,
ports.targetPort,
label,
edgeType,
// if the common ancestor is the parent of the target we want an edge with an arrow otherwise an intermediate edge
target.$container === commonAncestor ? CS_EDGE_TYPE : CS_INTERMEDIATE_EDGE_TYPE,
idCache
);
if (commonAncestor?.$type === "Graph") {
// if the common ancestor is the graph, the edge must be added at the top level and hence have to be returned
edges.push(csEdge);
} else if (commonAncestor) {
// if the common ancestor is a node, the edge must be added to the children of the common ancestor
const snodeAncestor = idToSNode.get(idCache.getId(commonAncestor)!);
snodeAncestor?.children
?.find(node => node.type === CS_INVISIBLE_SUBCOMPONENT_TYPE)
?.children?.push(csEdge);
createEdgeForCommand(source, target, edgeId, edgeType, label, idToSNode, idCache, edges);
}
}

// add missing feedback edges
if (addMissing && missingFeedback) {
// add feedback edge to each node to which a feedback is missing
let hasMissingFeedback = false;
for (const target of missingFeedback.get(source?.name ?? "") ?? []) {
if (source && target) {
hasMissingFeedback = true;
createEdgeForCommand(
source,
target,
idCache.uniqueId(`${source?.name}_missingFeedback_${target}`),
EdgeType.MISSING_FEEDBACK,
["MISSING"],
idToSNode,
idCache,
edges
);
}
}
// set flag for missing feedback to the source node
if (hasMissingFeedback) {
const sourceNode = idToSNode.get(idCache.getId(source) ?? "");
if (sourceNode && sourceNode.type === CS_NODE_TYPE) {
(sourceNode as CSNode).hasMissingFeedback = true;
}
}
}

return edges;
}

/**
* Creates (intermediate) edges for the given {@code source} and {@code target} and adds them to the correct node.
* @param source The source of the edge.
* @param target The target of the edge.
* @param edgeId The ID of the edge.
* @param edgeType The type of the edge.
* @param label The label of the edge.
* @param idToSNode The map of IDs to SNodes.
* @param idCache The ID cache of the STPA model.
* @param edges The list of edges to add the created edges to.
*/
export function createEdgeForCommand(
source: Node,
target: Node,
edgeId: string,
edgeType: EdgeType,
label: string[],
idToSNode: Map<string, SNode>,
idCache: IdCache<AstNode>,
edges: CSEdge[]
): void {
// edges can be hierachy crossing so we must determine the common ancestor of source and target
const commonAncestor = getCommonAncestor(source, target);
// create the intermediate ports and edges
const ports = generateIntermediateCSEdges(source, target, edgeId, edgeType, idToSNode, idCache, commonAncestor);
// add edge between the two ports in the common ancestor
const csEdge = createControlStructureEdge(
idCache.uniqueId(edgeId),
ports.sourcePort,
ports.targetPort,
label,
edgeType,
// if the common ancestor is the parent of the target we want an edge with an arrow otherwise an intermediate edge
target.$container === commonAncestor ? CS_EDGE_TYPE : CS_INTERMEDIATE_EDGE_TYPE,
idCache
);
if (commonAncestor?.$type === "Graph") {
// if the common ancestor is the graph, the edge must be added at the top level and hence have to be returned
edges.push(csEdge);
} else if (commonAncestor) {
// if the common ancestor is a node, the edge must be added to the children of the common ancestor
const snodeAncestor = idToSNode.get(idCache.getId(commonAncestor)!);
snodeAncestor?.children?.find(node => node.type === CS_INVISIBLE_SUBCOMPONENT_TYPE)?.children?.push(csEdge);
}
}

/**
* Translates the inputs or outputs of a node to edges.
* @param io The inputs or outputs of a node.
Expand Down
Loading

0 comments on commit c218c3c

Please sign in to comment.