A process algebra based verification of a production system

Author

Kleijn, J.J.T. ; Rooda, J.E. ; Reniers, M.A.

Author_Institution

Syst. Eng. Group, Eindhoven Univ. of Technol., Netherlands

fYear

1998

fDate

9-11 Dec 1998

Firstpage

90

Lastpage

99

Abstract

Studying industrial systems by simulation enables the designer to study the dynamic behaviour and to determine some characteristics of the system. Unfortunately simulation also has some disadvantages. These can be overcome by using formal methods. Formal methods allow a thorough analysis of the possible behaviours of a system, parameterised system analysis and a modular approach to the analysis of systems. We present a case study in which a model of an industrial system is studied in a formal way. For this purpose, the model is first specified and simulated using the CSP-based executable specification language χ. The model is translated into a model in the process algebra ACP^T. This enables us to give a correctness proof of the parameterised model and to study the model in isolation

Keywords

communicating sequential processes; digital simulation; formal specification; process algebra; production engineering computing; program verification; specification languages; systems analysis; CSP; case study; correctness proof; dynamic behaviour; executable specification language; formal methods; industrial systems; modular approach; parameterised system analysis; process algebra; production system verification; simulation; Algebra; Analytical models; Buildings; Machinery production industries; Modeling; Production facilities; Production systems; Software engineering; Systems engineering and theory; Throughput;

fLanguage

English

Publisher

ieee

Conference_Titel

Formal Engineering Methods, 1998. Proceedings. Second International Conference on

Conference_Location

Brisbane, Qld.

Print_ISBN

0-8186-9198-0

Type

conf

DOI

10.1109/ICFEM.1998.730573

Filename

730573