曝光臺 注意防騙 網曝天貓店富美金盛家居專營店坑蒙拐騙欺詐消費者

DOMINO Project (RNTL), MOPCOM-ING (Submitted DGE)
Conclusion and Perspectives
MoDeVVa @ ICST 2008 27 / 29
Concret
contexts,
Set of paths
α-contexts,
α-actions
(Intermediate
format)
Composition,
exploration
(IFx)
Simulation
CDL Model
(Contexts,
proprerties,
restrictions)
Model to
be validated
(IF2)
Analysis
data
return
Import (Transformations)
Prototype tool (Observer-Based Prover)
IF2 Programs
Transformations (java)
Observers
Automata
(properties)
Restriction
automata
unfolding
(Java)
Partitioning
(Java)
Vers 1.0 available (open-source) : TopCased project : http://gforge.enseeiht.fr/projects/obp/
OBP : version 2.0 (under development)
MoDeVVa @ ICST 2008 28 / 29
Thank you for your attention
MoDeVVa @ ICST 2008 29 / 29
APPENDIX
MoDeVVa @ ICST 2008 30 / 29
Entity_1
init
Entity_2 Entity_3
Level 1 :
Level 3 :
Sequence Activity diagrams
diagrams
action0
action1 action2
action3 action4 action5
Entity 3
Level 2 :
Properties :
P1 : … ;
P2 : … ;
P3 : … ;
Restrictions :
R1 : … ;
action3 << property >>
P3
<< property >>
P1
<< property >>
P2
<< restriction >>
R1
CDL (Context Description Language) [Whi05 , Rog06, Dha07]
MoDeVVa @ ICST 2008 31 / 29
CDL Meta model
(context)
MoDeVVa @ ICST 2008 32 / 29
CDL Meta model
(properties)
MoDeVVa @ ICST 2008 33 / 29
Initialization
Configuration
initialization
State_managment Config_managment Cond_managment
<< Property >>
REQ_S_CP_SUPSTATE_0320
CDL model Level 1
MoDeVVa @ ICST 2008 34 / 29
Env S_CP
CP_requested_conf’(‘Ready_to_fire’)
Req_accepted
Env S_CP
CP_INIT_ULT_status’(‘Ready’)
Condition_manage
Env S_CP
AIC_CP_change_req_CP_readiness_state
CP_state_manage
CP_status’(‘Immediate_Notice’)
Ra_To_I_Pmpi
Req_not_ok Req_accepted
cancel
Config_managment
Req_error
stop
ok
Level 2
CDL model Level 2 & 3 Level 3
MoDeVVa @ ICST 2008 35 / 29
CDL example
MoDeVVa @ ICST 2008 36 / 29
CDL level 1 example 1/2
MoDeVVa @ ICST 2008 37 / 29
CDL level 1 example 2/2
MoDeVVa @ ICST 2008 38 / 29
CDL level 2 and 3 example
MoDeVVa @ ICST 2008 39 / 29
REQ_SM_SUPSTATE_0320
Suite à une requête légale de changement d'état de 'Minimal Notice Normal' à 'Immediate
Notice Normal' provenant du CSCI AIC (Invoquée par PAAMS(E) uniquement) ou du CSCI
PMPI 'ANY_SM_request_of_change_of_PAAMS_readiness_state', le CSCI SM doit refuser la
requête si le système de navigation est indisponible (le dernier message
'PMPI_ANY_NAVS_availability' contenait dans le champ 'NAVS_availability' la valeur 'FALSE').
Sinon, le CSCI SM accepte la requête de changement d'état et doit envoyer :
• aux CSCIs AIC (Applicable à PAAMS(E) uniquement) et PMPI le message
'SM_ANY_PAAMS_status' contenant dans le champ 'PAAMS_requested_readiness_state'
la valeur 'Immediate Notice Normal';
• au CSCI VOI le message 'SM_VOI_VLS_requested_state' contenant dans le champ
'VLS_requested_state' la valeur 'Ready_to_fire'.
• (Applicable à PAAMS(E)) au CSCI INT le message 'SM_INT_ULT_requested_state'
contenant dans le champ 'ULT_requested_state' la valeur 'Ready'.
Le CSCI SM est alors en phase de transition.
END_REQ_SM_SUPSTATE_0320
Execution
context
Requirement specification : an example (Thales Air Systems)
MoDeVVa @ ICST 2008 40 / 29
Observers automata generation
MoDeVVa @ ICST 2008 41 / 29
Observers automata generation
MoDeVVa @ ICST 2008 42 / 29
CDL
P
<< property >>
Diagramme de scénarios Observateur
Scénario
Observers Activation
MoDeVVa @ ICST 2008 43 / 29
CDL
P
<< property >>
Diagramme de scénarios Observateur
Scénario
start
Actif
Observers Activation
MoDeVVa @ ICST 2008 44 / 29
CDL
P
<< property >>
Diagramme de scénarios Observateur
Scénario
stop
Inactif
Observers Activation
MoDeVVa @ ICST 2008 45 / 29
Some patterns
　
中國航空網 m.k6050.com
航空翻譯 www.aviation.cn
本文鏈接地址：航空資料19(192)