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

 Experience:
 First European validated Ada compiler
 Cheaper than without FM
 No verification or validation
 Tools are lacking
34
IFAD
IFAD
CICS (198X)
 Organisation: IBM (UK)
 Domain: Transaction Processing
 Tools: Z notation
 Experience:
 Reduction in development cost: 9%
 Code developed from Z had 2½ times fewer
problems
 Parsing, type checking tools increased
productivity
35
IFAD
IFAD
Sizewell B (198X)
 Organisation: TACS, UK
 Domain: Nuclear
 Tools: Malpas
 Experience:
 100000 lines of code
 Formal verification at source code
 About 200 man years of effort!
 Still favourable compared to retesting
36
IFAD
IFAD
Transputer
 Organisation: INMOS, UK
 Domain: Processor with floating-point
hardware
 Tools: Z notation
 Experience:
 IEEE standard formalised in Z
 occam code derived from Z
 Many algorithm errors discovered
 Commercial success
 Queen’s Award for Technological Achievements
37
IFAD
IFAD
Airbus CIDS (199X)
 Organisation: DST, Germany
 Domain: Avionics
 Tools: DST-Z + Kiel Uni prototype
 Experience:
 Uncovered many logical errors
 Straight forward to implement from Z
 Test case derivation initiated
38
IFAD
IFAD
CDIS (199X)
 Organisation: Praxis, UK
 Domain: Air Traffic Control
 Tools: VDM and CCS notations
 Experience:
 No net cost in using formal methods
 Quality of the software was much higher
 Defect rate of about 0.75 faults per KLOC
 Tools from VIP too prototypic
39
IFAD
IFAD
SACEM (198X)
 Organisation: GEC Alsthom, France
 Domain: Railways (Paris RER)
 Tools: B-Toolkit (early version)
 Experience:
 Formal refinement in B
 Verification but no animation
 Same price as for non FM development
 Tools improved during project
 High customer satisfaction
40
IFAD
IFAD
Météor (199X)
 Organisation: Matra Transport, France
 Domain: Railways (Paris Metro)
 Tools: Atelier-B
 Experience:
 Cost savings for safety-critical software
 Formal refinements
 Formal verification
 Tools improved during project
41
IFAD
IFAD
SHOLIS (199X)
 Organisation: Praxis (UK) for
Lockheed’s C130J
 Domain: Avionics (Military, Helicopter)
 Tools: SPARK and CADiZ
 Experience:
 Z Specification verification efficient
 SPARK code verification less efficient
 Better tool support needed
42
IFAD
IFAD
Mondex Smart Card (1999)
 Organisation: LOGICA, UK
 Domain: Smart card for e-finance
 Tools: Z notation
 Experience:
 Big security risk of financial loss
 Security verified by hand
 Major security flaw detected
 First successful ITSEC E6
 Repeated on other projects
43
IFAD
IFAD
ConForm(1994)
 Organisation: British Aerospace (UK)
 Domain: Security (gateway)
 Tools: The IFAD VDM-SL Toolbox
 Experience:
 Prevented propagation of error
 Successful technology transfer
 At least 4 more applications without support
 Statements:
 “Engineers can learn the technique in one week”
 “VDMTools can be integrated gradually into a
traditional existing development process”
44
IFAD
IFAD
DustExpert (1995-7)
 Organisation: Adelard (UK)
 Domain: Safety (dust explosives)
 Tools: The IFAD VDM-SL Toolbox
 Experience:
 Delivered on time at expected cost
 Large VDM-SL specification
 Testing support valuable
 Statement:
 “Using VDMTools we have achieved a
productivity and fault density far better than
industry norms for safety related systems”
45
　
中國航空網 www.k6050.com
航空翻譯 www.aviation.cn
本文鏈接地址：航空資料31(7)