Automated Synthesis of Numerical Programs for Simulation of Rigid Mechanical Systems in Physics-Based Animation

Physics-based animation programs are important in a variety of contexts, including science, engineering, education and entertainment among others. Manual construction of such programs is expensive, time-consuming and prone to error. We have developed a system for automatically synthesizing physics-based animation programs for a significant class of problems: constrained systems of rigid bodies, subject to driving and dissipative forces, under the control of an interactive user. Our system includes a graphical interface for specifying a physical scenario, including objects, geometry and coordinate systems, along with a symbolic interface for specifying dynamical variables, forces and constraints operating in the scenario. The entities defined in the graphical interface serve as the underlying vocabulary for specifications entered in the symbolic interface. Our system partitions the constraints and dynamical variables into classes and assigns each class to be implemented in a different component of a general simulation program scheme. It generates a numerical C⁺⁺ simulation program that drives a real-time animation of the specified scenario. Our system is implemented as a collection of rewrite rules in the Mathematica programming language. Our approach provides some of the benefits of formal deductive program synthesis, while keeping the computational costs of program synthesis more in line with conventional program generator technology. We have successfully tested our system on numerous examples.     

Foundation of logic programming based on inductive definition

A logical system of inference rules intended to give the foundation of logic programs is presented. The distinguished point of the approach taken here is the application of the theory of inductive definitions, which allows us to uniformly treat various kinds of induction schema and also allows us to regardnegation as failure as a kind of induction schema. This approach corresponds to the so-called least fixpoint semantics. Moreover, in our formalism, logic programs are extended so that a condition of a clause may be any first-order formula. This makes it possible to write a quantified specification as a logic program. It also makes the class of induction schemata much larger to include the usual course-of-values inductions.     

Application of the trace assertion method to the specification,design, and verification of automaton programs

The paper considers the application of the trace assertion method [1] for specification and verification of automaton programs [2–4]. The trace assertion method allows the programmer to define an externally visible behavior of an automaton program in a rigorous way, without considering details of its implementation. The method is employed at the requirements specification stage of the system development. The paper introduces techniques for defining semantics of some elements of an automaton program, especially those involved in interactions with the control system. A formal approach to defining states of automaton programs is described. Results of studies related to the verification of specification requirements for automaton programs are also presented.     

LDPChecker一个实时和混成系统模型检验工具

混成系统是一类复杂系统,线性混成系统作为其重要子类,在形式方法中,人们通常使用线性混成自动机来对它建模．虽然线性混成自动机的模型检验问题总的来说还是不可判定的,但对于其中的正环闭合自动机．其对于线性时段性质的满足性能够通过线性规划方法加以检验．为了实现自动检验正环闭合自动机对线性时段性质的满足性,设计并实现了工具LDPChecker．工具LDPChecker能够识别正环闭合自动机并对其进行相应的检验,其主要特色在于它能够对实时和混成系统检验包含可达性在内的许多实时性质,并且能够自动给出诊断信息．     

Algorithmic analysis of nonlinear hybrid systems

We present two methods for translating nonlinear hybrid systems into linear hybrid automata. Properties of the nonlinear systems can then be inferred from the automatic analysis of the translated linear hybrid automata. The first method, called clock translation, replaces constraints on nonlinear variables by constraints on clock variables. The second method, called linear phase-portrait approximation, conservatively overapproximates the phase portrait of a hybrid automaton using piecewise-constant polyhedral differential inclusions. Both methods are sound for safety properties. We illustrate both methods by using HYTECH, a symbolic model checker for linear hybrid automata, to automatically check properties of a nonlinear temperature controller and of a predator-prey ecology     

Partially interpreted schemas for CSP programming

