The embedded software of an electricity meter: An experience in using formal methods in an industrial project

被引：2

作者：

Arnold, A ^{[1
]}

Begay, D ^{[1
]}

Radoux, JP ^{[1
]}

机构：

[1] SERLI INFORMAT,F-86960 FUTUROSCOPE,FRANCE

来源：

SCIENCE OF COMPUTER PROGRAMMING | 1997年 / 28卷 / 2-3期

关键词：

transition systems; model-checking; embedded systems; industrial use of formal methods; scheduling; critical software;

D O I：

10.1016/S0167-6423(96)00018-4

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

This article presents how various formal methods have been involved, first on their own, then coupled, in the different steps of the industrial development of an embedded software for an electricity meter, Synchronized transition systems have been used to conceive and implement some rendezvous mechanisms for the distributed kernel, and the physical link protocol supporting communication between processors. The rate monotonic analysis model has been completed to suit some features of the product; however it appeared too rough to reach a positive issue. So we coupled both (synchronized transition systems and rate monotonic analysis) to achieve a fine analysis of the temporal properties of the system under development. This can be considered a first step towards formal methods engineering. (C) 1997 Elsevier Science B.V.

引用

页码：93 / 110

页数：18

共 13 条

[1]

ALABAU M, 1996, RTS 96

[2]

Arnold A., 1994, CONSTRUCTION ANAL TR

[3]

ARNOLD A, 1996, FME 96

[4]

Arnold A., 1994, FINITE TRANSITION SY

[5]

BEGAY D, 1994, THEORIES EXPERIENCES, V2, P363

[6]

CRUBILLE P, 1989, THESIS U BORDEAUX 1

[7]

DICKY A, 1985, THESIS U BORDEAUX 1

[8]

GRIFFAULT A, 1995, MODELS PROOFS BORDEA

[9] SYMBOLIC MODEL CHECKING FOR REAL-TIME SYSTEMS [J].

HENZINGER, TA ;

NICOLLIN, X ;

SIFAKIS, J ;

YOVINE, S .

INFORMATION AND COMPUTATION, 1994, 111 (02) :193-244

[10] SCHEDULING ALGORITHMS FOR MULTIPROGRAMMING IN A HARD-REAL-TIME ENVIRONMENT [J].

LIU, CL ;

LAYLAND, JW .

JOURNAL OF THE ACM, 1973, 20 (01) :46-61

← 1 2 →