Documentação complementar à tese intitulada “Geração Semiautomática de Máquinas Finitas de Estados Estendidas a partir de documento de padronização do domínio aeroespacial”
Validação do Modelo de Características
Base de Conhecimento
type(document_version, variationpoint).
type(service_description, variationpoint).
type(efsm_information, variationpoint).
type(tcv, variationpoint).
type(acceptance_capabilities, variationpoint).
type(start_execution_capabilities, variationpoint).
type(execution_progress_capabilities, variationpoint).
type(completion_execution_capabilities, variationpoint).
type(v1,variant).
type(v2,variant).
type(tcv,variant).
type(information_edition,variant).
type(text,variant).
type(graphic,variant).
type(acceptance_capabilities, variant).
type(start_execution_capabilities, variant).
type(execution_progress_capabilities, variant).
type(completion_execution_capabilities, variant).
type(acceptance_report_success, variant).
type(acceptance_report_failure, variant).
type(start_execution_report_success, variant).
type(start_execution_report_failure, variant).
type(execution_progress_report_success, variant).
type(execution_progress_report_failure, variant).
type(completion_execution_report_success, variant).
type(completion_execution_report_failure, variant).
variants(document_version,v1).
variants(document_version,v2).
variants(service_description,tcv).
variants(efsm_information,information_edition).
variants(tcv,acceptance_capabilities).
variants(tcv,start_execution_capabilities).
variants(tcv,execution_progress).
variants(tcv,completion_execution).
variants(acceptance_capabilities,acceptance_report_success).
variants(acceptance_capabilities,acceptance_report_failure).
variants(start_execution_capabilities,start_execution_report_success).
variants(start_execution_capabilities,start_execution_report_failure).
variants(execution_progress_capabilities,execution_progress_report_success).
variants(execution_progress_capabilities,execution_progress_report_failure).
variants(completion_execution_capabilities,completion_execution_report_success).
variants(completion_execution_capabilities,completion_execution_report_failure).
max(document_version,1).
max(service_description,2).
max(efsm_information,1).
min(document_version,1).
min(service_description,1).
min(efsm_information,0).
common(document_version,yes).
common(service_description,yes).
common(efsm_information,yes).
common(acceptance_capabilities,yes).
common(acceptance_report_failure,yes).
common(start_execution_report_failure,yes).
common(execution_progress_report_failure,yes).
common(completion_execution_report_failure,yes).
common(v1,no).
common(v2,no).
common(tcv,no).
common(information_edition,no).
common(acceptance_report_success,no).
common(start_execution_capabilities,no).
common(start_execution_report_success,no).
common(execution_progress_capabilities,no).
common(execution_progress_report_success,no).
common(completion_execution_capabilities,no).
common(completion_execution_report_success,no).
requires_v_v(acceptance_report_failure,acceptance_report_success).
requires_v_v(acceptance_report_success,acceptance_report_failure).
requires_v_v(start_execution_report_success,start_execution_report_failure).
requires_v_v(start_execution_report_failure,start_execution_report_success).
requires_v_v(execution_progress_report_success,execution_progress_report_failure).
requires_v_v(execution_progress_report_failure,execution_progress_report_success).
requires_v_v(completion_execution_report_success,completion_execution_report_failure).
requires_v_v(completion_execution_report_failure,completion_execution_report_success).
excludes_v_v(v1,v2).
excludes_v_v(v2,v1).
Regras Implementadas
/* DETERMINAR A VALIDADE DA PL E GERAR UM PRODUTO BÁSICO */
/* REGRA 4.1 pag 85, tese Elfaki */
select(X) :- common(y,yes), common(X,yes), variants(Y,X),type(Y,variationpoint), type(X,variant).
/* REGRA 4.2 pag 85, tese Elfaki */
select(Z) :- select(X)\^requires_v_v(X,Z)\^not(select(Z)), type(X,variant), type(Z,variant).
/* REGRA 4.3 pag 85, tese Elfaki */
notselect(Z) :- select(X),select(Z),excludes_v_v(X,Z), type(X,variant),type(Z,variant).
/* REGRA 4.4 pag 85, tese Elfaki */
notselect(Z) :-select(Z),common(Z,no),select(X)\^requires_v_v(X,Z),notselect(X),type(X,variant), type(Z,variant).
/* REGRA 4.5 pag 85, tese Elfaki */
basic_product :- select(X),not(notselect(X)),type(X,variant).
/* DETERMINAR INCONSISTÊNCIA DIRETA */
/* REGRA 4.6 pag 90, tese Elfaki */
error :- requires_v_v(X,Z), excludes_v_v(Z,X),type(X,variant),type(Z,variant).
/* REGRA 4.7 pag 90, tese Elfaki */
error :-requires_vp_vp(X,Z),excludes_v_v(Z,X),type(X,variationpoint),type(Z,variationpoint).
/* DETERMINAR INCONSITÊNCIA INDIRETA*/
/* REGRA 4.8 pag 92, tese Elfaki */
error :- requires_vp_vp(VP1,VP2),common(V1,yes),common(V2,yes),excludes_v_v(V1,V2),type(VP1,variationpoint),type(VP2,variationpoint),type(V1,variant),type(V2,variant),variants(VP1,V1), variants(VP2,V2).
/* REGRA 4.9 pag 92, tese Elfaki */
error :- requires_vp_vp(VP1,VP2),common(V1,yes),excludes_v_vp(V1,VP2),type(VP1,variationpoint),type(VP2,variationpoint),type(V1,variant),type(V2,variant),variants(VP1,V1), variants(VP2,V2).
/* REGRA 4.10 pag 92, tese Elfaki */
error :- excludes_vp_vp(VP1,VP2),requires_v_vp(V1,VP2),type(VP1,variationpoint),type(VP2,variationpoint),type(V1,variant),type (V2,variant), variants(VP1,V1), variants(VP2,V2).
/* REGRA 4.11 pag 92, tese Elfaki */
error :- excludes_vp_vp(VP1,VP2),requires_v_v(V1,V2),type(VP1,variationpoint),type(VP2,variationpoint),type(V1,variant),type(V2,variant),variants(VP1,V1), variants(VP2,V2).
/* DETERMINAR INCONSISTÊNCIA COMPLETA*/
/* REGRA 4.12 pag 95, tese Elfaki */
error :-excludes_vp_vp(VP1,VP2),common(VP1,yes),common(VP2,yes),type(VP1,variationpoint),type(VP2,variationpoint),type(V1,variant),type(V2,variant),variants(VP1,V1), and variants(VP2,V2).
/* REGRA 4.13 pag 95, tese Elfaki */
error :- common(VP1, yes) \^ common(V1, yes) \^ common(VP2, yes)
^excludes_v_vp(V1,VP2),type(VP1,variationpoint),type(VP2,variationpoint),type(V1,variant),type(V2,variant),variants(VP1,V1), variants(VP2,V2).
/* REGRA 4.14 pag 95, tese Elfaki */
error :- common(VP1,yes),common(V1,yes),common(VP2,yes), common(VP2,yes), excludes_v_v(V1,V2), type(VP1,variationpoint), type(VP2,variationpoint), type(V1,variant), type(V2,variant), variants(VP1,V1), variants(VP2,V2).
/* DETERMINAR INCONSISTÊNCIA CONDICIONAL*/
/* REGRA 4.15 pag 96, tese Elfaki */
error :- excludes_VP_VP(VP1,VP2), common(VP1,no), common(VP2,yes),type(VP1,variationpoint),type(VP2,variationpoint),type(V1,variant), type(V2,variant),variants(VP1,V1), variants(VP2,V2).
/* REGRA 4.16 pag 96, tese Elfaki */
error :- common(V1,yes),common(VP2,yes),common(VP1,no),excludes_v_vp(V1,VP2),type(VP1,variationpoint),type(VP2,variationpoint),type(V1,variant),type(V2,variant),variants(VP1,V1), variants(VP2,V2).
/* REGRA 4.17 pag 96, tese Elfaki */
error :- common(VP1,no),common(V1,yes),common(VP2,yes),common(V2,yes),excludes_v_v(V1,V2),type(VP1,variationpoint),type(VP2,variationpoint),type(V1,variant),type(V2,variant),variants(VP1,V1), variants(VP2,V2).
/* PREVENIR INCONSISTÊNCIA */
/* REGRA 4.18 pag 100, tese Elfaki */
assert(requires_v_v(V1,V3)) :-requires_v_v(V1,V2),requires_v_v(V2,V3),type(VP1,variationpoint),type(VP2,variationpoint),type(VP3,variationpoint),type(V1,variant), type(V2,variant), type(V3,variant).
/* REGRA 4.19 pag 100, tese Elfaki */
assert(requires_vp_vp(VP1,VP3)) :-requires_vp_vp(VP1,VP2),requires_vp_vp(VP2,VP3),type(VP1,variationpoint),type(VP2,variationpoint),type(VP3,variationpoint),type(V1,variant), type(V2,variant), type(V3,variant).
/* REGRA 4.20 pag 100, tese Elfaki */
requires_v_vp(V1,VP2) :-requires_v_vp(V1,VP1)\^requires_vp_vp(VP1,VP2),type(VP1,variationpoint),type(VP2,variationpoint),type(VP3,variationpoint),type(V1,variant), type(V2,variant),type(V3,variant).
/* REGRA 4.21 pag 100, tese Elfaki */
requires_v_vp(V1,VP1) :-requires_v_v(V1,V2),requires_v_vp(V2,VP1),type(VP1,variationpoint),type(VP2,variationpoint),type(VP3,variationpoint),type(V1,variant), type(V2,variant),type(V3,variant).
/* REGRA 4.22 pag 100, tese Elfaki */
excludes_v_v(V1,V3) :-requires_v_v(V1,V2),excludes_v_v(V2,V3),type(VP1,variationpoint),type(VP2,variationpoint),type(VP3,variationpoint),type(V1,variant), type(V2,variant), type(V3,variant).
/* REGRA 4.23 pag 101, tese Elfaki */
excludes_vp_vp(VP1,VP3) :-requires_vp_vp(VP1,VP2,excludes_vp_vp(VP2,VP3),type(VP1,variationpoint),type(VP2,variationpoint),type(VP3,variationpoint),type(V1,variant), type(V2,variant), type(V3,variant).
/* REGRA 4.24 pag 101, tese Elfaki */
excludes_v_vp(V1,VP1) :-requires_v_v(V1,V2),excludes_v_vp(V2,VP1),type(VP1,variationpoint),type(VP2,variationpoint),type(VP3,variationpoint),type(V1,variant), type(V2,variant), type(V3,variant).
/* REGRA 4.25 pag 101, tese Elfaki */
excludes_v_vp(V1,VP2) :-require_v_vp(V1,VP1),excludes_vp_vp(VP1,VP2),type(VP1,variationpoint),type(VP2,variationpoint),type(VP3,variationpoint),type(V1,variant), type(V2,variant),type(V3,variant).
/* DETECTAR DEAD FEATURE POR EXCLUSÃO INDIRETA */
/* REGRA 4.26 pag 103, tese Elfaki */
dead_variant(V3) :-type(V1,variant),type(V2,variant),type(V3,variant),type(VP1,varitionpoint),type(VP2,variationpoint), variants(VP1,V1),variants(VP2,V2),variants(VP2,V3),common(VP1,yes),common(V1,yes),requires_v_v(V1,V2)=max(VP2,n)).
/* DETECTAR DEAD FEATURE POR EXCLUSÃO DIRETA */
/* REGRA 4.27 pag 104, tese Elfaki */
dead_variant(V2) :-common(VP1,yes),excludes_vp_vp(VP1,VP2),variants(VP2,V2),type(VP1,variationpoint),type(VP2,variationpoint),type(V1,variant),type(V2,variant),variants(VP1,V1), variants(VP2,V2).
/* REGRA 4.28 pag 104, tese Elfaki */
dead_variant(V2) :-common(VP1,yes),common(V1,yes),excludes_v_v(V1,V2),type(VP1,variationpoint),type(VP2,variationpoint),type(V1,variant),type(V2,variant),variants(VP1,V1),variants(VP2,V2).
/* REGRA 4.29 pag 104, tese Elfaki */
dead_variant(V2) :-common(VP1,yes),common(V1,yes),excludes_v_vp(V1,VP2),variants(VP2,V2),type(VP1,variationpoint),type(VP2,variationpoint),type(V1,variant),type(V2,variant),variants(VP1,V1), variants(VP2,V2).
/* DETECTAR REDUNDÂNCIA */
/* REGRA 4.30 pag 106, tese Elfaki */
redundancy :-requires_v_v(V1,V2),requires_v_v(V2,V3),requires_v_v(V1,V3),type(V1,variant), type(V2,variant), type(V3,variant), write ('Redundancy: '),write (V1),write(' - '),write(V3).
/* REGRA 4.31 pag 108, tese Elfaki */
redundancy :-type(V1,variant),type(VP2,variationpoint),type(V2,variant),variants(VP2,V2),requires_v_vp(V1,VP2),common(V2,yes),requires_v_v(V1,V2), write('Redundancy:'),write (V1),write(' - '),write(V2).
/* REGRA 4.32 pag 109, tese Elfaki */
redundancy :-type(V1,variant),type(VP2,variationpoint),common(VP2,yes),requires_v_vp(V1,VP2),write('Redundancy: '),write (V1),write(' - '),write(VP2).
/* REGRA 4.33 pag 110, tese Elfaki */
redundancy :-type(VP1,variationpoint),type(V1,variant),type(VP2,variationpoint),variants(VP1,V1),common(V1,yes),requires_vp_vp(VP1,VP2),requires_v_vp(V1,VP2),write('Redundancy: '),write (V1),write(' - '),write(VP2).
/* REGRA 4.34 pag 111, tese Elfaki */
redundancy :-type(VP1,variationpoint),type(V1,variant),type(VP2,variationpoint),type(V2,variant),variants(VP1,V1),variants(VP2,V2),common(V1,yes),common(V2,yes),requires_vp_vp(VP1,VP2),requires_v_v(V1,V2),write('Redundancy: '),write (V1),write(' - '),write(V2).
/* REGRA 4.35 pag 111, tese Elfaki */
redundancy :- type(VP1, variation point),type(VP2, variationpoint),common(VP2,yes),requires_vp_vp(VP1,VP2),write('Redundancy:'),write (VP1),write(' - '),write(VP2).
/* REGRA 4.36 pag 112, tese Elfaki */
redundancy :-type(V1,variant),type(V2,variant),type(VP2,variationpoint),variants(VP2,V2),common(VP2,yes),common(V2,yes),requires_v_v(V1,V2), write('Redundancy: '),write(V1),write(' - '),write(V2).
/* REGRA 4.37 pag 113, tese Elfaki */
redundancy :-type(V1,variant),type(VP2,variationpoint),type(V2,variant),variants(VP2,V2),excludes_v_vp(V1,VP2),excludes_v_v(V1,V2), write('Redundancy: '),write(V1),write('- '),write(V2).
/* REGRA 4.38 pag 114, tese Elfaki */
redundancy :-type(VP1,variationpoint),type(V1,variant),type(VP2,variationpoint),type(V2,varant),variants(VP1,V1),variants(VP2,V2),excludes_vp_vp(VP1,VP2),excludes_v_v(V1,V2),write('Redundancy: '),write(VP1),write(' - '),write(VP2).
A representação dos dados do modelo de características para a validação com a ferramenta Fama-FW é apresentada a seguir:
%Relationships
SMMG: DOCUMENT_VERSION SERVICE_SELECTION EFSM_GENERATION;
DOCUMENT_VERSION: [1,1] {V1 V2};
SERVICE_SELECTION: TCV;
TCV: ACCEPTANCE [START] [PROGRESS] [COMPLET];
ACCEPTANCE: ACC_REP_FAIL ACC_REP_SUCC;
START: STA_REP_FAIL STA_REP_SUCC;
PROGRESS: PRG_REP_FAIL PRG_REP_SUCC;
COMPLET: CMP_REP_FAIL CMP_REP_SUCC;
EFSM_GENERATION: [EDIT_INFORMATION];
%Constraints
STA_REP_FAIL REQUIRES STA_REP_SUCC;
STA_REP_SUCC REQUIRES STA_REP_FAIL;
PRG_REP_FAIL REQUIRES PRG_REP_SUCC;
PRG_REP_SUCC REQUIRES PRG_REP_FAIL;
CMP_REP_FAIL REQUIRES CMP_REP_SUCC;
CMP_REP_SUCC REQUIRES CMP_REP_FAIL;
Codificação em .DVE para a validação da MFEE com o auxílio da ferramenta DIVINE.
Verificação de Telecomando - fluxo normal
byte accSucc, accFail, stSucc, stFail, prSucc, prFail, cmSucc, cmFail;
byte tc=1, succ_repA, succ_repC, succ_repP, succ_repS;
process P_0 {
state without, acceptance, start, progress, completion;
init without;
trans
without -> acceptance {guard tc == 1; effect accSucc=1;},
acceptance -> start { guard accSucc == 1; effect succ_repA=1,stSucc=1; },
acceptance -> start { guard accSucc == 1; effect succ_repA=0,stSucc=1; },
start -> progress { guard stSucc == 1; effect succ_repS=1, prSucc=1; },
start -> progress { guard stSucc == 1; effect succ_repS=0, prSucc=1; },
progress -> completion { guard prSucc == 1; effect succ_repP=1, cmSucc=1;},
progress -> completion { guard prSucc == 1; effect succ_repP=0, cmSucc=1;},
completion -> without { guard cmSucc == 1; effect succ_repC=1; },
completion -> without { guard cmSucc == 1; effect succ_repC=0; };}
process LTL_property {
state q1;
init q1;
accept q1;
trans
q1 -> q1 { guard (P_0.without) && not (P_0.completion); };
}
system async property LTL_property;
Verificação de Telecomando - fluxo de exceções especificadas
byte accSucc, accFail, stSucc, stFail, prSucc, prFail, cmSucc, cmFail;
byte tc=1, succ_repA, succ_repC, succ_repP, succ_repS, cod_errorA=-1,cod_errorS=-1,cod_errorP=-1,cod_errorC=-1;
process P_0 {
state without, acceptance, start, progress, completion;
init without;
trans
without -> acceptance {guard tc == 1; effect accSucc=1;},
acceptance -> start { guard accSucc == 1; effect succ_repA=1, stSucc=1; },
acceptance -> start { guard accSucc == 1; effect succ_repA=0, stSucc=1; },
acceptance -> without { guard accSucc == 0; effect cod_errorA = 0, succ_repA=0;},
acceptance -> without { guard accSucc == 0; effect cod_errorA = 1, succ_repA=0;},
acceptance -> without { guard accSucc == 0; effect cod_errorA = 2, succ_repA=0;},
acceptance -> without { guard accSucc == 0; effect cod_errorA = 3, succ_repA=0;},
acceptance -> without { guard accSucc == 0; effect cod_errorA = 4, succ_repA=0;},
acceptance -> without { guard accSucc == 0; effect cod_errorA = 5, succ_repA=0;},
start -> progress { guard stSucc == 1; effect succ_repS=1, prSucc=1; },
start -> progress { guard stSucc == 1; effect succ_repS=0, prSucc=1; },
start -> without { guard stSucc == 0; effect cod_errorS = 1, succ_repS=0;},
progress -> completion { guard prSucc == 1; effect succ_repP=1, cmSucc=1; },
progress -> completion { guard prSucc == 1; effect succ_repP=0, cmSucc=1; },
progress -> without { guard prSucc == 0; effect cod_errorP = 1, succ_repP=0;},
completion -> without { guard cmSucc == 1; effect succ_repC=1; },
completion -> without { guard cmSucc == 1; effect succ_repC=0; },
completion -> without { guard cmSucc == 0; effect cod_errorC = 1, succ_repC=0;};
}
process LTL_property {
state q1;
init q1;
accept q1;
trans
q1 -> q1 { guard (P_0.without) && not (P_0.completion); };
}
system async property LTL_property;
Procedimento de Operações de bordo - fluxo normal
byte load, delete, stop, start, suspend, abort, resume;
byte tc=1, succ_repA, succ_repC, succ_repP, succ_repS;
process P_0 {
state initial, inactive, running, held;
init initial;
trans
initial -> inactive {effect load=1;},
inactive -> initial { guard load == 1; effect delete=1;},
inactive -> running { guard load == 1; effect start = 1;},
running -> inactive { guard start ==1; effect stop = 1;},
running -> held { guard start == 1; effect suspend = 1;},
running -> inactive { guard start == 1; effect abort = 1;},
held -> running { guard suspend == 1; effect start = 1;};}
process LTL_property {
state q1;
init q1;
accept q1;
trans
q1 -> q1 { guard (P_0.running) && not (P_0.inactive); };}
system async property LTL_property;
Procedimento de Operações de bordo - fluxo de exceções especificadas
byte load, delete, stop, start, suspend, abort, resume;
byte tc=1, succ_repA, succ_repC, succ_repP, succ_repS;
process P_0 {
state initial, inactive, running, held;
init initial;
trans
initial -> inactive {effect load=1;},
inactive -> inactive { guard stop == 1; },
inactive -> inactive { guard resume == 1;},
inactive -> inactive { guard abort ==1;},
inactive -> initial { guard load == 1; effect delete=1;},
inactive -> running { guard load == 1; effect start = 1;},
running -> running { guard load == 1; },
running -> running { guard delete == 1; },
running -> running { guard resume == 1; },
running -> running { guard start == 1; },
running -> inactive { guard start ==1; effect stop = 1;},
running -> held { guard start == 1; effect suspend = 1;},
running -> inactive { guard start == 1; effect abort = 1;},
held -> running { guard suspend == 1; effect start = 1;},
held -> held { guard load == 1;},
held -> held { guard delete == 1;},
held -> held { guard start == 1;},
held -> held { guard suspend == 1;};}
process LTL_property {
state q1;
init q1;
accept q1;
trans
q1 -> q1 { guard (P_0.running) && not (P_0.inactive); };}
system async property LTL_property;
Caso de uso 1 Caso de uso 2 Caso de uso 3 Caso de uso 4 Caso de uso 5 Caso de uso 6 Caso de uso 7
Caso de uso 8 Caso de uso 9 Caso de uso 10 Caso de uso 11 Caso de uso 12 Caso de uso 13 Caso de uso 14
Diagrama de
Classes
Diagramas de
Sequência