Symbolic Bounded Model Checking of Abstract State Machines

Abstract State Machines (ASMs) allow modeling system behaviors at any desired level of abstraction, including a level with rich data types, such as sets, sequences, maps, and user-de.ned data types. The availability of high-level data types allow state elements to be represented both abstractly and faithfully at the same time. In this paper we look at symbolic analysis of ASMs. We consider ASMs over a .xed state background T that includes linear arithmetic, sets, tuples, and maps. For symbolic analysis, ASMs are translated into guarded update systems called model programs. We formulate the problem of bounded path exploration of model programs, or the problem of Bounded Model Program Checking (BMPC) as a satis.ability problem modulo T . Then we investigate the boundaries of decidable and undecidable cases for BMPC. In a general setting, BMPC is shown to be highly undecidable (Σ₁¹ -complete); and even when restricting to .nite sets the problem remains re-hard (Σ⁰₁-hard). On the other hand, BMPC is shown to be decidable for a class of basic model programs that are common in practice. We use Satis.ability Modulo Theories (SMT) for solving BMPC; an instance of the BMPC problem is mapped to a formula, the formula is satis.able modulo T if and only if the corresponding BMPC problem instance has a solution. The recent SMT advances allow us to directly analyze speci.cations using sets and maps with specialized decision procedures for expressive fragments of these theories. Our approach is extensible; background theories need in fact only be partially solved by the SMT solver; we use simulation of ASMs to support additional theories that are beyond the scope of available decision procedures.     

Natural Semantics-Directed Generation of Compilers and Abstract Machines

In this paper we present the motivation, theory and transformations of our semantics-directed compiler generator. The main novelty of our generator is that it generates compilers and abstract machines. The execution times of the abstract machine programs produced by our generated compiler compare well to those of target programs produced by compilers generated by other semantics-directed generators. The generated specifications of compilers and abstract machines are suitable as a starting point for handwriting compilers and abstract machines. Our generator is fully automated and its core transformations are proved correct. Received May 1997 / Accepted in revised form May 2000     

A Guarded Fragment for Abstract State Machines

Abstract State Machines (ASMs) provide a formal method for transparent design and specification of complex dynamic systems. They combine advantages of informal and formal methods. Applications of this method motivate a number of computability and decidability problems connected to ASMs. Such problems result for example from the area of verifying properties of ASMs. Their high expressive power leads rather directly to undecidability respectively uncomputability results for most interesting problems in the case of unrestricted ASMs. Consequently, it is rather natural to ask whether there exist expressive classes of ASMs for which we can prove positive decidability and computability results. In this work, we introduce such a class of ASMs. The concept is similar to the one of the guarded fragment of first-order logic. We analyze the expressive power of this class and prove that it is stronger than Datalog LITE and the guarded fragment of first-order fixed point logic. Some decidability and computability results have been proven in earlier works.     

The computable kernel of Abstract State Machines

Abstract State Machines (ASMs) were introduced as “a computation model that is more powerful and more universal than standard computation models”, by Yuri Gurevich in 1985. ASMs gained much attention as a specification method. It is extremely flexible because any mathematical structure may serve as a state. Gurevich characterized the expressive power of ASMs in terms of intuitively convincing postulates.     

Ambient Abstract State Machines with applications

We define a flexible abstract ambient concept which turned out to support current programming practice, in fact can be instantiated to apparently any environment paradigm in use in frameworks for distributed computing with heterogeneous components. For the sake of generality and to also support rigorous high-level system design practice we give the definition in terms of Abstract State Machines. We show the definition to uniformly capture the common static and dynamic disciplines for isolating states or concurrent behavior (e.g. handling of multiple threads for Java) as well as for sharing memory, patterns of object-oriented programming (e.g. for delegation, incremental refinement, encapsulation, views) and agent mobility.     

基于抽象状态的类的行为规格化方法

为独立方法定义严谨的规格可以保证程序的正确性。但是在面向对象的程序中,方法之间因为共享属性而相互影响,这就需要能够反映方法间影响的规格化方法。研究者们使用抽象变量、状态抽象、堆、查询等多种方法进行了尝试。文中给出一种基于抽象状态的类的行为规格方法,该方法基于抽象状态解决了类方法间的共享依赖和相互影响,同时实现了规格与实现的独立描述与运行时自动化验证。     

Completeness of fair ASM refinement

