A unified linear-time temporal logic solution to the steam-boiler control specification problem (Q5926751)
From MaRDI portal
scientific article; zbMATH DE number 1572991
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | A unified linear-time temporal logic solution to the steam-boiler control specification problem |
scientific article; zbMATH DE number 1572991 |
Statements
A unified linear-time temporal logic solution to the steam-boiler control specification problem (English)
0 references
15 July 2001
0 references
The solution to the steam boiler control specification problem on the basis of the TLL XYZ/E formal language previously developed by the authors is proposed. The physical model for the whole system is presented in detail and safety and liveness of the program are specified. Five steps of refinement are described. In the first step the concept of `Working Status' is introduced. In the second step a sampling process is specified and unobservable variables are replaced. In the third step the functioning of the system in the presence of physical units' faults is specified. In the fourth step the manipulation of valves and pumps to control water level are described. In the fifth step a clock process to synchronize all actions is specified.
0 references
temporal logic language
0 references
steam boiler control
0 references
hybrid real-time system
0 references
XYZ/E
0 references
program specification
0 references
stepwise refinement
0 references
verification
0 references
control of water level
0 references
safety
0 references
liveness
0 references
clock process
0 references
faults
0 references
