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 条

[41] NEW DEVELOPMENT IN THE FIELD OF INDUSTRIAL MAINTENANCE WITH SAFEMATIC CONDITION CONTROL-SYSTEM SAFE 2000
SIIMES, A
ILVONEN, P
WOCHENBLATT FUR PAPIERFABRIKATION, 1985, 113 (10): : 362 - 364
[42] DEVELOPMENT OF A COMPUTERIZED PHARMACY CONTROL-SYSTEM
MILLER, RA
DELEON, RF
AMERICAN JOURNAL OF HOSPITAL PHARMACY, 1972, 29 (11): : 963 - &
[43] A DEVELOPMENT ENVIRONMENT FOR THE SSC CONTROL-SYSTEM
MURRAY, D
MARTINSEN, G
WANG, J
NUCLEAR INSTRUMENTS & METHODS IN PHYSICS RESEARCH SECTION A-ACCELERATORS SPECTROMETERS DETECTORS AND ASSOCIATED EQUIPMENT, 1994, 352 (1-2): : 390 - 392
[44] DEVELOPMENT OF FUZZY EXCITATION CONTROL-SYSTEM
KITAUCHI, Y
TANIGUCHI, H
ELECTRICAL ENGINEERING IN JAPAN, 1994, 114 (03) : 47 - 58
[45] ELECTRONIC PROPELLER SPEED CONTROL-SYSTEM FOR TROLLING OPERATIONS
不详
NAVAL ARCHITECT, 1992, : E220 - E220
[46] EMULATOR HELPS SPEED MOTOR CONTROL-SYSTEM DESIGN
OHEL, I
CONTROL ENGINEERING, 1982, 29 (06) : 160 - &
[47] HPMS 5-SPEED SHOT CONTROL-SYSTEM
不详
DIE CASTING ENGINEER, 1982, 26 (05): : 30 - 30
[48] APPLICATIONS OF DISTRIBUTED MICROPROCESSORS IN THE CESR CONTROL-SYSTEM
REEVES, DB
DAIN, FW
HELMKE, R
IEEE TRANSACTIONS ON NUCLEAR SCIENCE, 1979, 26 (03) : 3445 - 3447
[49] SYNTHESIS OF A CONTROL-SYSTEM THAT IS OPTIMAL WITH RESPECT TO RESPONSE SPEED
KOZLOV, VI
ENGINEERING CYBERNETICS, 1976, 14 (03): : 145 - 155
[50] DIGITAL SPEED CONTROL-SYSTEM FOR A CONTINUOUS SECTION MILL
STAKHNO, VI
EGOROV, AP
TKACHEV, VS
KUVAEV, VN
METALLURGIST, 1983, 27 (1-2) : 66 - 68

← 1 2 3 4 5 →