Partially interpreted program schemas are suggested as a tool for formally specifying and defining the range of applicability of patterns of communication. The body of a schema syntactically resembles a program, but contains free variables which represent uninterpreted program sections, domains, functions, or other aspects of the program. The specification of the schema includes both applicability requirements and result assertions, as well as specifications for the free variables. A schema may be instantiated to obtain a correct program for a problem statement by matching a problem's assumptions and requirements to a schema specification, and appropriately substituting entities from the problem statement for the free variables in both the specification and the body of the schema. Examples are given of the types of schemas and specifications needed for distributed computing, and of the potential variety of instantiations.     

Discrete reachability of hybrid systems

This paper concerns hybrid systems subject to discrete-event supervisory control. It investigates the discrete reachability, where the hybrid system should be moved from a discrete initial state z init into a given discrete goal state z goal by a sequence of discrete inputs. The reachability analysis is carried out in three steps. First, a discrete-event model of the hybrid system is set up. Stochastic automata are used to describe all state sequences which may be generated by the hybrid system. Such a model is called complete. Second, methods for the reachability analysis of stochastic automata are elaborated which concern a weak and a strong condition for reachability. Third, these methods are applied to the hybrid system. It is shown that the reachability of the automaton implies the discrete reachability of the hybrid system, because the model is complete. Therefore, the weak and the strong condition for reachability of the stochastic automaton yield a necessary and a sufficient condition for discrete reachability of the hybrid system.     

一种新的离散事件系统监督器综合方法

我们把一个待控离散事件系统中各离散事件赋予满足一定限制条件的控制值并由此得到一个Ｍｅａｌｙ型自动机。再利用Ｍｅａｌｙ型自动机到Ｍｏｏｒｅ型自动机的标准转换算法便得到一个状态赋（控制）值监督器。删除该监督器中所有不可达状态（及对应的子事件串）便获得一个不含多余状态的最大监督器。     

Ptolemy离散事件模型形式化验证方法

Ptolemy是一个广泛应用于信息物理融合系统的建模和仿真工具包,主要通过仿真的方式保证所建模型的正确性.形式化方法是保证系统正确性的重要方法之一.本文提出了一种基于形式模型转换的方法来验证离散事件模型的正确性.离散事件模型根据不同事件的时间戳触发组件,时间自动机模型能够表达这个特征,因此选用Uppaal作为验证工具.首先定义了离散事件模型的形式语义,其次设计了一组从离散事件模型到时间自动机的映射规则.然后在Ptolemy环境中实现了一个插件,可以自动将离散事件模型转换为时间自动机模型,并通过调用Uppaal验证内核完成验证.最后以一个交通信号灯控制系统为例进行了成功的转换和验证,实验结果证实了该方法能够验证Ptolemy离散事件模型的正确性.     

Testing and Monitoring Model-based Generated Program

We propose an integrated framework to test and monitor code generated from hybrid models for embedded systems. The framework consists of the following elements: First, we create a testing automaton as a controlled environment to produce test traces achieving the desired testing criteria; Second, we synthesize a monitoring automaton from the behavior specification to check the run-time behavior of the tested system in response to the test traces; Finally, since both automata are encoded in the same language as the system model, the same code generator may be used to generate a tester and a monitor from the testing automaton and the monitoring automaton. The tester and the monitor may be linked as needed with the code generated from the system model. Our approach yields self-testing and self-monitoring code which may be run both on the simulation level and on the code level. We discuss our approach in its full details through an example on a SONY AIBO robotic dog.     

Resolution approach to testing compatibility of interacting automata

