search

loonwerks / AMASE

This is the repository for Architectural Modeling and Analysis for Safety Engineering (AMASE).
BSD 3-Clause "New" or "Revised" License
6 stars 4 forks source link

Permanent fault appears transient in multi-step counterexamples #1

Closed janetlj closed 6 years ago

janetlj commented 6 years ago

In multi-step counterexamples, permanent fault appears transient:

1) A fault can turn true for one step, and remains true the next step, but shows false in the counterexample panel. E.g., if having only the fault "AILL INVERT FAIL" (and commenting out the other faults) in https://github.com/loonwerks/AMASE/blob/develop/examples/QFCS_V3/packages/OSAS.aadl, verifying FCC shows that "once failed always failed" is false. In the counterexample the above fault turned true on step 4, and turned false on step 5, but the fault should still be true on step 5.

2) A fault can turn true for one step, and turns false the next step when another fault turns true on the same step. E.g., if having only faults "AILL PERSISTENT FAIL" and "AILL INVERT FAIL" (and commenting out the other faults) in https://github.com/loonwerks/AMASE/blob/develop/examples/QFCS_V3/packages/OSAS.aadl, verifying FCC shows that all guarantees hold. Counterexamples from verifying each of the above fault separately seem to indicate that OSAS-S-140 remains true with one of the faults because "AILL INVERT FAIL" fault turns true at step 4, and turns false at step 5, and "AILL PERSISTENT FAIL" turns true at step 5.

janetlj commented 6 years ago

This issue seems to have been fixed with the Master branch code committed Nov. 8th, 2017.

I tested the example from https://www-users.cs.umn.edu/svn_amase/examples/QFCS_V3 (SVN revision 65) with "AILL OUT STUCK TO VAL" fault uncommented in OSAS.aadl and other faults in the same file commented; ran verification on FCC.Impl of the same model, and on the counterexample for property OSAS-S-140; the 5-step counterexample showed that the above fault was false the first two steps and true the following three steps.

I tested another version of the example from https://github.com/loonwerks/AMASE/tree/master/examples/QFCS_V3 (committed Oct. 16, 2017), and uncommented "OSAS-S-140 fault" in OSAS.aadl and other faults in the same file commented; ran verification on FCC.Impl of the same model, and on the counterexample for property OSAS-S-140, the 5-step counterexample showed that the above fault was false the first four steps and true the fifth step.

dkstewart commented 6 years ago

Officially resolved.