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 条
  • [1] IMPLEMENTATION OF A MODEL LIFT CONTROL-SYSTEM FROM A FORMAL SPECIFICATION
    MOCEK, JP
    MCDERMID, JA
    SOFTWARE ENGINEERING JOURNAL, 1987, 2 (03): : 71 - 79
  • [2] INDUSTRIAL APPLICATIONS OF THE 473L COMMAND AND CONTROL-SYSTEM - PLAN DEVELOPMENT
    BERLINER, HJ
    OPERATIONS RESEARCH, 1963, 11 : B126 - B127
  • [3] DEVELOPMENT OF A VOICE SPEED CONTROL-SYSTEM LSI
    BABA, H
    ONISHI, N
    SAKASHITA, Y
    TOKIZAWA, H
    TANAKA, H
    IEEE TRANSACTIONS ON CONSUMER ELECTRONICS, 1995, 41 (03) : 909 - 916
  • [4] FORMAL SPECIFICATION AND MECHANICAL VERIFICATION OF SIFT - A FAULT-TOLERANT FLIGHT CONTROL-SYSTEM
    MELLIARSMITH, PM
    SCHWARTZ, RL
    IEEE TRANSACTIONS ON COMPUTERS, 1982, 31 (07) : 616 - 630
  • [5] ONLINE PRODUCTION CONTROL-SYSTEM WITH PROCESS COMPUTERS FOR INDUSTRIAL APPLICATIONS
    ALBERT, KH
    WILLINGER, R
    SIEMENS ZEITSCHRIFT, 1977, 51 (09): : 758 - 760
  • [6] MICROPROCESSOR SPEED CONTROL-SYSTEM
    LIN, AK
    KOEPSEL, WW
    IEEE TRANSACTIONS ON INDUSTRIAL ELECTRONICS AND CONTROL INSTRUMENTATION, 1977, 24 (03): : 241 - 247
  • [7] SPECIFICATION, INSTALLATION AND COMMISSIONING OF A LARGE INDUSTRIAL CONTROL-SYSTEM FOR THE LEP2 CRYOGENICS
    KUHN, HK
    JUILLERAT, AC
    RABANY, M
    WOLLES, JC
    NUCLEAR INSTRUMENTS & METHODS IN PHYSICS RESEARCH SECTION A-ACCELERATORS SPECTROMETERS DETECTORS AND ASSOCIATED EQUIPMENT, 1994, 352 (1-2): : 467 - 470
  • [8] BASE CONTROL-SYSTEM SPECIFICATION ON COMMUNICATIONS STRUCTURE
    DAMSKER, DJ
    POWER, 1983, 127 (06) : 69 - 72
  • [9] Formal Specification and Verification of Industrial Control Logic Components
    Ljungkrantz, Oscar
    Akesson, Knut
    Fabian, Martin
    Yuan, Chengyin
    IEEE TRANSACTIONS ON AUTOMATION SCIENCE AND ENGINEERING, 2010, 7 (03) : 538 - 548
  • [10] A formal component concept for the specification of industrial control systems
    Braatz, Benjamin
    Klein, Markus
    Schröter, Gunnar
    Bengel, Matthias
    Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2004, 3147 : 69 - 88
12345