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.     

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.     

Abstract machine modelling to produce portable software—a review and evaluation

This paper discusses the use of abstract machine modelling as a technique for producing portable software, i.e. software which can be moved readily from one computer to another. An overview of the principles involved is presented and a critical examination made of three existing abstract machines which were used respectively to implement a macro processor, a text editor and a BASIC compiler.     

Local Encoding Transformations for Optimizing OBDD-Representations of Finite State Machines

Ordered binary decision diagrams are the state-of-the-art representation of switching functions. In order to keep the sizes of OBDDs tractable, heuristics and dynamic reordering algorithms are applied to optimize the underlying variable order. When finite state machines are represented by OBDDs the state encoding can be used as an additional optimization parameter. In this paper, we analyze local encoding transformations which can be applied dynamically. First, we investigate the potential of re-encoding techniques. We then propose the use of an XOR-transformation and show why this transformation is most suitable among the set of all encoding transformations. The presented theoretical framework establishes a new optimization technique for OBDDs.     

Abstract data types for the logical modeling of complex data

In this paper we propose a logical data model for complex data. Our proposal extends the relational model by using abstract data types for domains specification and an extended relational algebra is also introduced. The introduction of the parameterized type Geometry(S), where S is a ground set of elements, allows the representation of complex aggregated data. As an example, we discuss how our model supports the definition of geographical DBMSs. Moreover, to show the generality of our approach, we sketch how the model can be used in the framework of statistical applications.     

一种分布式路由器抽象平台

提出了一种对分布式路由器结构的抽象平台,定义了虚拟网络接口、虚拟转发引擎、虚拟内部连接等虚拟设备,为上层软件提供一个统一的虚拟设备环境。使用这种抽象平台时,路由器原有的各种应用（包括路由协议、管理软件、转发引擎等）均可无更改平滑移植,最大程度上满足分布式结构下的开放性和扩展性。同时,该抽象平台还在很大程度上支持集群工作能力。     

面向数据密集应用的云计算服务架构

提出了一种具有云计算特点的可伸缩的服务器架构,通过采用模块化的方式有效地分割服务功能,能以对用户透明的方式满足三维网络应用的各种存储和带宽的需要。将该方案在一个三维虚拟现实项目中进行测试,结果表明,该方案有较好的伸缩性和效率。     

嵌入式软件中状态机的抽象与实现

文中提出了在嵌入式软件中把状态机作为一个独立模块从控制模块中抽象出来的思想,描述了抽象出来的状态机模块。并介绍了如何将这种状态机抽象模块应用到实际项目中。     

Stuttering for Abstract Probabilistic Automata

Probabilistic Automata (PAs) are a widely-recognized mathematical framework for the specification and analysis of systems with non-deterministic and stochastic behaviors. In a series of recent papers, we proposed Abstract Probabilistic Automata (APAs), a new abstraction framework for representing possibly infinite sets of PAs. We have developed a complete abstraction theory for APAs, and also proposed the first specification theory for them. APAs support both satisfaction and refinement operators, together with classical stepwise design operators.One of the major drawbacks of APAs is that the formalism cannot capture PAs with hidden actions – such actions are however necessary to describe behaviors that shall not be visible to a third party. In this paper, we revisit and extend the theory of APAs to such context. Our first main result takes the form of proposal for a new probabilistic satisfaction relation that captures several definitions of PAs with hidden actions. Our second main contribution is to revisit all the operations and properties defined on APAs for such notions of PAs. Finally, we also establish the first link between stochastic modal logic and APAs, hence linking an automata-based specification theory to a logical one.     

最小二乘双支持向量机的在线学习算法

针对具有两个非并行分类超平面的最小二乘双支持向量机,提出了一种在线学习算法。通过利用矩阵求逆分解引理,所提在线学习算法能充分利用历史的训练结果,避免了大型矩阵的求逆计算过程,从而降低了计算的复杂性。仿真结果验证了所提学习算法的有效性。