ASM refinements are verified using generalized forward simulations which allow us to refine m abstract operations to n concrete operations with arbitrary m and n. One main difference from data refinement is that ASM refinement considers infinite runs and termination. Since backward simulation does not preserve termination in general, the standard technique of adding history information to the concrete level is not applicable to get a completeness proof. The power set construction also adds infinite runs and is therefore not applicable either. This paper shows that a completeness proof is nevertheless possible by adding infinite prophecy information, effectively moving nondeterminism to the initial state. Adding such prophecy information can be done not only on the semantic level, but also by a simple syntactic transformation that removes the choose construct of ASMs. The completeness proof is also translated to a completeness proof for IO automata. Finally, the proof is extended to deal with supplementary predicates, that specify fairness and liveness assumptions, by transferring a related result of Wim Hesselink for refinements that use the Abadi-Lamport setting.     

System dynamics simulations for data-intensive applications

Simulation modeling is increasingly perceived as a methodological asset to the field of data science. Nonetheless, adequate graphical database interfaces are missing especially for most System Dynamics (SD) simulation tools. SimSyn is freely available middleware used to link together models developed in VENSIM with a PostgreSQL database for spanning SD models over geographic or multi-dimensional parameter space. The capabilities of SimSyn are demonstrated by simulating terrestrial carbon storage for 10,000 years on a 5 arc-min raster mesh with 278,115 grid cells. Results indicated the reasonable performance of data-linked simulations (7, 500 to 10,000 runs per 15 min) and a considerable increase of computational overheads associated with additional time series inputs. Apart from increasing performance, the incorporation of SD interoperability standards is a key objective for the further development of SimSyn.     

基于时间抽象状态机的AADL模型验证

提出了一种基于时间抽象状态机(timed abstract state machine,简称TASM)的AADL(architecture analysis and design language)模型验证方法.分别给出了AADL子集和TASM的抽象语法,并基于语义函数和类ML的元语言形式定义转换规则.在此基础上,基于AADL开源建模环境OSATE(open source AADL tool environment)设计并实现了AADL模型验证与分析工具AADL2TASM,并基于航天器导航、制导与控制系统(guidance,navigation and control)进行了实例性验证.     

Diagnosability Analysis of a Class of Hierarchical State Machines

This paper addresses the problem of fault detection and isolation for a particular class of discrete event dynamical systems called hierarchical finite state machines (HFSMs). A new version of the property of diagnosability for discrete event systems tailored to HFSMs is introduced. This notion, called L₁-diagnosability, captures the possibility of detecting an unobservable fault event using only high level observations of the behavior of an HFSM. Algorithms for testing L₁-diagnosability are presented. In addition, new methodologies are presented for studying the diagnosability properties of HFSMs that are not L₁-diagnosable. These methodologies avoid the complete expansion of an HFSM into its corresponding flat automaton by focusing the expansion on problematic indeterminate cycles only in the associated extended diagnoser.

Graded State Machines: The Representation of Temporal Contingencies in Simple Recurrent Networks

We explore a network architecture introduced by Elman (1990) for predicting successive elements of a sequence. The network uses the pattern of activation over a set of hidden units from time-step t-1, together with element t, to predict element t + 1. When the network is trained with strings from a particular finite-state grammar, it can learn to be a perfect finite-state recognizer for the grammar. When the net has a minimal number of hidden units, patterns on the hidden units come to correspond to the nodes of the grammar; however, this correspondence is not necessary for the network to act as a perfect finite-state recognizer. Next, we provide a detailed analysis of how the network acquires its internal representations. We show that the network progressively encodes more and more temporal context by means of a probability analysis. Finally, we explore the conditions under which the network can carry information about distant sequential contingencies across intervening elements to distant elements. Such information is maintained with relative ease if it is relevant at each intermediate step; it tends to be lost when intervening elements do not depend on it. At first glance this may suggest that such networks are not relevant to natural language, in which dependencies may span indefinite distances. However, embeddings in natural language are not completely independent of earlier information. The final simulation shows that long distance sequential contingencies can be encoded by the network even if only subtle statistical properties of embedded strings depend on the early information. The network encodes long-distance dependencies by shading internal representations that are responsible for processing common embeddings in otherwise different sequences. This ability to represent simultaneously similarities and differences between several sequences relies on the graded nature of representations used by the network, which contrast with the finite states of traditional automata. For this reason, the network and other similar architectures may be called Graded State Machines.     

Abstract Effective Models

We modify Gurevich's notion of abstract machine so as to encompass computational models, that is, sets of machines that share the same domain. We also add an effectiveness requirement. The resultant class of “Effective Models” includes all known Turing-complete state-transition models, operating over any countable domain.     

基于抽象解释的服务间消息的数据约减

