In this paper a methodology to develop safety-critical control systems is proposed. These systems continuously interact with the physical environment, and those admitting at least one failure causing a catastrophe are classified as safety-critical. Our methodology takes into account both the control system (controller) and the physical environment (plant). After the requirements analysis, the system is developed following data flow model, i.e., described as a static data flow network of nodes executing concurrently and communicating asynchronously. The plant is used as the test case for the validation of the controller and their composition is analysed to show whether hazards are reached. To this purpose we apply a transformation from data flow networks to LOTOS specifications. The transformation preserves the semantics of the original network and data flow network properties can be derived and proved on the LOTOS specification using available support tools. A train set example for the contact-free moving of trains on a circular track divided into sections is shown as an application of the methodology.
Data-flow Control Systems: An example of Safety Validation
BERNARDESCHI, CINZIA;SIMONCINI, LUCA;
1993-01-01
Abstract
In this paper a methodology to develop safety-critical control systems is proposed. These systems continuously interact with the physical environment, and those admitting at least one failure causing a catastrophe are classified as safety-critical. Our methodology takes into account both the control system (controller) and the physical environment (plant). After the requirements analysis, the system is developed following data flow model, i.e., described as a static data flow network of nodes executing concurrently and communicating asynchronously. The plant is used as the test case for the validation of the controller and their composition is analysed to show whether hazards are reached. To this purpose we apply a transformation from data flow networks to LOTOS specifications. The transformation preserves the semantics of the original network and data flow network properties can be derived and proved on the LOTOS specification using available support tools. A train set example for the contact-free moving of trains on a circular track divided into sections is shown as an application of the methodology.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
