FORMAL SPECIFICATION IN THE DEVELOPMENT OF INDUSTRIAL APPLICATIONS - SUBWAY SPEED CONTROL-SYSTEM

被引：0
|
作者：
DASILVA, C [1 ]
DEHBONEI, B [1 ]
MEJIA, F [1 ]
机构：
[1] GEC ALSTHOM,DIV TRANSPORT,F-93404 ST OUEN,FRANCE
来源：
IFIP TRANSACTIONS C-COMMUNICATION SYSTEMS | 1993年 / 10卷
关键词：
SOFTWARE ENGINEERING; REQUIREMENTS SPECIFICATIONS; PROGRAM VERIFICATION; LOGICS AND MEANINGS OF PROGRAMS; SPECIFYING AND VERIFYING AND REASONING ABOUT PROGRAMS;
D O I：
暂无
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
The paper describes the Subway Speed Control System (SSCS) as an example of industrial use of formal specification and development methods. The first part explains the insights of the B formal development process, designed by J.R. Abrial: Specification and implementation through refinements where each refinement step is proved using axioms based on the first-order predicate logic and an extension of the Zermelo set theory. The second part presents the specification of a small part of the SSCS and the related refinement. One of the associated proof obligations is selected. Then, the set of mathematical rules that allows this proof obligation to be proved by our automatic prover is detailed. Finally, statistics on the utilization of formal development methods in two of our projects are given.
引用
收藏
页码：199 / 213
页数：15
相关论文
共 50 条
  • [31] THE DEVELOPMENT AND PROOF OF A FORMAL SPECIFICATION FOR A MULTILEVEL SECURE SYSTEM
    GLASGOW, JI
    MACEWEN, GH
    ACM TRANSACTIONS ON COMPUTER SYSTEMS, 1987, 5 (02): : 151 - 184
  • [32] Control-system development of a high-speed electromagnetic actuator in consideration of the delay in the control force
    Higaki, J
    Imagi, A
    Yoshikuwa, Y
    Kim, TH
    Yoshizawa, T
    Sugawara, M
    IECON 2004 - 30TH ANNUAL CONFERENCE OF IEEE INDUSTRIAL ELECTRONICS SOCIETY, VOL. 1, 2004, : 672 - 677
  • [33] BASIC CONSIDERATIONS ON APPLICATIONS OF OPTIMAL-CONTROL AND THE MICROPROCESSOR TO THE INDUCTION-MOTOR SPEED CONTROL-SYSTEM
    TSUCHIYA, T
    INTERNATIONAL JOURNAL OF CONTROL, 1980, 31 (02) : 285 - 302
  • [34] MUSCULAR CONTROL OF A LEARNED MOVEMENT - THE SPEED CONTROL-SYSTEM HYPOTHESIS
    ENOKA, RM
    EXPERIMENTAL BRAIN RESEARCH, 1983, 51 (01) : 135 - 145
  • [35] DEVELOPMENT OF A DIGITAL EXCITATION CONTROL-SYSTEM
    HINGSTON, RS
    HAM, PAL
    GREEN, NJ
    FOURTH INTERNATIONAL CONFERENCE ON ELECTRICAL MACHINES AND DRIVES, 1989, 310 : 125 - 129
  • [36] RF CONTROL-SYSTEM DEVELOPMENT AT CEBAF
    SIMROCK, S
    HOVATER, C
    JONES, S
    FUGITT, J
    PROCEEDINGS OF THE 1989 IEEE PARTICLE ACCELERATOR CONFERENCE, VOLS 1-3: ACCELERATOR SCIENCE AND TECHNOLOGY, 1989, : 1885 - 1887
  • [37] THE DEVELOPMENT OF A ROBOTIC COMPLIANCE CONTROL-SYSTEM
    YAN, J
    ELBARADIE, MA
    HASHIMI, MSJ
    INTERNATIONAL JOURNAL OF MACHINE TOOLS & MANUFACTURE, 1992, 32 (04): : 477 - 486
  • [38] DEVELOPMENT OF AN INTEGRATED PROPULSION CONTROL-SYSTEM
    LAMPARD, GWN
    BATKA, JJ
    ASTRONAUTICS & AERONAUTICS, 1976, 14 (04): : B27 - B27
  • [39] MODEL FOR DEVELOPMENT OF AN AUTOMATED CONTROL-SYSTEM
    MELNIKOV, YN
    PETERSON, EY
    ENGINEERING CYBERNETICS, 1974, 12 (JAN-F): : 47 - 51
  • [40] SOME PERSPECTIVES IN CONTROL-SYSTEM DEVELOPMENT
    TRAPEZNIKOV, VA
    AUTOMATION AND REMOTE CONTROL, 1981, 42 (02) : 139 - 144
12345