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.

     

The design of Apple—A language for modular programs

Sometimes programming is difficult because of the amount of detail that is relevant to the problem being solved. A suitable language for these problems should aid the programmer in organizing a program as a synthesis of parts. Apple is a language designed for such applications. It is a typed language in which functions are objects, and it provides three complementary ways to modularize programs. These are the definition of environments, the use of functional abstraction, and the use of data abstraction or parameterized, abstract data types.In this paper we describe the main features of Apple, and explain the motivation for many of the design decisions. Another document furnishes a formal definition.     

Pattern-based design evolution using graph transformation

In recent years, design patterns gain more interest in software engineering communities for both software development and maintenance. As a template to solve a certain recurring problem, a design pattern documents successful experiences of software experts and gradually becomes the design guidelines of software development. Applying design patterns correctly can improve the efficiency of software design in terms of reusability and enhance maintainability during reverse engineering. Software can be evolved when developers modify their initial designs as requirements change. For instance, a developer may add/delete a set of design elements, such as classes and methods. Modifications on software artifacts can introduce conflicts and inconsistencies in the previously applied design patterns, which are difficult to find and time-consuming to correct. This paper presents a graph-transformation approach to pattern level design validation and evolution. Based on a well founded formalism, we validate a given design by a graph grammar parser and automatically evolve the design at pattern level using a graph-transformation system. Rules for potential pattern evolutions are predefined. The graph-transformation approach preserves the integrity and consistency of design patterns in the system when designs change. A prototype system is built and a case study on the Strategy pattern demonstrates the feasibility of pattern-based design validation and evolution using graph transformation techniques.     

Modula: A language for modular multiprogramming

This paper defines a language called Modula, which is intended primarily for programming dedicated computer systems, including process control systems on smaller machines. The language is largely based on Pascal, but in addition to conventional block structure it introduces a so-called module structure. A module is a set of procedures, data types and variables, where the programmer has precise control over the names that are imported from and exported to the environment. Modula includes general multiprocessing facilities, namely processes, interface modules and signals. It also allows the specification of facilities that represent a computer's specific peripheral devices. Those given in this paper pertain to the PDP-11.     

A method for the modular synthesis of controllers for timed discrete-event systems

A method for the modular supervisory control of timed discrete-event systems (TDES) is presented. The modular synthesis method is an extension of the centralized synthesis method proposed in our earlier work. We consider a state predicate specification as a conjunction of several state subpredicate specifications. The control problem is to synthesize a modular controller, the conjunction of all individual controllers, in such a way that the closed-loop behaviour of TDES satisfies the state predicate specification. Our modular synthesis method is developed based on the concept of state space of TDES, the notion of control-invariant state predicates for the TDES and a fixed point algorithm to calculate a control-invariant state subpredicate of a given state predicate. In addition, for the development of our modular synthesis method, we introduce the notion of control-invariance non-conflict among control-invariant state predicates, and the notion of forcing-non-conflict among controllers synthesized based on control-invariant state predicates which are control-invariance non-conflicting. The modular synthesis method in general offers better design flexibility and may require fewer computations than the centralized one. As in our centralized synthesis method, the proposed modular synthesis method does not require the construction and examination of complete sequences of event trajectories of the system. It is suggested that the computation of our proposed method of yielding solutions for a class of synthesis problems in TDES can be economical.     

A collection operator for graph transformation

Algebraic graph transformation has a wellestablished theory and associated tools that can be used to perform model transformations. However, the lack of a construct to match and transform collections of similar subgraphs makes graph transformation complex or even impractical to use in a number of transformation cases. This is addressed in this paper, by defining a collection operator which is powerful, yet simple to model and understand. A rule can contain multiple collection operators, each with lower and upper bound cardinalities, and the collection operators can be nested. An associated matching process dynamically builds a collection free rule that enables us to reuse the existing graph transformation apparatus. We present model transformation examples from different modeling domains to illustrate the benefit of the approach.     

A simulation-based design paradigm for complex cast components

This paper describes and exercises a new design paradigm for cast components. The methodology integrates foundry process simulation, non-destructive evaluation (NDE), stress analysis and damage tolerance simulations into the design process. Foundry process simulation is used to predict an array of porosity-related anomalies. The probability of detection of these anomalies is investigated with a radiographic inspection simulation tool (XRSIM). The likelihood that the predicted array of anomalies will lead to a failure is determined by a fatigue crack growth simulation based on the extended finite element method and therefore does not require meshing nor remeshing as the cracks grow. With this approach, the casting modeling provides initial anomaly information, the stress analysis provides a value for the critical size of an anomaly and the NDE assessment provides a detectability measure. The combination of these tools allows for accept/reject criteria to be determined at the early design stage and enables damage tolerant design philosophies. The methodology is applied to the design of a cast monolithic door used on the Boeing 757 aircraft.     

基于赋时事件图的故障诊断

赋时事件图(TEG)是一类用于描述同步特性的重要的Petri网.本文提出并研究了基于赋时事件图的故障诊断问题.文中定义了两类系统故障类型:变迁失效(Invalidation)故障和变迁时间延迟(Time_lag)故障.基于事件图关联矩阵,通过研究变迁失效故障的可观测传播特性,引入了故障特征向量的概念.基于此,给出了失效故障的可诊断性的充分必要条件.对于时延故障,提出了一种基于变迁触发时间估计进行故障诊断的简单算法.并基于此算法,研究了时延故障的可诊断条件.     

A genetic algorithm-based solution methodology for modular design

