Towards a denotational semantics of timed RSL using duration calculus

The Timed RAISE Specification Language(Timed RSL)is an extension of RAISE Specificatioin Language by adding time constructors for specifying real-time applications.Duration Calculus(DC) is a real-time interval logic,which can be used to specify and reason about timing and logical constraints on duration propoerties of Boolean states in a dynamic system.This paper gives a denotational semantics to a subset of Timed RSL expressions,using Duration Calculus extended with super-dense shop modality and notations to capture time point properties of piecewise continuous states of arbitrary types.Using this semantics,the paper pesents a proof rule for verifying Timed RSL iterative expressions and implements the rule to prove the satisfaction by a sample Timed RSL specification of its real-time requrements.     

Duration calculus: Logical foundations

The Duration Calculus (abbreviated DC) represents a logical approach for formal design of real-time systems, where real numbers are used to model time and Boolean valued functions over time are used to model states and events of real-time systems. Since its introduction, DC has been applied to many case studies and it has been extended in several directions. The aim of this paper is to provide a thorough presentation of the logic.on leave of absence from Software Institute, Academia Sinica, Beijing     

Model checking Duration Calculus: a practical approach

Model checking of real-time systems against Duration Calculus (DC) specifications requires the translation of DC formulae into automata-based semantics. The existing algorithms provide a limited DC coverage and do not support compositional verification. We propose a translation algorithm that advances the applicability of model checking tools to realistic applications. Our algorithm significantly extends the subset of DC that can be checked automatically. The central part of the algorithm is the automatic decomposition of DC specifications into sub-properties that can be verified independently. The decomposition is based on a novel distributive law for DC. We implemented the algorithm in a tool chain for the automated verification of systems comprising data, communication, and real-time aspects. We applied the tool chain to verify safety properties in an industrial case study from the European Train Control System (ETCS).     

Model-checking dense-time Duration Calculus

Since the seminal work of Zhou Chaochen, M. R. Hansen, and P. Sestoft on decidability of dense-time Duration Calculus [ZHS93] it is well known that decidable fragments of Duration Calculus can only be obtained through withdrawal of much of the interesting vocabulary of this logic. While this was formerly taken as an indication that key-press verification of implementations with respect to elaborate Duration Calculus specifications were also impossible, we show that the model property is well decidable for realistic designs which feature natural constraints on their switching dynamics.The key issue is that the classical undecidability results rely on a notion of validity of a formula that refers to a class of models which is considerably richer than the possible behaviours of actual embedded real-time systems: that of finitely variable trajectories. By analysing two suitably sparser model classes we obtain model-checking procedures for rich subsets of Duration Calculus. Together with undecidability results also obtained, this sheds light upon the exact borderline between decidability and undecidability of Duration Calculi and related logics.Received June 1999Accepted in revised form September 2003 by M. R. Hansen and C. B. Jones     

基于CORBA的分布式MVC软件体系结构

MVC作为一种经典的软件模式,在界面程序设计和B/S系统中得到广泛应用,但对于分布式实时交互应用而言,其高效性和可扩展性等仍有待提高。本文深入分析了MVC软件模式的结构特点,提出一种基于CORBA的分布式MVC软件体系结构SEV。SEV将动态数据处理从模型中分离出来,并采用CORBA分布对象机制提高系统可扩展性,为面向分布式实时交互式系统的设计提供了高效可扩展的软件参考模型。     

Axiomatisation and decidability of multi-dimensional Duration Calculus

The Shape Calculus is a spatio-temporal logic based on an n-dimensional Duration Calculus tailored for the specification and verification of mobile real-time systems. After showing non-axiomatisability, we give a complete embedding in n-dimensional interval temporal logic and present two different decidable subsets, which are important for tool support and practical use.     

基于多线程MVC模式的航电仿真系统软件设计

为了构建航电仿真系统,提出了一种基于多线程MVC(modal view controller)模式的航电仿真系统软件的设计与实现。软件架构采用多线程MVC模式,在保证系统实时性和数据的可靠性的同时,简化了软件设计的复杂度。对于多线程间的数据同步问题,采用由内存映射技术设计的共享变量池,为系统仿真模块、数据监控模块与参数设置模块之间的大量数据交互提供了可靠的解决方案。测试实验结果证实了该航电仿真系统软件的实时性与可靠性。     

Model-checking discrete duration calculus

Duration Calculus was introduced in [ZHR91] as a logic to specify and reason about requirements for real-time systems. It is an extension of Interval Temporal Logic [Mos85] where one can reason about integrated constraints over time-dependent and Boolean valued states without explicit mention of absolute time. Several major case studies, e.g. the gas burner system in [RRH93], have shown that Duration Calculus provides a high level of abstraction for both expressing and reasoning about specifications. Using Timed Automata [A1D92] one can express how real-time systems can be constructed at a level of detail which is close to an actual implementation. We consider in the paper the correctness of Timed Automata with respect to Duration Calculus formulae. For a subset of Duration Calculus, we show that one can automatically verify whether a Timed Automaton ? is correct with respect to a formulaD, abbreviated ? ?D, i.e. one can domodel-checking. The subset we consider is expressive enough to formalize the requirements to the gas burner system given in [RRH93]; but only for a discrete time domain. Model-checking is done by reducing the correctness problem ? ?D to the inclusion problem of regular languages.     

