Formal timing analysis of distributed systems

Although a large number of formal methods have been reported in the literature, most of them are applicable only at the initial stages of software development. A major reason for this situation is that those formalisms lack expressiveness to describe the behavior of systems with respect to their underlying configurations. On the other hand, recent experience has shown that the complex nature of distributed systems is conveniently described, constructed and managed in terms of their configuration. In this context, with the twin objectives of accurately modelling the real-timed behavior of distributed systems and supporting the analysis of timing behavior with respect to their underlying configurations, we formulate a logic language called distributed logic (DL). DL is a first-order logic augmented with temporal and spatial modalities. The semantics of DL are based on ideas drawn from both the interleaving and partial order models. In addition to the syntax and semantics of the logic, a formal proof scheme for a distributed programming model is also presented. Finally, use of the proof method is illustrated through the analysis of the real-time properties of a sample problem.     

Handling timing errors in distributed programs

The authors describe a tool called TAP, which is defined to aid the programmer in discovering the causes of timing errors in running programs. TAP is similar to a postmortem debugger, using the history of interprocess communication to construct a timing graph, a directed graph where an edge joins node x to node y if event x directly precedes event y in time. The programmer can then use TAP to look at the graph to find the events that occurred in an unacceptable order. Because of the nondeterministic nature of distributed programs, the authors feel a history-keeping mechanism but always be active so that bugs can be dealt with as they occur. The goal is to collect enough information at run time to construct the timing graph if needed. Since it is always active, this mechanism must be efficient. The authors also describe experiments run using TAP and report the impact that TAP's history-keeping mechanism has on the running time of various distributed programs     

Runtime monitoring of timing constraints in distributed real-time systems

Embedded real-time systems often operate under strict timing and dependability constraints. To ensure responsiveness, these systems must be able to provide the expected services in a timely manner even in the presence of faults. In this paper, we describe a run-time environment for monitoring of timing constraints in distributed real-time systems. In particular, we focus on the problem of detecting violations of timing assertions in an environment in which the real-time tasks run on multiple processors, and timing constraints can be either inter-processor or intra-processor constraints. Constraint violations are detected at the earliest possible time by deriving and checking intermediate constraints from the user-specified constraints. If the violations must be detected as early as possible, then the problem of minimizing the number of messages to be exchanged between the processors becomes intractable. We characterize a sub-class of timing constraints that occur commonly in distributed real-time systems and whose message requirements can be minimized. We also take into account the drift among the various processor clocks when detecting a violation of a timing assertion. Finally, we describe a prototype implementation of a distributed run-time monitor.This work was done while the first two authors were at the IBM T.J. Watson Research Center.Supported in part by the Office of Naval Research under grant number N00014-89-J-1040 and by National Science Foundation under grant number CCR-9200858.     

Formal concept analysis based user model for distributed systems

User profile has contributed to customize user access and adjusts applications to its needs. In this respect, automatically building of user profiles issue is an important research area. Nevertheless, standardizing these profiles in terms of representation and acquisition schemes, more especially in large scale systems like Peer-to-Peer systems (P2P), is a complex task. In this paper, we introduce a distributed user profile modelling approach based on user search topics history without the need of any external knowledge resource (e.g., ontology). This model learns from past interests to guess correlations between user requests, associated topics, relevant documents and nodes (i.e., peers) to enhance any information retrieval process. The solution is based on an extension of Formal Concept Analysis (FCA) theory. We also study, the integration of our model in query routing (i.e., content discovery) and results aggregation processes for P2P systems. Carried out experiments, performed under a P2P simulator environment, showed that our model outperforms its competitors in terms of effectiveness and efficiency.     

Compiling real-time programs with timing constraint refinement andstructural code motion

We present a programming language called TCEL (Time-Constrained Event Language), whose semantics are based on time-constrained relationships between observable events. Such a semantics infers only those timing constraints necessary to achieve real-time correctness, without overconstraining the system. Moreover, an optimizing compiler can exploit this looser semantics to help tune the code, so that its worst-case execution time is consistent with its real-time requirements. In this paper we describe such a transformation system, which works in two phases. First, the TCEL source code is translated into an intermediate representation. Then an instruction-scheduling algorithm rearranges selected unobservable operations and synthesizes tasks guaranteed to respect the original event-based constraints     

