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