An empirical study of control logic specifications for programmable logic controllers

This paper presents an empirical study of control logic specifications used to document industrial control logic code in manufacturing applications. More than one hundred input/output related property specifications from ten different reusable function blocks were investigated. The main purpose of the study was to provide understanding of how the specifications are expressed by industrial practitioners, in order to develop new tools and methods for specifying control logic software, as well as for evaluating existing ones. In this paper, the studied specifications are used to evaluate linear temporal logic in general and the specification language ST-LTL, tailored for functions blocks, in particular. The study shows that most specifications are expressed as implications, that should always be fulfilled, between input and output conditions. Many of these implications are complex since the input and output conditions may be mixed and involve sequences, timer issues and non-boolean variables. Using ST-LTL it was possible to represent all implications of this study. The few non-implication specifications could be specified in ST-LTL as well after being altered to suit the specification language. The paper demonstrates some advantages of ST-LTL compared to standard linear temporal logic and discusses possible improvements such as support for automatic rewrite of complex specifications.     

Latticed-LTL synthesis in the presence of noisy inputs

In the classical synthesis problem, we are given a specification ψ over sets of input and output signals, and we synthesize a finite-state transducer that realizes ψ: with every sequence of input signals, the transducer associates a sequence of output signals so that the generated computation satisfies ψ. In recent years, researchers consider extensions of the classical Boolean setting to a multi-valued one. We study a multi-valued setting in which the truth values of the input and output signals are taken from a finite lattice, and so is the satisfaction value of specifications. We consider specifications in latticed linear temporal logic (LLTL). In LLTL, conjunctions and disjunctions correspond to the meet and join operators of the lattice, respectively, and the satisfaction values of formulas are taken from the lattice too. The lattice setting arises in practice, for example in specifications involving priorities or in systems with inconsistent viewpoints. We solve the LLTL synthesis problem, where the goal is to synthesize a transducer that realizes the given specification in a desired satisfaction value. For the classical synthesis problem, researchers have studied a setting with incomplete information, where the truth values of some of the input signals are hidden and the transducer should nevertheless realize ψ. For the multi-valued setting, we introduce and study a new type of incomplete information, where the truth values of some of the input signals may be noisy, and the transducer should still realize ψ in the desired satisfaction value. We study the problem of noisy LLTL synthesis, as well as the theoretical aspects of the setting, like the amount of noise a transducer may tolerate, or the effect of perturbing input signals on the satisfaction value of a specification. We prove that the noisy-synthesis problem for LLTL is 2EXPTIME-complete, as is traditional LTL synthesis.     

Specification of communicating processes: temporal logic versus refusals-based refinement

In this paper we consider the relationship between refinement-oriented specification and specifications using a temporal logic. We investigate the extent to which one can check whether a program in a process algebra, such as Communicating Sequential Processes (CSP), satisfies a temporal logic specification using a refinement-based model checker, such as FDR. We consider what atomic formulae are appropriate in a temporal logic for specifying communicating processes, in particular where one wants to talk about the availability of events. We then show that, perhaps surprisingly, the standard stable failures model is not adequate for capturing specifications in such a logic: instead the refusal traces model must be used. We formalise the logic by giving it a semantics in this model. We show that the temporal operators eventually and until, and negation, cannot, in general, be tested for via simple refinement checks. For the remaining fragment of the logic, we present a translation into simple refinement checks. Finally, we show that refusal traces equivalence is characterised by a slightly augmented version of that fragment. M. J. Butler     

Distributed synthesis for well-connected architectures

We study the synthesis problem for external linear or branching specifications and distributed, synchronous architectures with arbitrary delays on processes. External means that the specification only relates input and output variables. We introduce the subclass of uniformly well-connected (UWC) architectures for which there exists a routing allowing each output process to get the values of all inputs it is connected to, as soon as possible. We prove that the distributed synthesis problem is decidable on UWC architectures if and only if the output variables are totally ordered by their knowledge of input variables. We also show that if we extend this class by letting the routing depend on the output process, then the previous decidability result fails. Finally, we provide a natural restriction on specifications under which the whole class of UWC architectures is decidable.     

Learning Fuzzy Rules from Data

We present an algorithm, FUZZEX, for learning fuzzy rules from a corpus of data mapping input antecedents to output consequents. The input and output spaces are first divided into a grid of cells and primitive if % then rules formulated from each occupied input cell in the role of an antecedent The distribution of output cells into which data in the input cell maps, plays the role of the consequent interpreted as a fuzzy set. Those input cells associated with sufficiently similar fuzzy output sets are then combined to form a composite rule. A concise set of rules in Disjunctive Normal Form (DNF) is formed by combining adjacent input cells belonging to the same rule, thereby simplifying the logical expression of the antecedents. Optionally, more succinctness of expression may be obtained by recruiting into a rule, adjacent input cells with (little or) no data, but which happen to simplify rule expression. Preliminary testing on testbed datasets is presented. FUZZEX can be applied effectively to problems of large dimensionality.     

