Modelling and verification of program logic controllers using timed automata

作     者：Wang, R. Song, X. Gu, M. 

作者机构：Tsinghua Univ Sch Software Beijing 100084 Peoples R China Portland State Univ Dept ECE Portland OR 97207 USA 

出 版 物：《IET SOFTWARE》 (IET Software)

年 卷 期：2007年第1卷第4期

页      面：127-131页

核心收录：

学科分类：0808[工学-电气工程] 08[工学] 0835[工学-软件工程] 

主　　题：formal verification computational tree logic complex embedded system designs automata theory Automata theory systems analysis program logic controllers timed automata programmable controllers Programmable controllers Formal methods embedded systems 

摘      要：Validation is an important task in complex embedded system designs. A method of modelling and analysing embedded systems with programmable logic controllers is presented. Controllers and physical plants are modelled using timed automata. The system requirements are specified and formalised as computational tree logic properties. It is demonstrated that the designed model satisfies the required properties by resorting to a symbolic model checker, Uppaal, for real-time systems. A realistic example, the steeve controller of a theatre, illustrates the strategies. The safety and time constraint requirements are validated by Uppaal. The experimental results demonstrate the effectiveness of the approach presented here.