Advanced Features of Duration Calculus and Their Applications in Sequential Hybrid Programs

Duration Calculus was introduced as a logic to specify real-time requirements of computing systems. It has been used successfully in a number of case studies. Moreover, many variants were proposed to deal with various features of real time systems, including sequential communicating processes, sequential hybrid systems and imperative programming languages. This paper aims to integrate several variants of Duration Calculus, and to provide a semantic framework for real-time programming languages and sequential hybrid programs. A shortversion of this paper appeared in J. Davis, A.W. Roscoe and J.C.P. Woodcock editors, Millennial Perspectives in Computer Science,Proceedings of the 1999 Oxford-Microsoft Symposium in Honour ofProfessor C.A.R. Hoare.     

A unifying action calculus

McCarthy's Situation Calculus is arguably the oldest special-purpose knowledge representation formalism, designed to axiomatize knowledge of actions and their effects. Four decades of research in this area have led to a variety of alternative formalisms: While some approaches can be considered instances or extensions of the classical Situation Calculus, like Reiter's successor state axioms or the Fluent Calculus, there are also special planning languages like ADL and approaches based on a linear (rather than branching) time structure like the Event Calculus. The co-existence of many different calculi has two main disadvantages: The formal relations among them is a largely open issue, and a lot of today's research concerns the transfer of specific results from one approach to another. In this paper, we present a unifying action calculus, which encompasses (well-defined classes of) all of the aforementioned formalisms. Our calculus not only facilitates comparisons and translations between specific approaches, it also allows to solve interesting problems for various calculi at once. We exemplify this by providing a general, calculus-independent solution to a problem of practical relevance, which is intimately related to McCarthy's quest for elaboration tolerant formalisms: the modularity of domain axiomatizations.     

Guaranteed real-time communication in packet-switched networks with FCFS queuing

In this paper, we propose a feasibility analysis of periodic hard real-time traffic in packet-switched networks using first come first served (FCFS) queuing but no traffic shapers. Our work constitutes a framework that can be adopted for real-time analysis of switched low-cost networks like Ethernet without modification of the standard network components. Our analysis is based on a flexible network and traffic model, e.g., variable-sized frames, arbitrary deadlines and multiple switches. The correctness of our real-time analysis and the tightness of it for network components in single-switch networks are given by theoretical proofs. The performance of the end-to-end real-time analysis is evaluated by simulations. Moreover, our conceptual and experimental comparison studies between our analysis and the commonly used Network Calculus (NC) shows that our analysis can achieve better performance than NC in many cases.     

Correctness criteria of some algorithms for uncertain reasoning using Incidence Calculus

Incidence Calculus is a technique for associating uncertainty values with logical sentences. These uncertainty values are called incidences and they are sets of points, which may be thought of as representing equivalence classes of situations, Tarskian models, or possible worlds. Incidence Calculus was originally introduced in [1]. Incidence Calculus was designed to overcome various inherent problems with purely numeric mechanisms for uncertain reasoning [2]. In particular, incidences can represent the dependence between sentences, which numbers cannot, and hence Incidence Calculus can provide genuine, probabilistic reasoning. In this paper we prove soundness and completeness results for some algorithms introduced in [1] and hence satisfy some of the correctness criteria for Incidence Calculus. These algorithms can be used for probabilistic reasoning and to check the consistency of the subjective probabilities of sentences.     

Model-checking discrete duration calculus

Duration Calculus was introduced in [ZHR91] as a logic to specify and reason about requirements for real-time systems. It is an extension of Interval Temporal Logic [Mos85] where one can reason about integrated constraints over time-dependent and Boolean valued states without explicit mention of absolute time. Several major case studies, e.g. the gas burner system in [RRH93], have shown that Duration Calculus provides a high level of abstraction for both expressing and reasoning about specifications. Using Timed Automata [A1D92] one can express how real-time systems can be constructed at a level of detail which is close to an actual implementation. We consider in the paper the correctness of Timed Automata with respect to Duration Calculus formulae. For a subset of Duration Calculus, we show that one can automatically verify whether a Timed Automaton is correct with respect to a formulaD, abbreviated D, i.e. one can domodel-checking. The subset we consider is expressive enough to formalize the requirements to the gas burner system given in [RRH93]; but only for a discrete time domain. Model-checking is done by reducing the correctness problem D to the inclusion problem of regular languages.     

Logical Semantics for the Rewriting Calculus