Specification-based Testing for Gui-based Applications

The development of GUI-based applications has raised a lot of new issues, one of them being how to automate effective testing for applications with complicated graphical user interactions. In this paper, we discuss the architectural issues and the implementation concerns of our approach to an automated specification-based testing technique for GUI-based applications. This approach is carried out by enriching existing architecture for automated specification-based testing. An essential part of our work is a visual environment to obtain test specifications. This environment pre-runs the Application Under Test (AUT) under its own control, with two prominent characteristics: First, testers can edit test specifications within the true GUI environment of the AUT. Second, the recorded input and output contain the same references as those in the AUT, so that the test cases generated from the edited specification can be used directly by test oracles during the automated testing procedure.We present our running prototype of a visual specification editor that allows users to graphically manipulate test specifications when these specifications are given in term of Finite State Machines (FSM) and the implementations of the AUT are GUI-based Java applications.     

Translating FSP into LOTOS and networks of automata

Many process calculi have been proposed since Robin Milner and Tony Hoare opened the way more than 25 years ago. Although they are based on the same kernel of operators, most of them are incompatible in practice. We aim at reducing the gap between process calculi, and especially making possible the joint use of underlying tool support. Finite state processes (FSP) is a widely used calculus equipped with Ltsa, a graphical and user-friendly tool. Language of temporal ordering specification (Lotos) is the only process calculus that has led to an international standard, and is supported by the Cadp verification toolbox. We propose a translation of FSP sequential processes into Lotos. Since FSP composite processes (i.e., parallel compositions of processes) are hard to encode directly in Lotos, they are translated into networks of automata which are another input language accepted by Cadp. Hence, it is possible to use jointly Ltsa and Cadp to validate FSP specifications. Our approach is completely automated by a translator tool.     

Generating online test oracles from temporal logic specifications

This paper is concerned with the problem of checking, by means of testing, that a software component satisfies a specification of temporal safety properties. Checking that an actual observed behavior conforms to the specification is performed by a test oracle, which can be either a human tester or a software module. We present a technique for automatically generating test oracles from specifications of temporal safety properties in a metric temporal logic. The logic can express quantitative timing properties, and can also express properties of data values by means of a quantification construct. The generated oracle works online in the sense that checking is performed simultaneously with observation. The technique has been implemented and used in case studies at Volvo Technical Development Corporation .     

VVSL: A language for structured VDM specifications

VVSL is a VDM specification language of the British School with modularisation constructs allowing sharing of hidden state variables and parameterisation constructs for structuring specifications, and with constructs for expressing temporal aspects of the concurrent execution of operations which interfere via state variables. The modularisation and parameterisation constructs have been inspired by the kernel design language COLD-K from the ESPRIT project 432: METEOR, and the constructs for expressing temporal aspects by various temporal logics based on linear and discrete time. VVSL is provided with a well-defined semantics by defining a translation to COLD-K extended with constructs which are required for translation of the VVSL constructs for expressing temporal aspects.In this paper, the syntax for the modularisation and parameterisation constructs of VVSL is outlined. Their meaning is informally described by giving an intuitive explanation and by outlining the translation to COLD-K. It is explained in some detail how sharing of hidden state variables is modelled. Examples of the use of the modularisation and parameterisation constructs are also given. These examples are based on a formal definition of the relational data model. With respect to the constructs for expressing temporal aspects, the ideas underlying the use of temporal formulae in VVSL are briefly outlined and a simple example is given.     

Development of communication protocols using algebraic and temporal specifications

The paper pursues two main goals. First, an attempt is made to specify and verify protocols in a completely rigorous manner using the formalisms of temporal logic and algebraic specification. Second––and even more important––the protocol specifications are not presented as monolithic pieces of text, but rather are developed in a stepwise process, evolving from simple genotypes into the final complex products. This is illustrated with selected fragments of the TCP/IP protocol.     

Temporal logic motion planning for dynamic robots

In this paper, we address the temporal logic motion planning problem for mobile robots that are modeled by second order dynamics. Temporal logic specifications can capture the usual control specifications such as reachability and invariance as well as more complex specifications like sequencing and obstacle avoidance. Our approach consists of three basic steps. First, we design a control law that enables the dynamic model to track a simpler kinematic model with a globally bounded error. Second, we built a robust temporal logic specification that takes into account the tracking errors of the first step. Finally, we solve the new robust temporal logic path planning problem for the kinematic model using automata theory and simple local vector fields. The resulting continuous time trajectory is provably guaranteed to satisfy the initial user specification.     

