Compositional verification of industrial control systems : methods and case studies
Ben Lukoschus · Multimedialen Archiv und Publikationsserver der Christian-Albrechts-Universität zu Kiel (Christian-Albrechts-Universität zu Kiel) · 2006
Production This software controls the production of "blue" and "green" in the reactors R21-R23 as described above.Resource management It has to be ensured that the access to hardware resources (e.g., reactor R21) is exclusive, i.e., two control programs must not use the same resource simultaneously. Emergency shutdown, maintenance, etc.There are several programs used for exceptional plant operations, e.g., rinsing all pipes and tanks with water.Complete descriptions of the multi-product batch plant and its control software can be found in [Bau00, BKSL00]. Chapter 4 Modular VerificationAs we have argued in Section 1.3, the main challenge in formal verification is the state explosion problem emerging from the parallel composition of many system components.This chapter introduces a modular verification approach which uses decomposition and a minimization technique for the composition of system parts to mitigate complexity issues.This approach is demonstrated by the verification of safety properties of the first batch plant introduced in Chapter 3. SPEC AG (PrgB2.state=q_3-> Valve6.StatusV6=closed & Valve7.StatusV7=closed & Valve9.StatusV9=closed) Verification result: true • Prg B 3 , Valve 8 , Valve 9 , Valve 10 , Valve 11 SPEC AG (PrgB3.state=q_6-> Valve8.StatusV8=closed & Valve9.StatusV9=closed & Valve10.StatusV10=closed & Valve11.StatusV11=closed) Verification result: true • Prg B 3K , Valve 8 , Valve 9 , Valve 10 , Valve 11 SPEC AG (PrgB3K.state=q_9-> Valve8.StatusV8=closed & Valve9.StatusV9=closed & Valve10.StatusV10=closed & Valve11.StatusV11=closed