实时系统动态行为模型的一种形式分析方法*

提出了一种基于统一建模语言UML 2.0的实时系统动态行为模型的形式分析方法。首先给出了UML顺序图的形式化描述,分析了UML顺序图中事件之间的关系;在此基础上,给出一种对象自动机来描述每个对象在UML顺序图描述的场景中所参与的事件序列的方法,并将该方法扩展到带有组合片段的UML 2.0顺序图;最后通过分析UML 2.0顺序图中的时间建模机制,给出了从UML 2.0顺序图中提取时间约束得到时间自动机的算法。     

Static analysis of real-time distributed systems

A static analysis for reasoning about the temporal behaviors of programs in real-time distributed programming languages is proposed. The analysis is based on the action set semantics using the pure maximal parallelism model. It is shown how to specify and verify various timing properties of real-time programs. The approach provides only an approximate timing behavior, because the state information is ignored. However, many interesting properties such as parallel actions, deadlocks, livelocks, terminations, temporal errors, and failures, can be identified. Furthermore, the approach is compositional and thus makes it possible to reason about the timing properties incrementally. The method not only leads to efficient algorithms for the static analysis of CSP programs but also applies to many other languages     

Performance analysis of distributed real-time databases

In a distributed process control system, information about the behavior of physical processes is usually collected and stored in a real-time database which can be remotely accessed by human operators. In this paper we propose an analytic approach to compute the response-time distribution of operator consoles in a distributed process control environment. The technique we develop is based on Markov regenerative processes (MRGPs) and described with the assistance of deterministic and stochastic Petri nets (DSPNs). We construct exact models for performance analysis of centralized and decentralized database architectures. However, due to limitations on the exact solution, we also propose an approximate solution which is then used to study response-time distributions of large systems.     

基于构件的嵌入式实时软件组合时间分析研究

在嵌入式实时软件的开发早期,将构件技术应用于对其进行时间需求的形式化分析中,不但有助于保证软件的正确性和可靠性,还能缩短需求分析周期、提高软件生产率。给出了一种基于构件技术、UML和时间ER网技术的组合时间分析方法,对嵌入式实时软件的时间需求进行分析和检测,实践表明该方法可以检测出需求模型中的时间冲突,有助于保证嵌入式实时软件时间约束的正确性,而且其分析结果具有可复用、可扩展的优点。     

基于多级一致性协议的多核处理器WCET分析方法

由于多核处理器优越的计算性能,多核处理器现已广泛应用在嵌入式实时系统中. 相对于单核处理器,多核处理器存在资源共享竞争、并行任务干扰等因素,尤其是缓存（Cache）一致性问题,导致任务最坏情况执行时间（worst-case execution time,WCET）的预测更加困难.基于以上因素,提出基于多级一致性协议的多核处理器WCET分析方法.该方法针对多级一致性协议体系架构,提出多级一致性域的概念,将多核处理器的数据访问分为域内访问和跨域访问2个层次,根据Cache读写策略和MESI（modify exclusive shared invalid）一致性协议,得出一致性域内部和跨一致性域的Cache状态更新函数,从而实现多级一致性协议嵌套情况下的WCET分析.实验结果表明,在改变Cache配置参数的情况下,该方法分析结果与GEM5仿真结果的变化趋势一致,经过相关性分析,GEM5仿真结果与该方法分析结果相关性系数不低于0.98;在分析精度方面,该方法的平均过估计率为1.30,相比现有方法降低了0.78.

     

Dependability modeling and analysis of distributed programs

Presents a modeling approach based on stochastic Petri nets to estimate the reliability and availability of programs in a distributed computing system environment. In this environment, successful execution of programs is conditioned on the successful access of related files distributed throughout the system. The use of stochastic Petri nets is demonstrated by extending a basic reliability model to account for repair actions when faults occur. To this end, two possible models are discussed: the global repair model, which assumes a centralized repair team that restores the system to its original status when a failure state is reached, and the local repair model, which assumes that repairs are localized to the node where they occur. The former model is useful in evaluating the availability of programs (or the availability of the hardware support) subject to hardware faults that are repaired globally; therefore, the programs of interest can be interrupted. On the other hand, the latter model can be used to evaluate program reliability in the presence of hardware faults subject to repair, without interrupting the normal operation of the system     

