Skip to content

Commit

Permalink
Add the safety annex
Browse files Browse the repository at this point in the history
  • Loading branch information
kfhoech committed Sep 9, 2020
1 parent 2ce4c6f commit a25ab4b
Show file tree
Hide file tree
Showing 3 changed files with 26 additions and 4 deletions.
20 changes: 20 additions & 0 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,26 @@ computational functions in Resolute annex libraries, i.e., Resolute
annex clauses placed directly in an AADL package. The verification
results are then displayed in a view labeled Assurance Case.

## Safety Analysis

The Safety Annex for the Architecture Analysis and Design Language (AADL)
provides the ability to reason about faults and faulty component behaviors in
AADL models. In the Safety Annex approach, we use formal assume-guarantee
contracts to define the nominal behavior of system components. The nominal
model is then verified using the Assume Guarantee Reasoning Environment
(AGREE). The Safety Annex provides a way to weave faults into the nominal
system model and analyze the behavior of the system in the presence of faults.
We also providea library of common faultnode definitions that is customizable
to the needs of system and safety engineers. The Safety Annex supports model
checking and quantitative reasoning by attaching behavioral faults to
components and then using the normal behavioral propagation and proof
mechanisms built into the AGREE AADL annex. This allows users to reason about
the evolution of faults over time, and produce counterexamples demonstrating
how component faults lead to system failures. It can serve as the shared model
to capture system design and safety-relevant information, and produce both
qualitative and quantitative description of the causal relationship between
faults/failures and system safety requirements.

## BriefCASE

BriefCASE is a collection formal system modeling and transformation
Expand Down
5 changes: 3 additions & 2 deletions compositeArtifacts.xml
Original file line number Diff line number Diff line change
Expand Up @@ -3,11 +3,12 @@
<repository name='&quot;Eclipse Project Test Site&quot;'
type='org.eclipse.equinox.internal.p2.artifact.repository.CompositeArtifactRepository' version='1.0.0'>
<properties size='1'>
<property name='p2.timestamp' value='1243822505000'/>
<property name='p2.timestamp' value='1599663305628'/>
</properties>
<children size='5'>
<children size='6'>
<child location='https://raw.githubusercontent.com/loonwerks/AGREE-Updates/master/'/>
<child location='https://raw.githubusercontent.com/loonwerks/Resolute-Updates/master/'/>
<child location='https://raw.githubusercontent.com/loonwerks/AMASE/master/safety-update-site/'/>
<child location='https://raw.githubusercontent.com/loonwerks/BriefCASE-Updates/master/'/>
<child location='https://raw.githubusercontent.com/loonwerks/jkind-plugin/master/compositeRepository/'/>
<child location='https://raw.githubusercontent.com/loonwerks/z3-plugin/master/com.collins.trustedsystems.z3.updates/target/repository/'/>
Expand Down
5 changes: 3 additions & 2 deletions compositeContent.xml
Original file line number Diff line number Diff line change
Expand Up @@ -3,11 +3,12 @@
<repository name='&quot;Eclipse Project Test Site&quot;'
type='org.eclipse.equinox.internal.p2.metadata.repository.CompositeMetadataRepository' version='1.0.0'>
<properties size='1'>
<property name='p2.timestamp' value='1243822505000'/>
<property name='p2.timestamp' value='1599663305628'/>
</properties>
<children size='5'>
<children size='6'>
<child location='https://raw.githubusercontent.com/loonwerks/AGREE-Updates/master/'/>
<child location='https://raw.githubusercontent.com/loonwerks/Resolute-Updates/master/'/>
<child location='https://raw.githubusercontent.com/loonwerks/AMASE/master/safety-update-site/'/>
<child location='https://raw.githubusercontent.com/loonwerks/BriefCASE-Updates/master/'/>
<child location='https://raw.githubusercontent.com/loonwerks/jkind-plugin/master/compositeRepository/'/>
<child location='https://raw.githubusercontent.com/loonwerks/z3-plugin/master/com.collins.trustedsystems.z3.updates/target/repository/'/>
Expand Down

0 comments on commit a25ab4b

Please sign in to comment.