Analysis of conditional specifications for programmable logic controllers

本计画研究可程式逻辑控制器（PLC）的条件软体规格，以及一种有效搜寻其中可能存在的错误的方法。当系统层面的要求被分解并细化为功能块层面的行为要求时，就会出现条件规范，区分组件/功能块行为的“保证”和其环境行为的“假设”。实现（和类似实现的模型）通过检查它们的行为来验证先前创建的需求。相比之下，验证的条件规范之一，分析是否分解成一组组件的正式系统的要求确实意味着原来的，上级requirement.We打算设计一个算法，可扩展的方法来检测不一致的软件规格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.