DocumentCode :
130831
Title :
A hierarchy framework on compositional verification for PLC software
Author :
Litian Xiao ; Mengyuan Li ; Ming Gu ; Jiaguang Sun
Author_Institution :
Beijing Special Eng. Design & Res. Inst., Beijing, China
fYear :
2014
fDate :
27-29 June 2014
Firstpage :
204
Lastpage :
207
Abstract :
The correctness verification of embedded control software has become an important research topic in embedded system field. The paper analyses the present situation on correctness verification of control software as well as the limitations of existing technologies. In order to the high reliability and high security requirements of control software, the paper proposes a hierarchical framework and architecture of control software (PLC program) verification. The framework combines the technologies of testing, model checking and theorem proving. The paper introduces the construction, flow and key elements of the architecture.
Keywords :
control engineering computing; embedded systems; program verification; programmable controllers; theorem proving; PLC program verification; PLC software; compositional verification; control software verification; correctness verification; embedded control software; embedded system field; hierarchical framework; model checking; security requirements; theorem proving; Computer architecture; Computer bugs; Mathematical model; Model checking; Semantics; Software; PLCsoftware; compositional verification; hierarchy framework; verification architecture;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Software Engineering and Service Science (ICSESS), 2014 5th IEEE International Conference on
Conference_Location :
Beijing
ISSN :
2327-0586
Print_ISBN :
978-1-4799-3278-8
Type :
conf
DOI :
10.1109/ICSESS.2014.6933545
Filename :
6933545
Link To Document :
بازگشت