Conclusion The notion of compatibility of automata was proposed in [1] for formalization of requirements that must be met by interacting partial automata. Testing the compatibility of automata is of essential importance for the design of systems that interact with the environment, especially when we use declarative specificatio of the system to be designed. Under the assumptions of this article for the automaton that models the environment, partiality of the specified automaton is a source of possible incompatibility with the environment. When declarative specification is used, we can never decide in advance if the specified automaton is partial or not. Moreover, even a specification thata priori describes a completely defined automaton may be altered by the actions of the designer in the process of design (especially if these actions are incorrect) so that the specified automaton becomes partial. Therefore the initial specification, and each successive specification produced by human intervention in the design process, must be tested for compatibility with the environment. In the methodology of verification design of automata, compatibility testing is used to solve two problems: a) generating the specification of the class of all automata that satisfy the initial specification and are compatible with the specification of the environment; b) testing for correctness the designer's decisions that alter the current specification of the automaton being designed. The results of this article have led to the development of an efficient resolution procedure for testing the compatibility of automaton specification with the specification of the environment. this procedure has been implemented in the system for verification design of automata from their logical specifications. The efficiency of the developed procedure is based on the results of compatibility analysis of automata from [1] and on the restricted resolution strategy whose completeness and correctness have been proved in [2]. Translated from Kibernetika i Sistemnyi Analiz, No. 6, pp. 36–50, November–December, 1994.     

Checking Finite Traces Using Alternating Automata

Alternating automata have been commonly used as a basis for static verification of reactive systems. In this paper we show how alternating automata can be used in runtime verification. We present three algorithms to check at runtime whether a reactive program satisfies a temporal specification, expressed by a linear-time temporal logic formula. The three methods start from the same alternating automaton but traverse the automaton in different ways: depth-first, breadth-first, and backwards, respectively. We then show how an extension of these algorithms, that collects statistical data while verifying the execution trace, can be used for a more detailed analysis of the runtime behavior. All three methods have been implemented and experimental results are presented.     

Hybrid MARTE statecharts

The specification of modeling and analysis of real-time and embedded systems (MARTE) is an extension of the unified modeling language (UML) in the domain of real-time and embedded systems. Even though MARTE time model offers a support to describe both discrete and dense clocks, the biggest effort has been put so far on the specification and analysis of discrete MARTE models. To address hybrid real-time and embedded systems, we propose to extend statecharts using both MARTE and the theory of hybrid automata. We call this extension hybrid MARTE statecharts. It provides an improvement over the hybrid automata in that: the logical time variables and the chronometric time variables are unified. The formal syntax and semantics of hybrid MARTE statecharts are given based on labeled transition systems and live transition systems. As a case study, we model the behavior of a train control system with hybrid MARTE statecharts to demonstrate the benefit.     

Two CEGAR-based approaches for the safety verification of PLC-controlled plants

In this paper we address the safety analysis of chemical plants controlled by programmable logic controllers (PLCs). We consider a specification of the control program of the PLCs, extended with the specification of the dynamic plant behavior. The resulting hybrid models can be transformed to hybrid automata, for which advanced techniques for reachability analysis exist. However, the hybrid automata models are often too large to be analyzed. We propose two counterexample-guided abstraction refinement (CEGAR) approaches to keep the size of the hybrid models moderate.     

Emulating cellular automata in chemical reaction–diffusion networks

Chemical reactions and diffusion can produce a wide variety of static or transient spatial patterns in the concentrations of chemical species. Little is known, however, about what dynamical patterns of concentrations can be reliably programmed into such reaction–diffusion systems. Here we show that given simple, periodic inputs, chemical reactions and diffusion can reliably emulate the dynamics of a deterministic cellular automaton, and can therefore be programmed to produce a wide range of complex, discrete dynamics. We describe a modular reaction–diffusion program that orchestrates each of the fundamental operations of a cellular automaton: storage of cell state, communication between neighboring cells, and calculation of cells’ subsequent states. Starting from a pattern that encodes an automaton’s initial state, the concentration of a “state” species evolves in space and time according to the automaton’s specified rules. To show that the reaction–diffusion program we describe produces the target dynamics, we simulate the reaction–diffusion network for two simple one-dimensional cellular automata using coupled partial differential equations. Reaction–diffusion based cellular automata could potentially be built in vitro using networks of DNA molecules that interact via branch migration processes and could in principle perform universal computation, storing their state as a pattern of molecular concentrations, or deliver spatiotemporal instructions encoded in concentrations to direct the behavior of intelligent materials.     

