Name
Title | ||
|---|---|---|
Rigorous development of an embedded fault-tolerant system based on coordinated atomic actions |
Abstract | ||
|---|---|---|
Describes our experience using coordinated atomic (CA) actions as a system structuring tool to design and validate a sophisticated and embedded control system for a complex industrial application that has high reliability and safety requirements. Our study is based on an extended production cell model, the specification and simulator for which were defined and developed by FZI (Forschungszentrum Informatik, Germany). This "fault-tolerant production cell" represents a manufacturing process involving redundant mechanical devices (provided in order to enable continued production in the presence of machine faults). The challenge posed by the model specification is to design a control system that maintains specified safety and liveness properties even in the presence of a large number and variety of device and sensor failures. Based on an analysis of such failures, we provide details of: (1) a design for a control program that uses CA actions to deal with both safety-related and fault tolerance concerns and (2) the formal verification of this design based on the use of model checking. We found that CA action structuring facilitated both the design and verification tasks by enabling the various safety problems (involving possible clashes of moving machinery) to be treated independently. Even complex situations involving the concurrent occurrence of any pairs of the many possible mechanical and sensor failures can be handled simply yet appropriately. The formal verification activity was performed in parallel with the design activity, and the interaction between them resulted in a combined exercise in "design for validation"; formal verification was very valuable in identifying some very subtle residual bugs in early versions of our design which would have been difficult to detect otherwise |
Year | DOI | Venue |
|---|---|---|
2002 | 10.1109/12.980006 | IEEE Trans. Computers |
Keywords | Field | DocType |
reliability requirements,sensor failure,moving machinery clashes,control system,rigorous development,fault-tolerant production cell,device failures,design activity,model checking,formal verification activity,machine faults,ca action,coordinated atomic actions,redundant mechanical devices,model specification,fault tolerant computing,complex industrial application,embedded fault-tolerant system development,subtle residual bugs,control program design,safety requirements,multiprocessing systems,flexible manufacturing systems,liveness properties,system structuring tool,concurrency,exception handling,simulator,redundancy,continued production,fault-tolerant system,design for validation,object orientation,manufacturing process,verification task,sensor failures,control program,safety requirement,embedded systems,safety,embedded control system,formal verification,fault tolerant,fault tolerance,control systems,manufacturing industries,reliability,production,fault tolerant system | Functional verification,Model checking,Concurrency,Computer science,Exception handling,Parallel computing,Real-time computing,Fault tolerance,Control system,Liveness,Formal verification | Journal |
Volume | Issue | ISSN |
51 | 2 | 0018-9340 |
Citations | PageRank | References |
22 | 1.20 | 16 |
Authors | ||
7 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Jie Xu | 1 | 711 | 57.85 |
| Brian Randell | 2 | 3123 | 551.69 |
| Alexander Romanovsky | 3 | 824 | 80.19 |
| Robert J. Stroud | 4 | 240 | 24.67 |
| Avelino F. Zorzo | 5 | 188 | 24.27 |
| E. Canver | 6 | 47 | 3.43 |
| f von henke | 7 | 36 | 2.41 |