Formal testing of timed graph transformation systems using metric temporal graph logic

Embedded real-time systems generate state sequences where time elapses between state changes. Ensuring that such systems adhere to a provided specification of admissible or desired behavior is essential. Formal model-based testing is often a suitable cost-effective approach. We introduce an extended version of the formalism of symbolic graphs, which encompasses types as well as attributes, for representing states of dynamic systems. Relying on this extension of symbolic graphs, we present a novel formalism of timed graph transformation systems (TGTSs) that supports the model-based development of dynamic real-time systems at an abstract level where possible state changes and delays are specified by graph transformation rules. We then introduce an extended form of the metric temporal graph logic (MTGL) with increased expressiveness to improve the applicability of MTGL for the specification of timed graph sequences generated by a TGTS. Based on the metric temporal operators of MTGL and its built-in graph binding mechanics, we express properties on the structure and attributes of graphs as well as on the occurrence of graphs over time that are related by their inner structure. We provide formal support for checking whether a single generated timed graph sequence adheres to a provided MTGL specification. Relying on this logical foundation, we develop a testing framework for TGTSs that are specified using MTGL. Lastly, we apply this testing framework to a running example by using our prototypical implementation in the tool AutoGraph.

     

ProMiner:系统性质驱动的双向一致性检验框架

在模型驱动软件开发过程中,基于模型的测试方法往往用于检验软件代码针对软件模型的一致性以确保软件质量.然而,随着当今软件系统规模的不断扩大,相应的软件开发过程也变得越来越灵活,代码有时会先于模型被修改,以更忠实地体现系统功能和实现机制.传统的基于模型的测试方法只能检测代码之于模型的一致性而不能反作用于模型层面,模型的修改者只能人为地评估修改的正确性,大大降低了效率并增加了系统的潜在隐患.为此,对传统基于模型的测试方法的一致性检验进行了扩展,实现了一致性检验框架ProMiner,通过抽取表达模型与代码的不一致的系统性质来自动定位模型中与实际运行系统不匹配的部分,并将其表示为可直接用于模型检测的线性时序逻辑(LTL)表达式,以支持软件模型和代码间双向的一致性检验.实验结果表明,ProMiner可有效查找软件模型和代码间的不一致并生成可直接检测模型的系统性质,从而实现了自动化的模型与代码间的双向一致性检测,不仅提高了一致性检测的有效性,而且大大减少了人力开销.     

Knowledge engineering for model-based diagnosis: An experience-based development approach

Falut diagnosis has proved to be one of the most rewarding application areas for the introduction of knowledge-based systems. Initially all diagnostic systems were based upon shallow knowledge, and many proved to be highly effective within a narrow task-specific domain. The current thrust of research, however, is also focusing on the use of model-based reasoning, which provides deeper knowledge of the structure and function of the device under diagnosis. Whilst much has been written with regard to development methods for shallow knowledge-based systems, relatively little has been published specifically relating to model-based approaches. This paper describes the approach adopted for the development of a model-based application for the diagnosis of hydraulic systems, paying particular attention to the lessons learned.     

Observer‐based fault diagnosis and self‐restore control for systems with measurement delays

The problems of fault diagnosis and fault‐tolerant control are considered for systems with measurement delays. In contrast to the present fault diagnosis and fault‐tolerant control approaches, which consider only the input delay and/or state delay, the main contribution of this paper consists of proposing a new observer‐based reduced‐order fault diagnoser construction approach and a design approach to dynamic self‐restore fault‐tolerant control law for systems with measurement delays. First, the time‐delay system is transformed into a delay‐free system in form by a special functional‐based delay‐free transformation approach for measurement delays. Then, the fault diagnosis is realized online via the proposed reduced‐order fault diagnoser. Using the results of fault diagnosis, two dynamic self‐restore control laws are designed to make the system isolated from faults. A numerical example demonstrates the feasibility and validity of the proposed scheme. © 2012 John Wiley and Sons Asia Pte Ltd and Chinese Automatic Control Society     

A probabilistic theory of model-based diagnosis

Diagnosis of a malfunctioning physical system is the task of identifying those component parts whose failures are responsible for discrepancies between observed and correct system behavior. The result of diagnosis is to enable system repair by replacement of failed parts.The model-based approach to diagnosis has emerged as a strong alternative to both symptom-based and fault-model-based approaches. Hypothesis generation and hypothesis discrimination (action selection) are two major subtasks of model-based diagnosis. Hypothesis generation has been partially resolved by symbolic reasoning using a subjective notion of parsimony such as non-redundancy. Action selection has only been studied for special cases, e.g. probes with equal cost. Little formal work has been done on repair selection and verification.This paper presents a probabilistic theory for model-based diagnosis. An objective measure is used to rank hypotheses, viz., posterior probabilities, instead of subjective parsimony. Fault hypotheses are generated in decreasing probability order. The theory provides an estimate of the expected diagnosis cost of an action. The result of the minimal cost action is used to adjust hypothesis probabilities and to select further actions.The major contributions of this paper are the incorporation of probabilistic reasoning into model-based diagnosis and the integration of repair as part of diagnosis. The integration of diagnosis and repair makes it possible to troubleshoot failures effectively in complex systems.     

