Analysis of conditional specifications for programmable logic controllers

本项目研究可编程逻辑控制器(PLC)的条件性软件规范和一种有效的故障搜索方法。当系统级的要求被分解并细化为功能块级的行为要求时，就会出现条件规范，区分对组件/功能块行为的“保证”和对其环境行为的“假设”。实现(和类似实现的模型)通过对照先前创建的需求检查它们的行为来验证。相比之下，对于条件规范的验证，必须分析将正式系统需求分解为一组组件需求是否确实意味着原始的、高级的需求。我们打算设计一种算法、可伸缩的方法来在早期阶段检测由于错误分解而导致的PLC软件规范中的不一致。由于时钟变量引入了额外的状态，用时间形式进行(详尽的)验证是出了名的困难。由于主要目标是在不搜索整个状态空间的情况下尽可能快地找到规范错误，因此我们使用不完全的方法。条件规范由一个关于组件环境的预期行为的条件(“假设”)和一个关于组件本身的行为的条件(“保证”)组成。后者只有在环境行为符合相应假设的情况下才能实现。将部分规格说明建模为观察者自动机，并通过模型检查进行证伪，抽象是一种在实现验证中行之有效的技术。然而，一般而言，它不能应用于需求级别，需要改进效率和可伸缩性的新方法。为此，我们使用定向/引导式模型检测，利用上级条件需求及其分解之间的关系来定义新的距离度量，这些度量为我们提供启发式方法来加快目标状态(分别是规范错误)的搜索。在不生成观察者自动机的显式乘积的情况下，这变得可能是特别重要的。

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.