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
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;
Conference_Titel :
Software Engineering and Service Science (ICSESS), 2014 5th IEEE International Conference on
Conference_Location :
Beijing
Print_ISBN :
978-1-4799-3278-8
DOI :
10.1109/ICSESS.2014.6933545