嵌入式实时系统的软件需求检测

以需求描述模型HRFSM(hierarchical finite state machines based on rules)为基础,提出了一个嵌入式实时系统软件的动态执行模型(dynamic execution model,简称DEM)和基于该模型的检测方法.由于DEM能将控制流、数据流和时间有效地集成为一体,故提出的检测方法能检测嵌入式实时系统的软件需求的一致性和完全性.该检测方法由3种侧重点不同的检测形式组成,并能在检测过程中提供一些重要的检测信息.分析员可以利用基于该检测方法的工具灵活地对嵌入式实时系统的软件需求进行检测,以提高分析和检测软件需求的效率.     

Logic-based modeling of information transfer in cyber–physical multi-agent systems

In modeling multi-agent systems, the structure of their communication is typically one of the most important aspects, especially for systems that strive toward self-organization or collaborative adaptation. Traditionally, such structures have often been described using logic-based approaches as they provide a formal foundation for many verification methods. However, these formalisms are typically not well suited to reflect the stochastic nature of communication in the cyber–physical setting. In particular, their level of abstraction is either too high to provide sufficient accuracy or too low to be practicable in more complex models. Therefore, we propose an extension of the logic-based modeling language SALMA, which we have introduced recently, that provides adequate high-level constructs for communication and data propagation, explicitly taking into account stochastic delays and errors. In combination with SALMA’s tool support for simulation and statistical model checking, this creates a pragmatic approach for verification and validation of cyber–physical multi-agent systems.     

Decomposition algorithm of dynamic programming for large-scale time-delay systems

This paper addresses the development of a dynamic programming decomposition-coordination algorithm for the optimal control of discrete-time large-scale systems with multiple time delays. The systems under study can be converted into the corresponding augmented systems satisfying the Markov processes denning the augmented state vectors. The resulting dynamic programming can then be further decomposed into a series of subproblems which might be solved in parallel by combining the dynamic programming techniques with approaches to matrix partition. The entire system's solution is finally given by the iterative computation between the subproblems being the local control level and the coordinator. The major advantages of the proposed algorithm over others are to avoid two-point boundary-value problems of the systems with multiple time delays and to significantly reduce the computer memory and time required for such large-scale systems optimal control problems.     

Behavioral modeling and formal verification of a resource discovery approach in Grid computing

Grid computing is the federation of resources from multiple locations to facilitate resource sharing and problem solving over the Internet. The challenge of finding services or resources in Grid environments has recently been the subject of many papers and researches. These researches and papers evaluate their approaches only by simulation and experiments. Therefore, it is possible that some part of the state space of the problem is not analyzed and checked well. To overcome this defect, model checking as an automatic technique for the verification of the systems is a suitable solution. In this paper, an adopted type of resource discovery approach to address multi-attribute and range queries has been presented. Unlike the papers in this scope, this paper decouple resource discovery behavior model to data gathering, discovery and control behavior. Also it facilitates the mapping process between three behaviors by means of the formal verification approach based on Binary Decision Diagram (BDD). The formal approach extracts the expected properties of resource discovery approach from control behavior in the form of CTL and LTL temporal logic formulas, and verifies the properties in data gathering and discovery behaviors comprehensively. Moreover, analyzing and evaluating the logical problems such as soundness, completeness, and consistency of the considered resource discovery approach is provided. To implement the behavior models of resource discovery approach the ArgoUML tool and the NuSMV model checker are employed. The results show that the adopted resource discovery approach can discovers multi-attribute and range queries very fast and detects logical problems such as soundness, completeness, and consistency.     

Dual constrained single machine sequencing to minimize total weighted completion time

We study a single-machine sequencing problem with both release dates and deadlines to minimize the total weighted completion time. We propose a branch-and-bound algorithm for this problem. The algorithm exploits an effective lower bound and a dynamic programming dominance technique. As a byproduct of the lower bound, we have developed a new algorithm for the generalized isotonic regression problem; the algorithm can also be used as an O(nlogn)-time timetabling routine in earliness-tardiness scheduling. Extensive computational experiments indicate that the proposed branch-and-bound algorithm competes favorably with a dynamic programming procedure. Note to Practitioners-Real-life production systems usually involve multiple machines and resources. The configurations of such systems may be complex and subject to change over time. Therefore, model-based solution approaches, which aim to solve scheduling problems for specific configurations, will inevitably run into difficulties. By contrast, decomposition methods are much more expressive and extensible. The single-machine problem and its solution procedure studied in this paper will prove useful to a decomposition method that decomposes multiple-machine, multiple-resource scheduling problems into a number of single-machine problems. The total weighted completion time objective is relevant to production environments where inventory levels and manufacturing cycle times are key concerns. Future research can be pursued along two directions. First, it seems to be necessary to further generalize the problem to consider also negative job weights. Second, the solution procedure developed here is ready to be incorporated into a machine-oriented decomposition method such as the shifting bottleneck procedure.     

