search

loonwerks / AGREE

Assume-Guarantee REasoning Environment
BSD 3-Clause "New" or "Revised" License
13 stars 5 forks source link

AGREE support for Safety Annex #13

Closed kfhoech closed 4 years ago

kfhoech commented 4 years ago

Issue by daniellestewart Wednesday Jun 13, 2018 at 14:09 GMT Originally opened as https://github.com/smaccm/smaccm/issues/142

This enhancement is specifically for the Safety Annex and incorporating new fault tree generation into the annex using AGREE and JKind.

kfhoech commented 4 years ago

Comment by dkstewart Wednesday Jun 13, 2018 at 15:06 GMT

We are utilizing the IVC generation abilities of JKind and the all-IVC algorithm in order to generate fault trees through the Safety Annex and Agree.

Currently, Agree inserts IVCs into the lustre code through assumptions and guarantees (inputs and outputs of components). With this new method, we wish to add the IVC elements as faults and supporting guarantees. In order to accomplish this task, we must change how the set of support is constructed in Agree nodes.

An important item to note about the AST node classes is that they are immutable. That is, the value of any given instance is not allowed to change. Other elements of the design depend on this immutability property.

In Java, the pattern applied to implement immutable classes is to make all fields public (so they can be directly accessed) and final (so their value cannot be changed). Aggregates should likewise be immutable, using jkind.util.Util.safeList or java.util.Collections.UnmodifiableList (or similar unmodifiable Set, Map, SortedSet, etc. aggregates).

Instead, of added private fields and getter/setter methods, we will make the new fields public, final (and unmodifiable) and then add them to the constructor and to the AgreeNodeBuilder. Only, the AgreeNodeBuilder should be calling the AgreeNode constructor. If any other classes call it directly, they should be refactored to instead use the AgreeNodeBuilder to construct the instance of AgreeNode.

These new fields will be "separate" from the "normal" IVCs by naming convention. These fields will specifically refer to the fault analysis, even though in the end we are calling on the all-IVC algorithm. This will make it more clear what these new fault IVCs are doing.

A new menu will be added for the user to select this form of safety analysis. Currently the Safety Annex supports max number of fault analysis and probabilistic monolithic analysis. Through this approach we are adding the capability of compositional fault tree analysis which is a separate analysis from the other options listed above.

kfhoech commented 4 years ago

Comment by dkstewart Monday Jun 18, 2018 at 17:44 GMT

After discussion with the AMASE team, we have decided the best way of implementing this is to keep the safety analysis and AGREE analysis as separate as possible. We have created a new menu in OSATE specifically for the safety analysis options.

As far as the AgreeNode is concerned, we will be adding a new list to the constructor and calling it ivcElements. This will be a public final field with getters and setters.

In LustreASTBuilder, it will check this list. If nonempty, it adds these elements to the Lustre program. Else, it gathers the ivc elements as done previously (assumptions and guarantees).

This makes it possible for other applications to possibly use this list to add ivc elements to a program without it being specifically for safety analysis.

kfhoech commented 4 years ago

Comment by dkstewart Friday Jul 06, 2018 at 17:14 GMT

We are adding a field to the AgreeNode that checks to see if fault analysis is being run. In this way it can refer to that flag when adding guarantees into the lustre code. In the future we will look into extending the LustreASTBuilder class and if this is implemented, we can avoid having to turn to Agree in order to make these adjustments.

kfhoech commented 4 years ago

Completed by pull request #27.