Combinatorial optimization problems usually have a finite number of feasible solutions. However, the process of solving these types of problems can be a very long and tedious task. Moreover, the cost and time for getting accurate and acceptable results is usually quite large. As the complexity and size of these problems grow, the current methods for solving problems such as the scheduling problem or the classification problem have become obsolete, and the need for an efficient method that will ensure good solutions for these complicated problems has increased. This paper presents a genetic algorithm (GA)-based method used in the solution of a set of combinatorial optimization problems. A definition of a combinatorial optimization problem is first given. The definition is followed by an introduction to genetic algorithms and an explanation of their role in solving combinatorial optimization problems such as the traveling salesman problem. A heuristic GA is then developed and used as a tool for solving various combinatorial optimization problems such as the modular design problem. A modularity case study is used to test and measure the performance of the developed algorithm.     

一种用于无线传感器网络的模块化设计方法

针对无线传感器网络应用多样化的特点,建立了基于ZigBee技术的无线传感器网络节点与网关节点的模块化软、硬件设计方案。该硬件方案具有模块化与集成度高的特点,软件方案基于嵌入式操作系统进行多种功能的模块化设计,具有良好扩展性以及可维护性。实现了一种基于单芯片平台的传感器节点与ARM平台的网关节点,讨论了当前与未来适用的各种嵌入式设计关键技术。     

A variable-size local domain approach for increased design confidence in simulation-based optimization

Simulation-based design optimization utilizes computational models that rely on assumptions and approximations. There is a need therefore, to ensure that the obtained designs will exhibit the desired behavior as anticipated given the model predictions. The common approach to accomplish that is to validate the utilized computational models prior to the design optimization process. However, this is practically an impossible task especially for design problems with high-dimensional design and parameter spaces. We have recently proposed a different approach for maximizing confidence in the designs generated during a sequential simulation-based optimization process based on calibrating the computational models when necessary and within local subdomains of the design space. In that work, the size of the local domains was held fixed and not linked to uncertainty, and the confidence in designs was quantified using Bayesian hypothesis testing. In this article, we present an improved methodology. Specifically, we use a statistical methodology to account for uncertainty and to determine the size of the local domains at each stage of the sequential design optimization process using parametric bootstrapping that involves maximum likelihood estimators of model parameters. The sequential process continues until the local domain does not change from stage to stage during the design optimization process, ensuring convergence to an optimal design. The proposed methodology is illustrated with the design of a thermal insulator using one-dimensional, linear heat conduction in a solid slab with heat flux boundary conditions.     

The clock constraint specification language for building timed causality models

The uml Profile for Modeling and Analysis of Real-Time and Embedded (RTE) systems has recently been adopted by the OMG. Its Time Model extends the informal and simplistic Simple Time package proposed by Unified Modeling Language (UML2) and offers a broad range of capabilities required to model RTE systems including discrete/dense and chronometric/logical time. The Marte specification introduces a Time Structure inspired from several time models of the concurrency theory and proposes a new clock constraint specification language (ccsl) to specify, within the context of the uml, logical and chronometric time constraints. A semantic model in ccsl is attached to a (uml) model to give its timed causality semantics. In that sense, ccsl is comparable to the Ptolemy environment, in which directors give the semantics to models according to predefined models of computation and communication. This paper focuses on one historical model of computation of Ptolemy [Synchronous Data Flow (SDF)] and shows how to build SDF graphs by combining uml models and ccsl.     

A framework for the verification of infinite-state graph transformation systems

We propose a technique for the analysis of infinite-state graph transformation systems, based on the construction of finite structures approximating their behaviour. Following a classical approach, one can construct a chain of finite under-approximations (k-truncations) of the Winskel style unfolding of a graph grammar. More interestingly, also a chain of finite over-approximations (k-coverings) of the unfolding can be constructed. The fact that k-truncations and k-coverings approximate the unfolding with arbitrary accuracy is formalised by showing that both chains converge (in a categorical sense) to the full unfolding. We discuss how the finite over- and under-approximations can be used to check properties of systems modelled by graph transformation systems, illustrating this with some small examples. We also describe the Augur tool, which provides a partial implementation of the proposed constructions, and has been used for the verification of larger case studies.     

同步语言Signal在综合航电系统建模仿真中的应用

为了辅助航空电子系统进行综合设计,提出了用Signal语言对新一代综合航电系统进行建模仿真和性能评估的方法。Signal语言是一种同步语言,它通过时钟推理机制来反映复杂系统的确定性、安全性、有界性等问题,能够直观地表示系统元素之间的约束关系及特性,通过构造同步实时评估模型来反映系统的实时性。基于ARINC653标准,对新一代模块化综合航电系统进行了建模仿真。     

Pascal-plus—another language for modular multiprogramming

This paper informally describes the programming language Pascal-Plus. The language is an extended version of Pascal, incorporating the envelope construct which is an aid to program modularization and data abstraction, the process, monitor and condition constructs which provide a means for representing multiprocessing programs, and a simulation monitor which provides pseudo-time control facilities for multiprocessing programs.     

A simulation-based flexible platform for the design and evaluation of rail service infrastructures

We present a simulation-based flexible platform developed to support strategic and tactical decision making related to terminal design and redesign. The platform may be used to implement a wide range of rail–road terminal models, in a rather detailed manner. Moreover, the platform is very easy to use, as no programming skills are needed to construct a complete terminal model and run simulations with it. The platform is composed of two basic elements: a terminal simulation model implemented in Witness® (a commercial simulator) and an interface, implemented in MS Excel®, which enables the user to define the terminal in terms of resources, infrastructures, layout and demand patterns for trains and trucks. The platform provides indicators of service level, productivity and resource use. After presenting the platform, we illustrate its use through a case study where we implement the model of a specific terminal and study its performance under a variety of working conditions.