|
|
|
|
|
|
|
|
1. |
Record Nr. |
UNINA9910820072403321 |
|
|
Autore |
Missal Dirk |
|
|
Titolo |
Formal synthesis of safety controller code for distributed controllers / / by Dirk Missal |
|
|
|
|
|
|
|
Pubbl/distr/stampa |
|
|
Berlin : , : Logos Verlag, , [2012] |
|
©2012 |
|
|
|
|
|
|
|
|
|
ISBN |
|
|
|
|
|
|
Descrizione fisica |
|
1 online resource (156 pages) |
|
|
|
|
|
|
Collana |
|
Hallenser Schriften zur Automatisierungstechnik |
|
|
|
|
|
|
Disciplina |
|
|
|
|
|
|
Soggetti |
|
Automatic control - Standards |
|
|
|
|
|
|
Lingua di pubblicazione |
|
|
|
|
|
|
Formato |
Materiale a stampa |
|
|
|
|
|
Livello bibliografico |
Monografia |
|
|
|
|
|
Note generali |
|
PublicationDate: 20120510 |
|
|
|
|
|
|
Sommario/riassunto |
|
Long description: Modern control systems in manufacturing are characterized by rising complexity in size and functionality. They are highly decentralized and constitute a network of physically and functionally distributed controllers collaborating to perform the control tasks. That goes along with a further growing demand on safety and reliability. A distributed control architecture supporting functional decomposition of large systems as well as accommodating flexibility of modular systems is defined. This work describes the formal synthesis of distributed control functions for the sub area of safety requirements. The formal synthesis is applied to avoid the potentially faulty influence of human work through the whole process from the formal specification to the executable control function. Starting points are a formal model of the uncontrolled plant behavior and a formal specification of forbidden behavior. The formulation of the specification and the modeling is exemplified on a manufacturing system in lab-scale. The introduced synthesis methods produce controller models describing the correct control actions to achieve the given specification. The methods use symbolic backward search from a forbidden state to determine the last admissible state before entering an uncontrollable trajectory to a forbidden state. Hence, the determination of the reachable state space is avoided to reduce the |
|
|
|
|