The Synchronous Approach to Designing Reactive Systems

Synchronous programming is available through several formally defined languages having very different characteristics: Esterel is imperative, while Lustre and Signal are declarative in style; Statecharts and Argos are graphical languages that allow one to program by constructing hierarchical automata. Our motivation for taking the synchronous design paradigm further, integrating imperative, declarative (or dataflow), and graphical programming styles, is that real systems typically have components that match each of these profiles. This paper motivates our interest in the mixed language programming of embedded software around a number of examples, and sketches the semantical foundation of the Synchronie toolset which ensures a coherent computational model. This toolset supports a design trajectory that incorporates rapid prototyping and systematic testing for early design validation, an object oriented development methodology for long term software management, and formal verification at the level of automatically generated object code.     

A Decidable Clock Language for Synchronous Specifications

Presence and absence of signals inside a reaction are inherent to the synchronous paradigm. Clocks are sets of instants (indicating for example when a signal is present) mainly used to describe the control part of data-flow specifications. The language C

we define here expresses relations between clocks. Such relations can describe the combinational part of specifications, as well as particular instantaneous safety properties. We give a decision procedure for C

and apply it to the model-checking of Signal programs abstracted from their state handling part. Thanks to the use of clocks, absence is not explicitly encoded by a special value.     

Micro-Cobol: A Data Processing Language for Microprocessor Systems

New constructs and the essentials of Cobol are combined to Create Micro-Cobol: a new, simple language for small business systems.     

HiPoLDS: A Hierarchical Security Policy Language for Distributed Systems

Expressing security policies to govern distributed systems is a complex and error-prone task. Policies are hard to understand, often expressed with unfriendly syntax, making it difficult for security administrators and for business analysts to create intelligible specifications. We introduce the Hierarchical Policy Language for Distributed Systems (HiPoLDS), which has been designed to enable the specification of security policies in distributed systems in a concise, readable, and extensible way. HiPoLDS design focuses on decentralized execution environments under the control of multiple stakeholders. It represents policy enforcement through the use of distributed reference monitors, which control the flow of information between services. HiPoLDS allows the definition of both abstract and concrete policies, expressing respectively high-level properties required and concrete implementation details to be ultimately introduced into the service implementation.     

RPL:一种基于反应式Agent的机器人编程语言

开放环境下的机器人具有环境敏感性、行为自主性和并发性、反应实时性等特点,这对支撑这类机器人的控制软件及其编程语言提出了新的要求,包括支持对环境进行显式表示,支持自主和并发的行为,需要对行为间在时间、空间、物理上的关系进行规约等等.面向Agent的编程语言将软件系统的基本执行单元视为自主的软件Agent,它为机器人控制软件的构造提供了新的方法和思路.针对开放环境下机器人特点对其编程语言的要求,提出了基于反应式Agent的编程模型RECA和编程语言RPL.RECA将单个机器人的软件系统视为一个反应式Agent,它包括Sen-sorEvent、EventRule和ScenarioBehaviour 3个组成部分,其中SensorEvent是对机器人所处环境信息变化的一种封装;ScenarioBehaviour是对机器人的不同行为进行的规约;EventRule定义了机器人环境输入到行为输出的动态绑定关系.RPL提供了一系列的机制来支持机器人控制软件的编程,包括事件机制、多线程机制、优先级描述、行为动态绑定.最后介绍了RPL程序开发和运行支撑环境的技术框架,并基于NAO机器人分析了机器人作为老人生活助理的案例,验证了该编程模型、语言和运行支撑环境的有效性.     

一种系统生物学建模语言的开发

本文设计并实现了一种用于系统生物学研究的交互式解释型语言——B语言及其运行环境。根据系统生物学标记语言(SBML)的标准定义设计B语言的建模语法，介绍了B语言解释器和运行环境的开发过程，最后通过仿真实例对B语言与Matlab语言的仿真方式进行了比较，结果表明B语言可更快速获得仿真结果。     

Verifying Temporal Properties of Reactive Systems: A STeP Tutorial

We review a number of formal verification techniques supported by STeP, the Stanford Temporal Prover, describing how the tool can be used to verify properties of several versions of the Bakery Mutual exclusion algorithm for mutual exclusion. We verify the classic two-process algorithm and simple variants, as well as an atomic parameterized version. The methods used include deductive verification rules, verification diagrams, automatic invariant generation, and finite-state model checking and abstraction.     

一种多ADSP21060系统的数字仿真平台的同步方法

基于1553B总线的多ADSP21060/20芯片系统广泛应用在控制系统中,在这类系统的测试过程中,传统的采用实物的测试方法存在诸如代价太大等问题,对系统进行数字仿真是解决此类问题的一个有效方法.提出了一种利用总线发送数据的频率和芯片采用频率的不同来确立最小基准时间,并通过时间服务器向所有终端广播包含自定义时间的同步帧,各个终端根据自己的实际情况采取执行-等待-再执行的方式达到同步.     

A Constructive Object Oriented Modeling Language for Information Systems

