Analysis of conditional specifications for programmable logic controllers

点击翻译按钮获取中文摘要

This project investigates conditional software specifications for programmable logic controllers (PLC) and an efficient search method for faults that may be present in them. Conditional specifications arise when requirements on system level are decomposed and detailed into behavioural requirements on function block level, discriminating between "guarantees" for the behaviour of components/function blocks and "assumptions" about the behaviour of their environment. Implementations (and implementation-like models) are verified by checking their behaviour against previously created requirements. In contrast, for the verification of conditional specifications one has to analyse whether the decomposition of a formal system requirement into a set of component requirements does indeed imply the original, superordinated requirement.We intend to devise an algorithmic, scalable method to detect inconsistences in software specifications for PLCs that are caused by wrong decomposition, at an early stage. The (exhaustive) verification with timed formalisms, due to the additional states introduced by clock variables, is notoriously difficult. Since the primary aim is to find specification faults as quickly as possible without searching the entire state space we employ incomplete methods.Conditional specifications consist of one condition on the expected behaviour of the component's environment ("assumption") and one condition on the behaviour of the component itself ("guarantee"). The latter must only be fulfilled if the environment behaviour conforms to the corresponding assumption. Partial specifications are modelled as observer automata, and falsification is performed by model checking.Abstraction is a well-tried technique in the verification of implementations. In general, however, it cannot be applied on the level of requirements, and new approaches to improving efficiency and scalability are necessary. For this purpose we use directed/guided model checking, exploiting the relationship between a superordinated conditional requirement and its decomposition to define novel distance measures that provide us with heuristics to speed up the search for target states (respectively, specification faults). That this becomes possible without generating an explicit product of observer automata is of particular importance.