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

IFAD
IFAD
Adelard Metrics
 31 faults in Prolog and C++ (< 1/kloc)
 Most minor, only 1 safety-related
 1 (small) design error, rest in coding
Initial requirements 450 pages
VDM specification 16kloc (31 modules)
12kloc (excl comments)
Prolog
implementation
37kloc
16kloc (excl comments)
C++ GUI
implementation
23kloc
18kloc (excl comments)
46
IFAD
IFAD
CAVA (1998-)
 Organisation: Baan (Denmark)
 Domain: Constraint solver (Sales Configuration)
 Tools: The IFAD VDM-SL Toolbox
 Experience:
 Common understanding
 Faster route to prototype
 Earlier testing
 Statement:
 “VDMTools has been used in order to increase
quality and reduce development risks on high
complexity products”
47
IFAD
IFAD
Dutch DoD (1997-8)
 Organisation: Origin, The Netherlands
 Domain: Military
 Tools: The IFAD VDM-SL Toolbox
 Experience:
 Higher level of assurance
 Mastering of complexity
 Delivered at expected cost and on schedule
 No errors detected in code after delivery
 Statement:
 “We chose VDMTools because of high demands
on maintainability, adaptability and reliability”
48
IFAD
IFAD
DoD, NL Metrics (1)
 Estimated 12 C++ loc/h with manual coding!
kloc hours loc/hour
spec 15 1196 13
manual impl 4 471 8.5
automatic impl 90 0 NA
test NA 612 NA
total code 94 2279 41.2
totAL
49
IFAD
IFAD
DoD - Comparative Metrics
CODING TESTING
ANALYSIS & CODING TESTING
DESIGN
Traditional:
VDMTools®:
Cost
ANALYSIS &
DESIGN
900 2000 700
1200 500 600
0% 64%
100%
50
IFAD
IFAD
BPS 1000 (1997-)
 Organisation: GAO, Germany
 Domain: Bank note processing
 Tools: The IFAD VDM-SL Toolbox
 Experience:
 Better understanding of sensor data
 Errors identified in other code
 Savings on maintenance
 Statement:
 VDMTools provides unparalleled support for design
abstraction ensuring quality and control throughout
the development life cycle.
51
IFAD
IFAD
Flower Auction (1998)
 Organisation: Chess, The Netherlands
 Domain: Financial transactions
 Tools: The IFAD VDM++ Toolbox
 Experience:
 Successful combination of UML and VDM++
 Use iterative process to gain client commitment
 Implementers did not even have a VDM course
 Statement:
 “The link between VDMTools and Rational Rose is
essential for understanding the UML diagrams”
52
IFAD
IFAD
SPOT 4 (1999)
 Organisation: CS-CI, France
 Domain: Space (payload for SPOT4 satellite)
 Tools: The IFAD VDM-SL Toolbox
 Experience:
 38 % less lines of source code
 36 % less overall effort
 Use of automatic C++ code generation
 Statement:
The cost of applying Formal methods is
significantly lower than without them.
53
IFAD
IFAD
K-LINE
 Organisation: Sidereus, Portugal
 Domain: reverse engineering of database systems
 Tools: The IFAD VDM-SL/++ Toolbox
 Experience:
 Development of a tool for FM-based data-intensive
operations (data-migration and data-quality)
 Semi-automatic generation of ISO/IEC 13817-1 abstract
descriptions out of informal or poorly structured meta-data.
 Statement:
 Formal properties of data provide a firm basis for quality
control in maintaining legacy information systems, thus
saving costs in data cleansing/reverse specification
contracts.
54
IFAD
IFAD
IFAD VDM Applications
 VDMTools
 VDM interpreter
 VDM static semantics
 VDM to C++ code generator
 Specification manager
 UML mapper
 Java static semantics
 Java VDM++ translator
 MUSTER: Emergency response training
55
IFAD
IFAD
VDM++ VDM++ VDM++ VDM++
VDM++ VDM++ VDM++ VDM++
The “Bootstrapping” Process
VDM-SL
DS spec
VDM-SL
　
中國航空網 www.k6050.com
航空翻譯 www.aviation.cn
本文鏈接地址：航空資料31(8)