One of the central aspects in an Information System is the meaning of data in the external world and the information carried by them. We propose a Constructive Object Oriented Modeling Language (COOML) for information systems, based on a constructive logic of pieces of information. The focus is on the definition of a data model suitable for organizing the information stored in OO systems. The underlying constructive logic supports a correct way of storing, exchanging and elaborating information.     

Concurrency in Synchronous Systems

In this paper we introduce the notion of weak endochrony, which extends to a synchronous setting the classical theory of Mazurkiewicz traces. The notion is useful in the synthesis of correct-by-construction communication protocols for globally asynchronous, locally synchronous (GALS) systems. The independence between various computations can be exploited here to provide communication schemes that do not restrict concurrency while still guaranteeing correctness. Such communication schemes are then lighter and more flexible than their latency-insensitive or endo/isochronous counterparts. Work supported by the ARTIST and COLUMBUS IST European projects     

synERJY An Object-oriented Synchronous Language

The programming language synERJY is presented. It integrates object-orientation and synchronous formalisms in the spirit of Esterel, Lustre, and Statecharts.     

Repeating and Remembering Foreign Language Words: Implications for Language Teaching Systems

The current experiment examined the proposal thatvisible speech can help with a difficult signal suchas listening to a foreign language. This work extendsearlier work by examining whether presenting the faceof the speaker improves the accuracy of repetitions ofshort phrases of a language participants had not heardbefore (Korean) as well as examining whether thismanipulation facilitates performance on a subsequentold/new recognition task. The results showed that bothrepetition accuracy and the subsequent memory offoreign language phrases were improved by showing thespeaker's face. The implication of this finding isthat foreign language learning will benefit by usinga presentation method that includes the visible speechof the speaker. Ways that this might be reasonablyachieved using a computer interface are discussed.     

Testing Feature-Rich Reactive Systems

Reactive systems that service multiple clients or users are often highly configurable to provide customized, value-added services to individual users. A large configuration space is characteristic of such systems, resulting in a large test state space. A new framework reduces specification complexity and enables automated testing for such systems. A running example from class-5 telephony illustrates the benefits of this new approach and the experiences gained in developing and testing it.     

一个公开可验证的加密方案

基于高幂离散对数问题,文章构造了一个公开可验证的加密方案.该方案能正确、安全地加密、解密,同时具有公开可验证性,即任何人都可以验证加密者是否正确加密.该方案可用于构造具有公开可验证性的密钥共享方案和安全多方计算方案,可用于保障云计算信息系统数据的保密性、完整性.     

PMaude: Rewrite-based Specification Language for Probabilistic Object Systems

We introduce a rewrite-based specification language for modelling probabilistic concurrent and distributed systems. The language, based on PMaude, has both a rigorous formal basis and the characteristics of a high-level rule-based programming language. Furthermore, we provide tool support for performing discrete-event simulations of models written in PMaude, and for statistically analyzing various quantitative aspects of such models based on the samples that are generated through discrete-event simulation. Because distributed and concurrent communication protocols can be modelled using actors (concurrent objects with asynchronous message passing), we provide an actor PMaude module. The module aids writing specifications in a probabilistic actor formalism. This allows us to easily write specifications that are purely probabilistic – and not just non-deterministic. The absence of such (un-quantified) non-determinism in a probabilistic system is necessary for a form of statistical analysis that we also discuss. Specifically, we introduce a query language called Quantitative Temporal Expressions (or QuaTEx in short), to query various quantitative aspects of a probabilistic model. We also describe a statistical technique to evaluate QuaTEx expressions for a probabilistic model.     

Synchronous/Reactive Programming of Concurrent System Software

Synchronous languages are intended for programming reactive systems. Reactive systems, which include real-time systems and key operating system components, interact continually with their environment. This paper considers the applicability of imperative synchronous/reactive languages to the development of general system software, that is, to the implementation of operating system kernels, file systems, databases, networks, server architectures, device drivers, etc. The languages Esterel and Reactive C (RC) receive special attention as Esterel is the oldest and most developed such language and RC is specifically designed for compatibility with C systems programming. An alternative soft-instruction software architecture is described, which is well suited to real-world system programming. © 1997 by John Wiley & Sons, Ltd.     

A Supermodel Framework Supporting Validated Upgrading of Reactive Systems

A software product is typically upgraded many times over its lifetime. Reactive systems are no exception, undergoing evolutionary version changes to add features and fix bugs. Evolving these stateful systems, such as email clients, software agents, smart cell phones, and personal digital assistants, is complicated by the fact that new versions of the software must deal correctly with legacy instances. Users of earlier versions have invested significant resources in creating the state of the legacy instance, and usually require that this state be upgraded appropriately when the new system version is activated. However, validating the correctness of this upgrading behavior is particularly difficult, whether through testing or automated reasoning techniques like theorem proving or model checking, because legacy states are typically unreachable to the new version of the software. This paper explores this problem and requirements for its solution. It then presents a simple and widely applicable upgrade framework, based upon the idea of a supermodel that allows upgrade behavior to be validated using mainstream approaches. Finally, it also gives techniques for simplifying the validation problem.