The Rewriting Calculus has been proposed as a language for defining term rewriting strategies. Rules are explicitly represented as terms, and are applied explicitly to other terms to transform them. Sets of rules may be applied to (sets of) terms non-deterministically to obtain sets of results. Strategies are implemented as rules which accept other rules as arguments and apply them in certain ways. This paper describes work in progress to strengthen the Rewriting Calculus by giving it a logical semantics. Such a semantics can provide crucial guidance for studying the language and increasing its expressive power. The latter is demonstrated by adding support to the Rewriting Calculus for what we call higher-form rewriting, where rules rewrite other rules. The logical semantics used is based on ordered linear logic. The paper develops the ideas through several examples.     

A formal framework for modeling and validating Simulink diagrams

Simulink has been widely used in industry to model and simulate embedded systems. With the increasing usage of embedded systems in real-time safety-critical situations, Simulink becomes deficient to analyze (timing) requirements with high-level assurance. In this article, we apply Timed Interval Calculus (TIC), a real-time specification language, to complement Simulink with TIC formal verification capability. We elaborately construct TIC library functions to model Simulink library blocks which are used to compose Simulink diagrams. Next, Simulink diagrams are automatically transformed into TIC models which preserve functional and timing aspects. Important requirements such as timing bounded liveness can be precisely specified in TIC for whole diagrams or some components. Lastly, validation of TIC models can be rigorously conducted with a high degree of automation using a generic theorem prover. Our framework can enlarge the design space by representing environment properties to open systems, and handle complex diagrams as the analysis of continuous and discrete behavior is supported.     

Assessing effectiveness of learning units under the teaching unit model in an undergraduate mathematics course

This paper reports on the findings of the evaluation of Learning Units (LU), a special type of Learning Object designed to help overcome the difficulties associated with learning Calculus concepts at undergraduate level. An Interactive Platform for Learning Calculus (PIAC) that serves as a container for the LU was created following a specific instructional design, namely, the Teaching Unit Model (TUM), which in turn, rules the platform's design, development and implementation. A general perspective on the development of the platform and its LU is presented, including the results of usability and functionality evaluations, which indicate that the platform and the LU comply with different functionality and usability criteria which are fundamental for their introduction into formal university courses. The platform was utilized in a higher education Calculus course, and its effects on different aspects of the learning process were studied. Two experimental groups and two control groups for a total of 102 students taking the Calculus course participated in the study. Results indicated an overall acceptance of using PIAC in class. Important evidence was obtained on the positive effects of using PIAC, not only influencing academic performance of students, but also in motivational aspects of the learning process. The grades obtained in all of academic activities by the groups using PIAC, compared with the control groups, provide solid evidence to the positive influence of the intervention of the technology under the TUM.     

Adaptive data-driven parallelization of multi-view video coding on multi-core processor

Multi-view video coding (MVC) comprises rich 3D information and is widely used in new visual media,such as 3DTV and free viewpoint TV (FTV). However,even with mainstream computer manufacturers migrating to multi-core processors,the huge computational requirement of MVC currently prohibits its wide use in consumer markets. In this paper,we demonstrate the design and implementation of the first parallel MVC system on Cell Broadband EngineTM processor which is a state-of-the-art multi-core processor. We propose a task-dispatching algorithm which is adaptive data-driven on the frame level for MVC,and implement a parallel multi-view video decoder with modified H.264/AVC codec on real machine. This approach provides scalable speedup (up to 16 times on sixteen cores) through proper local store management,utilization of code locality and SIMD improvement. Decoding speed,speedup and utilization rate of cores are expressed in experimental results.     

Transformational design of real-time systems Part I: From requirements to program specifications

In the two parts of this article a transformational approach to the design of distributed real-time systems is presented. The starting point are global requirements formulated in a subset of Duration Calculus called implementables and the target are programs in an OCCAM dialect PL. In the first part we show how the level of program specifications represented by a language SL can be reached. SL combines regular expressions with ideas from action systems and with time conditions, and can express the distributed architecture of the implementation. While Duration Calculus is state-based, SL is event-based, and the switch between these two worlds is a prominent step in the transformation from implementables to SL. Both parts of the transformational calculus rely on the mixed term techniques by which syntax pieces of two languages are mixed in a semantically coherent manner. In the first part of the article mixed terms between implementables and SL and in the second part of the article mixed terms between SL and PL are used. The approach is illustrated by the example of a computer controlled gas burner. Received: 10 June 1996 / 29 December 1997     

基于极值搜索的光伏电池最大功率点跟踪仿真

针对光伏发电系统中最大功率点跟踪问题,在太阳能电池的数学模型的基础上建立了PV模块的Matlab仿真模型;考虑到了太阳能的波动性和随机性对太阳电池阵列的影响,利用一种基于极值搜索方法的实时MPPT控制原理,控制Buck DC/DC变换电路,结合S函数在Matlab/Simulink环境下建立其动态仿真模型,实现了光伏电池输出的最大功率跟踪;仿真结果表明,该算法具有较好的动态特性和稳态特性,具有一定的实用价值。