基于环境建模的物联网系统TAP规则生成方法

用户需求是物联网智能服务的根本驱动力,如IFTTT等很多物联网框架允许用户使用简单的触发-命令编程(TAP)规则进行编程,但它们描述的是设备调度程序,并不是用户服务需求.一些物联网系统提出采用面向目标的需求方法,支持服务目标的分解,但很难保证物联网不同服务间的一致性和服务部署的完整性.为了支持正确的“用户编程”并保证用...     

Identification and control of Hammerstein systems via wireless networks

This article investigates a systematic approach for the identification and control of Hammerstein systems over a physical IEEE 802.11b wireless channel. Three major factors which may affect system stability and stabilisation are concerned: wireless network-induced delays, nonlinearity and model mismatch. First the network-induced delays are characterised by an inverse Gaussian distribution model according to IEEE 802.11b protocol and a model-based compensation method is used to estimate the delayed samples. Then an inverse function of nonlinear part of the identified model is used to attenuate the influence of nonlinearity, while the model mismatch is regarded as disturbance which is then dealt with by H _∞ control approach. A sufficient condition for mean-square asymptotic stability is obtained and expressed by a set of linear matrix inequalities, enabling direct controller design. Finally, numerical simulation examples are used to confirm the efficacy of the proposed approach.     

Self-tuning controller design for systems with arbitrary time delays Part 1. Theoretical development

Self-tuning control of multivariable systems with arbitrary time delays has been an active area of research in recent years. The use of an interactor matrix in deriving controllers for such systems has been suggested by various authors. Factorization of the input polynomial matrix has also been proposed for the controller design stage. It is shown in this paper that these two approaches are not, in general, equivalent. A simple and straightforward procedure for the extraction of the input and output time delay matrices is proposed for the input polynomial matrix factorization approach. Conditions for the time delay matrices to exist are also derived for a class of multivariable systems. These conditions provide a theoretical justification for the use of time delay matrices in self-tuning control of such systems.     

Model-based test generation using extended symbolic grammars

A novel, model-based test case generation approach for validating reactive systems, especially those supporting richly structured data inputs and/or interactions, is presented. Given an executable system model and an extended symbolic grammar specifying plausible system inputs, the approach performs a model-based simulation to (i) ensure the consistency of the model with respect to the specified inputs, and (ii) generate corresponding test cases for validating the system. The model-based simulation produces a state transition diagram (STD) automatically justifying the model runtime behaviors within the test case coverage. The STD can further be transformed to produce an evolved symbolic grammar, which can then be used to incrementally generate a refined set of test cases. As a case study, we present a live sequence chart (LSC) model-based test generator, named LCT in short, for LSC simulation and consistency testing. The evolved symbolic grammar produced by the simulator can either be used to generate practical test cases for software testing, or be further refined by applying our model-based test generation approach again with additional test coverage criteria. We further show that LSCs can also be used to specify and test certain temporal system properties during the model simulation. Their satisfaction, reflected in the STD, can either be served as a directive for selective test generation, or a basis for further temporal property model checking.     

Production-inventory system controller design and supply chain dynamics

The paper deals with the modelling and control of aggregated production-inventory systems as described by differential equations. Hitherto, research in the area has been characterized by the approximation of production delays by first-order lags rather than more realistic pure delays. We demonstrate the substantial qualitative differences between these two approaches and thus generate the motivation for the rest of the paper, which tackles pure delay systems. The application of some relatively new design methodologies for delay systems yields four design choices that are tested for their performance over a range of criteria including stability robustness. The investigation is then extended to the model of a supply chain comprising many such productioninventory systems. The mechanism by which disturbances can be transmitted along the supply chain causing disruption and incurring costs to other supply chain echelons is elucidated. A heuristic feedback policy designed adaptively to tune the individual system designs in response to such disturbances is presented.     

Optimal control of continuous-time switched affine systems

This paper deals with optimal control of switched piecewise affine autonomous systems, where the objective is to minimize a performance index over an infinite time horizon. We assume that the switching sequence has a finite length, and that the decision variables are the switching instants and the sequence of operating modes. We present two different approaches for solving such an optimal control problem. The first approach iterates between a procedure that finds an optimal switching sequence of modes, and a procedure that finds the optimal switching instants. The second approach is inspired by dynamic programming and identifies the regions of the state space where an optimal mode switch should occur, therefore providing a state feedback control law.