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

Present :
 The complete methodology has to be defined
 CDL (Context + Properties) has to be integrated in OBP for more experimentations
 Definition of MDA components (Adaptation and Proof units) in progress
 Development of OBP V2 in progress
 CDL experimentation in progress
MoDeVVa @ ICST 2008 14 / 29
Outline
1. Context and Motivations
2. Experimentations : Thales Air Systems, Airbus CSSI
3. Context Description Language (CDL)
4. Conclusion and perspectives
MoDeVVa @ ICST 2008 15 / 29
Environment description : What features do engineer have ?
System model
to be
validated
Most of the time engineers have specification and analysis documents with :
not formalized and incomplete textual descriptions
some actors with sequence diagrams
use cases
…
Environment model
formalization
MoDeVVa @ ICST 2008 16 / 29
Context Description Language
DSL : Context Description Language
Formals properties (Patterns)
Description of all the system environment
MoDeVVa @ ICST 2008 17 / 29
Activity diagrams
Sequence
diagrams
The verification context [Jon Whittle , Jean-Charles Roger]
MoDeVVa @ ICST 2008 18 / 29
Eclipse CDL editor
Eclipse CDL editor (develop with GMF)
MoDeVVa @ ICST 2008 19 / 29
Context unfolding and partitioning
The unfolding action provides partitioning:
• Executions without cycles
• Actions count
Finished and acyclic concrete context
Finite number of paths
CDL
Model
MoDeVVa @ ICST 2008 20 / 29
Properties definition
In most cases, the requirement description :
•Is ambiguous
•Refers:
to the state of the system
to a history of system or environment behaviour
(described “somewhere else")
to an implicit behaviour knowledge of the of the system
and its environment
MoDeVVa @ ICST 2008 21 / 29
Proof context description
Context
model
Properties
model
Proof context
CDL (Context Description Language)
Inspired by [Whittle 05]
Adapted in [Roger 06]
Extended in [de Belloy & Dhaussy 07]
Property patterns
Inspired by [Smith et al. 02, Dwyers M.B
et al. 99, Konrad S. and Cheng B. 05]
1- extended in [Dhaussy et al. 07]
2 – linked to the context
MoDeVVa @ ICST 2008 22 / 29
Property patterns : extension (Response)
[Dhaussy et al., 07]
[ Scope ]
[ An, All ] [ ORDER / COMBINED ]
if ( condition_m0 )
[ Pre-arity ] occurrences of x0
…
if ( condition_mk )
[ Post-arity ] occurrences of xk
END
[ Immediacy ] leads to [ < to ]
[ An, All ] [ ORDER / COMBINED ]
if ( condition_n0 )
[ Post-arity ] occurrences of y0
…
if ( condition_nk )
[ Post-arity ] occurrences of yk’
END
x0 [ Nullity ] occurs, …, xk [ Nullity ] occurs
one of [ y0, … yk’ ] [ Precedency ] occurs before the first one of [ x0, … xk ]
[ Repeatability ]
Inspired by [Smith et al. 02, Dwyers M.B et al. 99, Konrad S. and Cheng B. 05]
Global, Before, After, Between, After-Until
Immediately, Eventually
Exactly one,
One or more
May Never,
Must
True, False Cannot, May
MoDeVVa @ ICST 2008 23 / 29
Methodology for property definition
1. choice of the pattern (with events)
2. choice of options and guards
3. choice of the scope
4. link to a node of the context
Context
model
Properties
model
Proof
context
P1
P2
P3
Pn
Observer
automata
(formal
semantic)
automatic
generation
MoDeVVa @ ICST 2008 24 / 29
Observer automata generation
MoDeVVa @ ICST 2008 25 / 29
Outline
1. Context and Motivations
2. Experimentations : Thales Air Systems, Airbus CSSI
3. Context Description Language (CDL)
4. Conclusion and perspectives
MoDeVVa @ ICST 2008 26 / 29
Integration of CDL graphic editors (context and properties):
FIACRE code generation (TopCased project): proving tools connection
Managing contexts (thesis CIFRE CS-SI): completeness and consistency
Studying on different abstraction levels : traceability for properties
Properties (time, frequency,…)
Case studies underway:
Specifications SoS (DGA / MRIS), embedded components (Thales Air Systems)
Avionic protocols Airbus-ATC (CS-SI), dev. process (CNES)
Methodology: MDA Components (Units of proof):
　
中國航空網 m.k6050.com
航空翻譯 www.aviation.cn
本文鏈接地址：航空資料19(191)