Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #641 from ge-high-assurance/check_upd_2022_01
Updates to ASSIST-DV checks
- Loading branch information
Showing
13 changed files
with
655 additions
and
132 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,51 @@ | ||
| % Copyright (c) 2022, Galois, Inc. | ||
| % | ||
| % All Rights Reserved | ||
| % | ||
| % This material is based upon work supported by the Defense Advanced Research | ||
| % Projects Agency (DARPA) under Contract No. FA8750-20-C-0203. | ||
| % | ||
| % Any opinions, findings and conclusions or recommendations expressed in this | ||
| % material are those of the author(s) and do not necessarily reflect the views | ||
| % of the Defense Advanced Research Projects Agency (DARPA). | ||
|
|
||
| :- module(interfaceChecks, | ||
| [ | ||
| check_INTERFACE/1 | ||
| ]). | ||
|
|
||
| :- ensure_loaded('../paths'). | ||
| :- use_module(rack(model)). | ||
|
|
||
|
|
||
| %! check_INTERFACE_no_dest_SYSTEM is det. | ||
| % | ||
| % Checks that no INTERFACE is lacking a destination SYSTEM. | ||
| % Always succeeds, emits warnings. | ||
| % | ||
| % Similar to "nodegroups/query/query dataVer INTERFACE without destination SYSTEM.json" | ||
| % | ||
| check_INTERFACE_no_dest_SYSTEM(IFACE) :- | ||
| check_has_no_rel('http://arcos.rack/SYSTEM#INTERFACE', | ||
| 'http://arcos.rack/SYSTEM#destination', | ||
| 'http://arcos.rack/SYSTEM#SYSTEM', IFACE). | ||
|
|
||
|
|
||
| %! check_INTERFACE_no_src_SYSTEM is det. | ||
| % | ||
| % Checks that no INTERFACE is lacking a source SYSTEM. | ||
| % Always succeeds, emits warnings. | ||
| % | ||
| % Similar to "nodegroups/query/query dataVer INTERFACE without source SYSTEM.json" | ||
| % | ||
| check_INTERFACE_no_src_SYSTEM(IFACE) :- | ||
| check_has_no_rel('http://arcos.rack/SYSTEM#INTERFACE', | ||
| 'http://arcos.rack/SYSTEM#source', | ||
| 'http://arcos.rack/SYSTEM#SYSTEM', IFACE). | ||
|
|
||
| %! check_INTERFACE is det. | ||
| % | ||
| % Performs all checks for INTERFACEs. Always succeeds, emits warnings. | ||
| check_INTERFACE(IFACE) :- | ||
| check_INTERFACE_no_dest_SYSTEM(IFACE); | ||
| check_INTERFACE_no_src_SYSTEM(IFACE). |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,64 @@ | ||
| % Copyright (c) 2022, Galois, Inc. | ||
| % | ||
| % All Rights Reserved | ||
| % | ||
| % This material is based upon work supported by the Defense Advanced Research | ||
| % Projects Agency (DARPA) under Contract No. FA8750-20-C-0203. | ||
| % | ||
| % Any opinions, findings and conclusions or recommendations expressed in this | ||
| % material are those of the author(s) and do not necessarily reflect the views | ||
| % of the Defense Advanced Research Projects Agency (DARPA). | ||
|
|
||
| :- module(sbvt_checks, | ||
| [ | ||
| check_SBVT/1 | ||
| ]). | ||
|
|
||
| :- ensure_loaded('../paths'). | ||
| :- use_module(rack(model)). | ||
|
|
||
| %! check_Result_not_confirmed is det. | ||
| % | ||
| % Checks that no SBVT_Result is lacking a confirming TEST. | ||
| % Always succeeds, emits warnings. | ||
| % | ||
| % NOTE: this test is superfluous since it's already validated by the | ||
| % base checks for cardinality constraints, but it's included here as | ||
| % an example of how a higher-level check might be written. | ||
| % | ||
| % Similar to "nodegroups/query/query | ||
| % dataVer SBVT_Result without confirms_SBVT_Test.json" | ||
| % | ||
| check_Result_not_confirmed(I) :- | ||
| check_has_no_rel('http://arcos.AH-64D/Boeing#SBVT_Result', | ||
| 'http://arcos.rack/TESTING#confirms', | ||
| 'http://arcos.AH-64D/Boeing#SBVT_Test', | ||
| I). | ||
|
|
||
| %! check_no_Test_requirement is det. | ||
| % | ||
| % Checks that no SBVT_Test is lacking a Requirement to verify. | ||
| % Always succeeds, emits warnings. | ||
| % | ||
| % NOTE: the core ontology specifies that an SBVT_Test is a type of | ||
| % TESTING#TEST, and TESTING#verifies specifies it must describe an | ||
| % ENTITY. Here, there is a higher-level semantic assertion that an | ||
| % SBVT_Test must "verifies" a REQUIREMENT. | ||
| % | ||
| % Similar to "nodegroups/query/query dataVer SBVT_Test without REQUIREMENT.json" | ||
| % and "nodegroups/query/query dataVer SRS_Req without verifies SBVT_Test.json" | ||
| % where the latter additionally qualifies the target of the former. | ||
| % | ||
| check_no_Test_requirement(I) :- | ||
| check_has_no_rel('http://arcos.AH-64D/Boeing#SBVT_Test', | ||
| 'http://arcos.rack/TESTING#verifies', | ||
| 'http://arcos.AH-64D/Boeing#SRS_Req', | ||
| %% 'http://arcos.rack/REQUIREMENTS#REQUIREMENT', | ||
| I). | ||
|
|
||
| %! check_SBVT is det. | ||
| % | ||
| % Performs all checks for SBVT classes. Always succeeds, emits warnings. | ||
| check_SBVT(SBVT) :- | ||
| check_Result_not_confirmed(SBVT); | ||
| check_no_Test_requirement(SBVT). |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,52 @@ | ||
| % Copyright (c) 2022, Galois, Inc. | ||
| % | ||
| % All Rights Reserved | ||
| % | ||
| % This material is based upon work supported by the Defense Advanced Research | ||
| % Projects Agency (DARPA) under Contract No. FA8750-20-C-0203. | ||
| % | ||
| % Any opinions, findings and conclusions or recommendations expressed in this | ||
| % material are those of the author(s) and do not necessarily reflect the views | ||
| % of the Defense Advanced Research Projects Agency (DARPA). | ||
|
|
||
| :- module(software_checks, | ||
| [ | ||
| check_SOFTWARE/1 | ||
| ]). | ||
|
|
||
| :- ensure_loaded('../paths'). | ||
| :- use_module(rack(model)). | ||
|
|
||
|
|
||
| %! check_SOFTWARE_partOf_SOFTWARE is det. | ||
| % | ||
| % Checks every SOFTWARE partOf target is a SOFTWARE. | ||
| % Always succeeds, emits warnings. | ||
| % | ||
| % Similar to "nodegroups/query/query dataVer SOFTWARE without partOf SOFTWARE.json" | ||
| % | ||
| check_SOFTWARE_COMPONENT_contained(I) :- | ||
| check_has_no_rel('http://arcos.rack/SOFTWARE#SWCOMPONENT', | ||
| 'http://arcos.rack/SOFTWARE#subcomponentOf', | ||
| 'http://arcos.rack/SOFTWARE#SWCOMPONENT', | ||
| I). | ||
|
|
||
| %! check_SOFTWARE_COMPONENT_impact is det. | ||
| % | ||
| % Checks every SOFTWARE partOf target is a SOFTWARE. | ||
| % Always succeeds, emits warnings. | ||
| % | ||
| % Similar to "nodegroups/query/query dataVer SOFTWARE without partOf SOFTWARE.json" | ||
| % | ||
| check_SOFTWARE_COMPONENT_impact(I) :- | ||
| check_has_no_rel('http://arcos.rack/SOFTWARE#SWCOMPONENT', | ||
| 'http://arcos.rack/PROV-S#wasImpactedBy', | ||
| 'http://arcos.rack/REQUIREMENTS#REQUIREMENT', | ||
| I). | ||
|
|
||
| %! check_SOFTWARE is det. | ||
| % | ||
| % Performs all checks for SOFTWARE classes. Always succeeds, emits warnings. | ||
| check_SOFTWARE(SC) :- | ||
| check_SOFTWARE_COMPONENT_contained(SC); | ||
| check_SOFTWARE_COMPONENT_impact(SC). |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,111 @@ | ||
| % Copyright (c) 2022, Galois, Inc. | ||
| % | ||
| % All Rights Reserved | ||
| % | ||
| % This material is based upon work supported by the Defense Advanced Research | ||
| % Projects Agency (DARPA) under Contract No. FA8750-20-C-0203. | ||
| % | ||
| % Any opinions, findings and conclusions or recommendations expressed in this | ||
| % material are those of the author(s) and do not necessarily reflect the views | ||
| % of the Defense Advanced Research Projects Agency (DARPA). | ||
|
|
||
| :- module(srs_checks, | ||
| [ | ||
| check_SRS/1 | ||
| ]). | ||
|
|
||
| :- ensure_loaded('../paths'). | ||
| :- use_module(rack(model)). | ||
|
|
||
|
|
||
| %! check_SRS_insertion_source is det. | ||
| % | ||
| % Checks that no SRS_Req is inserted by any activity other than | ||
| % "SRS Data Ingestion". Always succeeds, emits warnings. | ||
| % | ||
| % Similar to "nodegroups/query/query dataVer SRS_Req dataInsertedBy other than SRS Data Ingestion.json" | ||
| % | ||
| check_SRS_insertion_source(I) :- | ||
| T = 'http://arcos.AH-64D/Boeing#SRS_Req', | ||
| rack_data_instance(T, I), | ||
| rdf(I, 'http://arcos.rack/PROV-S#dataInsertedBy', A), | ||
| rack_instance_ident(A, AName), | ||
| \+ AName = 'SRS Data Ingestion', | ||
| rack_instance_ident(I, IN), | ||
| rdf(A, rdf:type, ATy), | ||
| print_message(warning, invalid_srs_req_inserter(T, I, IN, ATy, A, AName)). | ||
|
|
||
| %! check_SRS_Req_CSID_or_PIDS is det. | ||
| % | ||
| % Checks every SRS_Req satisfies only a CSID or PIDS. | ||
| % Always succeeds, emits warnings. | ||
| % | ||
| % Similar to "nodegroups/query/query dataVer SRS_Req without CSID or PIDS.json" | ||
| % | ||
| check_SRS_Req_CSID_or_PIDS(I) :- | ||
| T = 'http://arcos.AH-64D/Boeing#SRS_Req', | ||
| rack_data_instance(T, I), | ||
| rdf(I, 'http://arcos.rack/REQUIREMENTS#satisfies', R), | ||
| \+ is_CSID_or_PIDS(R), | ||
| rack_instance_ident(I, Ident), | ||
| rack_instance_ident(R, RIdent), | ||
| rdf(R, rdf:type, RTy), | ||
| print_message(warning, invalid_srs_req_satisfies(T, I, Ident, RTy, R, RIdent)). | ||
|
|
||
| is_CSID_or_PIDS(Inst) :- rdf(Inst, rdf:type, 'http://arcos.AH-64D/Boeing#PIDS_Req'). | ||
| is_CSID_or_PIDS(Inst) :- rdf(Inst, rdf:type, 'http://arcos.AH-64D/Boeing#CSID_Req'). | ||
|
|
||
|
|
||
| %! check_SRS_Req_description is det. | ||
| % | ||
| % Checks every SRS_Req has a PROV-S description | ||
| % Always succeeds, emits warnings. | ||
| % | ||
| % Similar to "nodegroups/query/query dataVer SRS_Req without description.json" | ||
| % | ||
| check_SRS_Req_description(I) :- | ||
| check_has_no_rel('http://arcos.AH-64D/Boeing#SRS_Req', | ||
| 'http://arcos.rack/PROV-S#description', | ||
| I). | ||
|
|
||
|
|
||
| %! check_SubDD_Req_satisifies_SRS_Req is det. | ||
| % | ||
| % Checks every SubDD_Req satisifes an SRS_Req. | ||
| % Always succeeds, emits warnings. | ||
| % | ||
| % Similar to "nodegroups/query/query dataVer SubDD_Req without satisfies SRS_Req.json" | ||
| % | ||
| check_SubDD_Req_satisfies_SRS_Req(I) :- | ||
| check_has_no_rel('http://arcos.AH-64D/Boeing#SubDD_Req', | ||
| 'http://arcos.rack/TESTING#satisifes', | ||
| 'http://arcos.AH-64D/Boeing#SRS_Req', | ||
| I). | ||
|
|
||
|
|
||
| prolog:message(invalid_srs_req_inserter(ITy, Inst, InstIdent, InsTy, InsI, InsN)) --> | ||
| { prefix_shorten(ITy, SIT), | ||
| prefix_shorten(Inst, SII), | ||
| prefix_shorten(InsTy, STT), | ||
| prefix_shorten(InsI, STI) | ||
| }, | ||
| [ '~w instance ~w (~w) inserted by invalid ACTIVITY: ~w ~w (~w)'-[ | ||
| SIT, SII, InstIdent, STT, STI, InsN ] ]. | ||
| prolog:message(invalid_srs_req_satisfies(ITy, Inst, InstIdent, TgtTy, Tgt, TgtIdent)) --> | ||
| { prefix_shorten(Inst, SI), | ||
| prefix_shorten(ITy, ST), | ||
| prefix_shorten(Tgt, SR), | ||
| prefix_shorten(TgtTy, SRT) | ||
| }, | ||
| [ '~w instance ~w (~w) satisifes something not a PIDS_Req or CSID_Req: ~w ~w (~w)'-[ | ||
| ST, SI, InstIdent, SRT, SR, TgtIdent ] ]. | ||
|
|
||
|
|
||
| %! check_SRS is det. | ||
| % | ||
| % Performs all checks for SRS classes. Always succeeds, emits warnings. | ||
| check_SRS(SRS) :- | ||
| check_SRS_insertion_source(SRS); | ||
| check_SRS_Req_CSID_or_PIDS(SRS); | ||
| check_SRS_Req_description(SRS); | ||
| check_SubDD_Req_satisfies_SRS_Req(SRS). |
Oops, something went wrong.