Today＇s automation industry is driven by the need for an increased productivity, higher flexibility, and higher individuality, and characterized by tailor-made and more complex control solutions. In the processing in...Today＇s automation industry is driven by the need for an increased productivity, higher flexibility, and higher individuality, and characterized by tailor-made and more complex control solutions. In the processing industry, logic controller design is often a manual, experience-based, and thus an error-prone procedure. Typically, the specifications are given by a set of informal requirements and a technical flowchart and both are used to be directly translated into the control code. This paper proposes a method in which the control program is constructed as a sequential function chart （SFC） by transforming the requirements via clearly defined intermediate formats. For the purpose of analysis, the resulting SFC can be translated algorithmically into timed automata. A rigorous verification can be used to determine whether all specifications are satisfied if a formal model of the plant is available which is then composed with the automata model of the logic controller （LC）.展开更多
基金the European Union through the Network of Excellence Hybrid Control (HYCON) under contract IST-511368.
文摘Today＇s automation industry is driven by the need for an increased productivity, higher flexibility, and higher individuality, and characterized by tailor-made and more complex control solutions. In the processing industry, logic controller design is often a manual, experience-based, and thus an error-prone procedure. Typically, the specifications are given by a set of informal requirements and a technical flowchart and both are used to be directly translated into the control code. This paper proposes a method in which the control program is constructed as a sequential function chart （SFC） by transforming the requirements via clearly defined intermediate formats. For the purpose of analysis, the resulting SFC can be translated algorithmically into timed automata. A rigorous verification can be used to determine whether all specifications are satisfied if a formal model of the plant is available which is then composed with the automata model of the logic controller （LC）.