Graphical scenarios for specifying temporal properties: an automated approach

Temporal logics are commonly used for reasoning about concurrent systems. Model checkers and other finite-state verification techniques allow for automated checking of system model compliance to given temporal properties. These properties are typically specified as linear-time formulae in temporal logics. Unfortunately, the level of inherent sophistication required by these formalisms too often represents an impediment to move these techniques from “research theory” to “industry practice”. The objective of this work is to facilitate the nontrivial and error prone task of specifying, correctly and without expertise in temporal logic, temporal properties. In order to understand the basis of a simple but expressive formalism for specifying temporal properties we critically analyze commonly used in practice visual notations. Then we present a scenario-based visual language called Property Sequence Chart (PSC) that, in our opinion, fixes the highlighted lacks of these notations by extending a subset of UML 2.0 Interaction Sequence Diagrams. We also provide PSC with both denotational and operational semantics. The operational semantics is obtained via translation into Büchi automata and the translation algorithm is implemented as a plugin of our Charmy tool. Expressiveness of PSC has been validated with respect to well known property specification patterns. Preliminary results appeared in (Autili et al. 2006a).     

An input–output simulation approach to controlling multi-affine systems for linear temporal logic specifications

This article presents an input–output simulation approach to controlling multi-affine systems for linear temporal logic (LTL) specifications, which consists of the following steps. First, the state space is partitioned into rectangles, each of which satisfies atomic LTL propositions. Then, we study the control of multi-affine systems on rectangles, including the control based on the exit sub-region to drive all trajectories starting from a rectangle to exit through a facet and the control to stabilise the multi-affine system towards a desired point. With the proposed controllers, a finitely abstracted transition system is constructed which is shown to be input–output simulated by the rectangular transition system of the multi-affine system. Since the input–output simulation preserves LTL properties, the controller synthesis of the multi-affine system for LTL specifications is achieved by designing a nonblocking supervisor for the abstracted transition system and by implementing the resulting supervisor to the original multi-affine system.     

Formal Verification of Activity-Based Specification of Protocols

In this paper, we describe a method to formally verify activity-based specifications such as EBSDL. Starting from EBSDL-like specifications that specify engineering activities in terms of input and output behaviors, we derive programs in an asynchronous language CSP-R. CSP-R programs are then verified by the Maxpar method by composing them with the programs abstracting their environment. EBSDL-like specification and its verification using our method, is illustrated through the example of a fragment of LAPD protocol. The derivation of programs from the specification of activities of the underlying protocols through EBSDL-like specifications provides an important useful tool for formal verification of real-time protocols. We shall also discuss a translation of EBSDL-like specifications to synchronous languages such as Esterel. In the method proposed, it is possible for the user to choose asynchronous or synchronous formalisms depending upon the requirements of verification vis-a-vis logical specification.     

时态粗糙神经网

论文提出了一种基于粗糙集和时态概念的新神经网模型—时态粗糙神经网。在神经网的输入中加入时间的因素,即神经网络的输入是时间的函数,从而把传统的神经元改造成了时态神经元;时态粗糙神经网中的神经元是时态粗糙神经元,它包括一对时态神经元,即将数据中的上边界和下边界加入时间因素以后,作为神经网络的输入和输出。当网络的输入和输出不是单值数据而是一个随时间变化的数据的集合时,经典的神经网络建立的预测模型的输出就会产生较大的误差,而基于时态粗糙理论的神经网络则可以很好地解决这个问题,更能真实刻画实际问题。从而为解决这类问题提供了一个较好的理论模型。     

Test generation for radiotherapy accelerators

System specification with Lotos (Language Of Temporal Ordering Specification) is briefly introduced. To make test generation practicable, specifications are annotated with event constraints using PCL (Parameter Constraint Language) as a means of stating test purposes. Automated test generation can then use the principle of input-output conformance to check whether an implementation agrees with its specification. Test suites are generated by a transition tour that either visits every transition at least once (for infinite behaviour) or follows every path (for finite behaviour). The approach is applied to a case study in which tests are generated for radiotherapy accelerators used in cancer treatment. A typical specification and set of test purposes yields 256 test cases that can be executed manually or automatically. The goal is to determine situations in which an accelerator does not behave in conformity with its specification.     

Semantics,calculi, and analysis for object-oriented specifications

We present a formal semantics for an object-oriented specification language. The formal semantics is presented as a conservative shallow embedding in Isabelle/hol and the language is oriented towards ocl formulae in the context of uml class diagrams. On this basis, we formally derive several equational and tableaux calculi, which form the basis of an integrated proof environment including automatic proof support and support for the analysis of this type of specifications. We show applications of our proof environment to data refinement based on an adapted standard refinement notion. Thus, we provide an integrated formal method for refinement-based object-oriented development.