面向服务软件中服务间消息的变量值可能存在无穷域的情况,从而导致模型检测时产生状态空间爆炸问题。为了使终止性验证在实践上可行,需要约减模型状态空间的大小,使得计算时间和空间需求合理。为此,基于抽象解释的区间抽象理论扩展了经典区间抽象域方法,并在统一的区间抽象域方法上借助异常控制流图对变量进行区间分析,在此基础上逆向分析得到服务间消息的变量区间集。变量区间上任意值相对于终止性验证是等价性,因此从每一个变量区间集中选取一个代表值,可组成服务间消息变量的约减值,从而为异常处理的终止性验证提供了约减的初始配置,有效避免了状态空间爆炸。     

基于多边形逼近和有限状态机的笔段提取-合并算法

汉字的基本特征表示是笔段,提出一种基于多边形逼近和有限状态机的笔段提取-合并算法.该算法首先找到笔画的拐点(最小内角值小于指定阈值),然后分别寻找拐点两侧曲线段上的拐点,反复执行,直到再也找不到拐点为止.依次连接一个笔画中所有曲线的起点和终点,就形成了该笔画的笔段系列.随后,运用有限状态机描述并判定笔段的状态,并以此判定笔段的合并要求,以最大限度地减少冗余笔段.实验表明,这种算法具有较低的计算复杂度和很好的逼近效果,能适应手写汉字的笔段提取合并要求.     

对象—关系型数据库系统的类型扩展

由于应用的要求 ,需要对传统的关系型数据库系统进行功能扩展。介绍了自主开发的面向对象工程数据库OSCAR中类型扩展的一般方法 ,并从类型存储、类型操纵和类型管理等方面对数据类型的扩展进行了讨论。     

Modular Design of Real-Time Systems Using Hierarchical Communicating Real-time State Machines

This paper proposes a methodology for the development of distributed real-time systems. The methodology consists of the Hierarchical Communicating Real-Time State Machines (H-CRSM) modelling language, and the Violin toolset. H-CRSM combines Statecharts constructs with CSP-like timed communications. Violin provides a visual environment supporting in a seamless way all the life-cycle development phases of an H-CRSM system. Temporal validation rests on assertion checking during system simulation. Code generation is based on Java and a customizable runtime. The practical use of H-CRSM/Violin is shown by an example. A preliminary version of this paper appears in Proc. of Joint Modular Languages Conference (JMLC'2003), Klagenfurt, Austria, August 2003, LNCS 2789, Springer, pp. 110–121. Angelo Furfaro, Phd, is a computer science assistant professor at Unical, DEIS, teaching object-oriented programming. His research interests include: multiagent systems, Petri nets, parallel simulation, verification of time-dependent systems, distributed measurement systems. He is a member of ACM. Libero Nigro is a full professor of computer science at Unical, DEIS, where he teaches object-oriented programming, software engineering and real-time systems courses. He is the responsible of Software Engineering Laboratory (www.lis.deis.unical.it). His current research interests include: software engineering of time-dependent and distributed systems, real-time systems, Petri nets, modeling and parallel simulation of complex systems, distributed measurement systems. Prof. Nigro is a member of ACM and IEEE. Francesco Pupo, Phd, is a computer science assistant professor at Unical, DEIS, teaching introductory programming and computer architecture courses. His research interests include: Petri nets, discrete-event simulation, real-time systems, distributed measurement systems.     

Chord协议的抽象状态机模型

P2P是构筑于互联网的大规模分布计算协议,采用形式化方法对P2P协议的本质原理进行分析,将有助于P2P协议的优化和改进。本文采用抽象状态机(ASM)对经典P2P协议Chord进行分析,用基于抽象状态机语言(Asml)对其建模,设计了核心运行规则,并得到了该协议的有限状态机模型。本文的工作有助于分析、优化P2P协议。     

两类模糊有限状态机积的交换性

利用代数工具矩阵、半群等对两类模糊有限状态机的交换性作了进一步的研究.首先给出了模糊有限状态机是可交换的几个等价刻画,即模糊有限状态机交换与其状态转移矩阵关于模糊矩阵乘法交换等价,与其输入集上字符串关于同余关系构成的乘法半群交换等价,并讨论了模糊有限状态机的直积、级联积、圈积以及和的交换性.其次提出了Mealy-型模糊有限状态机是可交换的概念,同时在新的概念下详细地研究了Mealy-型模糊有限状态机的直积、级联积、圈积以及和、商的交换性.得到了两个(Mealy-型)模糊有限状态机的完全直积、和交换的充要条件;得到两个(Mealy-型)模糊有限状态机的圈积、级联积交换的一个充分条件;证明了商Mealy-型模糊有限状态机保持原Mealy-型模糊有限状态机的交换性.最后给出判别模糊有限状态机交换性的算法.