Modeling and analysis of scheduling for distributed real-time embedded systems

Aimed at the deficiencies of resources based time Petri nets (RBTPN) in doing scheduling analysis for distributed real-time embedded systems, the assemblage condition of complex scheduling sequences is presented to easily compute scheduling length and simplify scheduling analysis. Based on this, a new hierarchical RBTPN model is proposed. The model introduces the definition of transition border set, and represents it as an abstract transition. The abstract transition possesses all resources of the set, and has the highest priority of each resource; the execution time of abstract transition is the longest time of all possible scheduling sequences. According to the characteristics and assemblage condition of RBTPN, the refinement conditions of transition border set are given, and the conditions ensure the correction of scheduling analysis. As a result, it is easy for us to understand the scheduling model and perform scheduling analysis.     

A debugger for distributed programs

Developing a distributed debugger is much more complex than developing a sequential debugger. This added complexity is mainly due to the non-determinism of events that communication delays introduce into distributed systems. We explore the problems that one must address when designing a distributed program debugger and then describe our design and implementation of DPD (distributed program debugger). Problems addressed include non-determinism of events, finding consistent system states, setting breakpoints, recording events, and checkpointing. Important features of DPD include dynamic roll back and replay, as well as a graphical user interface. DPD has been tested successfully in debugging distributed programs within a distributed facility called REM (remote execution manager).     

A simple distributed garbage collector for distributed real-time Java

The use of real-time distribution middleware programmed with high-level languages like Java is becoming of increasing interest in next generation applications. Technology like Java’s Remote Method Invocation (RMI) paves the way towards these new distributed horizons. RMI offers many high-level abstractions useful for distributed application programmers to reduce their development times. One of these abstractions is a distributed garbage collector (DGC) that removes unreachable remote objects from the distributed ecosystem. However, in real-time Java, distributed garbage collection is underspecified and it introduces unbounded indeterminism on end-to-end real-time Java communications. This article analyzes this problem proposing a simple characterization for a predictable real-time distributed garbage collector (RT-DGC). The approach requires support from the middleware infrastructure that implements the abstraction but it also introduces bounded overhead. The article provides insight on the performance that RT-DGC offers to a distributed real-time Java application and the extra overheads due to the intrinsic cost of this abstraction.     

Formal verification of Ada programs

The Penelope verification editor and its formal basis are described. Penelope is a prototype system for the interactive development and verification of programs that are written in a rich subset of sequential Ada. Because it generates verification conditions incrementally, Penelope can be used to develop a program and its correctness proof in concert. If an already-verified program is modified, one can attempt to prove the modified version by replaying and modifying the original sequence of proof steps. Verification conditions are generated by predicate transformers whose logical soundness can be proven by establishing a precise formal connection between predicate transformation and denotational definitions in the style of continuation semantics. Penelope's specification language, Larch/Ada, belongs to the family of Larch interface languages. It scales up properly, in the sense that one can demonstrate the soundness of decomposing an implementation hierarchically and reasoning locally about the implementation of each node in the hierarchy     

Synchronized UTC for distributed real-time systems

We present a novel technique for establishing a highly accurate global time in fault-tolerant, large-scale distributed real-time systems. Unlike the usual clock synchronization approaches, our clock validation technique provides a precise system time that also relates to an external time standard like UTC with high accuracy. The underlying idea is to validate time information of external time sources like GPS-receivers against a global time maintained by the local clocks in the system. As an example, a promising interval-based clock validation algorithm ICV that exhibits excellent fault-tolerance properties is outlined and analyzed. It requires only a few high-accurate external time sources and provides each node with the actual accuracy of its clock.     

Virtual machines for distributed real-time systems

The steady increase in raw computing power of the processors commonly adopted for distributed real-time systems leads to the opportunity of hosting diverse classes of tasks on the same hardware, for example process control tasks, network protocol stacks and man–machine interfaces.This paper describes how virtualization techniques can be used to concurrently run multiple operating systems on the same physical machine, although they are kept fully separated from the security and execution timing points of view, and still have them exhibit acceptable real-time execution characteristics.With respect to competing approaches, the main advantages of this method are that it requires little or no modifications to the operating systems it hosts, along with a better modularity and clarity of design.