PSL构造双向交换自动机及非确定自动机的方法

PSL(property specification language)是一种用于描述并行系统的属性规约语言,包括线性时序逻辑FL(foundation language)和分支时序逻辑OBE(optional branching extension)两部分.由于OBE就是CTL(computation tree logic),并且具有时钟声明的公式很容易改写成非时钟公式,因此重点研究了非时钟FL逻辑.为便于进行模型检验,每个FL公式必须转化成为一种可验证形式,通常是自动机(非确定自动机).构造非确定自动机的过程主要是通过中间构建交换自动机来实现.详细给出了由非时钟FL构造双向交换自动机的构造规则.构造规则的核心逻辑不仅仅局限于是在LTL(linear temporal logic)基础上的正规表达式,而且全面而充分地考虑了各种FL操作算子的可能性.并且给出了将双向交换自动机转化为非确定自动机的一种方法.最后,编写了将PSL转化为上述自动机的实现工具.FL双向交换自动机的构造规则计算复杂度仅是FL公式长度的线性表达式,验证了构造规则的正确性.在此基础上,证明了双向交换自动机与其转化的等价的非确定自动机接受的语言相同.上述工作对解决复杂并行系统建模和模型验证问题具有重要的理论意义和应用价值.     

新型一维偏移耦合映像格系统及其动态特性

混沌系统具有复杂的动力学行为,但在数字系统中运行时会出现动力学特性退化的问题。元胞自动机在时间、空间上都具有离散性,能够有效减弱混沌系统在有限精度下的动力学退化问题。基于元胞自动机,提出了一种一维偏移耦合映像格系统,利用初等元胞自动机每次更新的不同状态,动态产生每个格子的耦合索引偏移量,再根据偏移量对混沌序列施加不同的扰动,然后交替切换元胞自动机的迭代规则。最后,对混沌系统的动力学特性进行对比分析以及对该系统产生的时间序列进行量化和随机性检测,仿真实验结果表明,该混沌系统周期更长,遍历性更好,产生的序列随机性更佳,在序列密码算法中有很大的应用价值。     

使用事件自动机规约的C语言有界模型检测

提出使用事件自动机对 C 程序的安全属性进行规约,并给出了基于有界模型检测的形式化验证方法。事件自动机可以规约程序中基于事件的安全属性,且可以描述无限状态的安全属性。事件自动机将属性规约与C程序本身隔离,不会改变程序的结构。在事件自动机的基础上,提出了自动机可达树的概念。结合自动机可达树和有界模型检测技术,给出将事件自动机和C程序转化为可满足性模理论SMT(satisfiability modulo theory)模型的算法。最后,使用SMT求解器对生成的SMT模型求解,并根据求解结果给出反例路径分析算法。实例分析和实验结果表明,该方法可以有效验证软件系统中针对事件的属性规约。     

Using Hybrid Automata to Support Human Factors Analysis in a Critical System

A characteristic that many emerging technologies and interaction techniques have in common is a shift towards tighter coupling between human and computer. In addition to traditional discrete interaction, more continuous interaction techniques, such as gesture recognition, haptic feedback and animation, play an increasingly important role. Additionally, many supervisory control systems (such as flight deck systems) already have a strong continuous element. The complexity of these systems and the need for rigorous analysis of the human factors involved in their operation leads us to examine formal and possibly automated support for their analysis. The fact that these systems have important temporal aspects and potentially involve continuous variables, besides discrete events, motivates the application of hybrid systems modelling, which has the expressive power to encompass these issues. Essentially, we are concerned with human-factors related questions whose answers are dependent on interactions between the user and a complex, dynamic system.In this paper we explore the use of hybrid automata, a formalism for hybrid systems, for the specification and analysis of interactive systems. To illustrate the approach we apply it to the analysis of an existing flight deck instrument for monitoring and controlling the hydraulics subsystem.