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

 Prime: IFAD
 Partners (6) including: Ansaldo, I; OSS, DK;
PdM, I; SSG, F
 Tool extensions including
 Java code generator
 Rose-VDM++ mapper
 Extensions and improvements of VDM++
21
IFAD
IFAD
VICE
 VICE = VDM++ Specification In a
Constrained Environment
 Prime: Matra Bae Dynamics, France
 Tool extensions including
 Support for real-time
 Parallel interpreter
 Extensions and improvements of
VDM++
22
IFAD
IFAD
PROSPER
 Proof and Specification Assisted Design
Environments
 Prime: Glasgow University, UK
 Partners (6) including: Cambridge Uni, UK;
Prover Technology, S, Edinburgh Uni, UK
 Long-term Research
 Proof support for IFAD VDM-SL Toolbox
 Engineer from RTRI for two years
23
IFAD
IFAD
European Industrial use of FM
 European Academia
 FME Profile
 The ESPRIT Programme
European Tool Support
 Example Industrial Projects
 Concluding Remarks
24
IFAD
IFAD
European Tool Support
 VDMTools from IFAD
 Atelier-B from Stéria Méditérranée
 B-Toolbox from B-Core
 FDR from Formal Systems Europe
 NP Tools from Prover Technology
 Telelogic Tau from Telelogic
 Lots of prototype/academic tools
25
IFAD
IFAD
VDMTools
 Company: IFAD, Denmark
 Main users: Boeing, BAe, GAO, Chess
 Notations: VDM-SL and VDM++
 A suite of professional software
development tools for modelling,
validation and code generation
 Rose VDM++ link
 VDM-SL & VDM++ tools
 C++ & Java Code Generators
26
IFAD
IFAD
Atelier-B
 Company: Stéria Méditérranée, France
 Main users: Matra, Alstrom
 Notations: B
 Professional development tools for
modelling, refinement and proof
 Automatic proof support
 Formal refinement support
 Limited code generation to C
27
IFAD
IFAD
B-Toolbox
 Company: B-Core, UK
 Main users: IBM
 Notations: B
 Professional development tools for
modelling, some proof and code
generation
 Very small organisation
 Some proof support
 Limited code generation to C
28
IFAD
IFAD
FDR
 Company: Formal Systems Europe, UK
 Main users: DERA
 Notations: CSP
 Professional development tools for
model-checking CSP descriptions
 Very small organisation
 Automatic model-checking
29
IFAD
IFAD
NP Tools
 Company: Prover Technology, Sweden
 Main users: Swedish Railways, Intel
 Notations: Logic
 Professional development tools for
model-checking first-order propositional
logic
 Automatic model-checking
 Low level descriptions
30
IFAD
IFAD
Telelogic Tau
 Company: Telelogic, Sweden
 Main users: Telecom companies
 Notations: SDL, MSC, UML
 Professional development tools for
modelling and validating SDL
descriptions
 Professional user interface
 Monopoly in telecom sector
 Rather low level
31
IFAD
IFAD
European Industrial use of FM
 European Academia
 FME Profile
 The ESPRIT Programme
 European Tool Support
Example Industrial Projects
 Concluding Remarks
32
IFAD
IFAD
Example Industrial
Projects
 DDC Ada Compiler
 CICS
 Sizewell B
 Transputer
 Airbus CIDS
 CDIS
 SACEM
 Météor
 SHOLIS
 Mondex smart card
 ConForm
 DustExpert
 CAVA
 Dutch DoD
 BPS 1000
 Flower Auction
 SPOT4
 K-LINE
 VDMTools/MUSTER
33
IFAD
IFAD
DDC Ada Compiler (197X)
 Organisation: DDC (Denmark)
 Domain: Compiler
 Tools: VDM notation
　
中國航空網 www.k6050.com
航空翻譯 www.aviation.cn
本文鏈接地址：航空資料31(6)