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     

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     

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     

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.     

APIs for real-time distributed object programming

Ideally, according to the author, a real-time distributed programming method should be based on a general high-level style that could be easily accommodated by application programmers using C++ and Java. If such a method were to exist, these programmers could specify the interactions among distributed components and the timing requirements of various actions without expending much effort. Facilitating high-level, high precision, real-time object programming by establishing some form of language tools has consequently become a subject of great interest to the embedded systems community. This article focuses on application programming interfaces (APIs) that take the form of C++ and Java class libraries and support high-level, high precision, real-time object programming without requiring new language translators. These APIs wrap the services of the real-time object execution engines, which consist of hardware, node OSs, and middleware; they enable convenient high-level programming almost to the extent that a new real-time object language can. The author explains the API's fundamental features, how they interact among real-time objects, and how multicast channels and real-time multicast APIs contribute     

Language constructs for real-time distributed systems

The paper observes syntactic and semantic requirements for a language for programming real-time distributed systems. A proposal for language features that meet these requirements is offered, and the features are applied to an example.     

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.     

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     

Building finite element analysis programs in distributed services environment

Traditional finite element analysis (FEA) programs are typically built as stand-alone desktop software. This paper describes an Internet-enabled framework that facilitates building a FEA program as distributed web services. The framework allows users easy access to the FEA core service and the analysis results by using a web browser or other application programs. In addition, the framework enables new as well as legacy codes to be incorporated from disparate sites in a dynamic and distributed manner. To provide flexible project management and data access, a database system is employed to store project-related information and selected analysis results. The prototype framework demonstrates that the Internet can potentially enhance the flexibility and extendibility of traditional FEA programs.     

Verification of schedulability for real-time programs

Assume that a real-time programP ^T consisting of a number of parallel processes is executed on a system having a setPr of processors which are shared between the processes by a real-time schedulerS ^T. Assume that P^T must meet some timing deadlines. We show that such an implementation ofP ^T can be represented as a transformationL(P ^T) and that the deadlines ofP ^T will be met if they are satisfied by the timing properties of the transformed program. The condition for feasibility of a real-time program executed under a scheduler is formalized and rules are provided for verification. The schedulerS ^T can be specifiedgenerically and applied to different programs, making it unnecessary to introduce low-level operations such as scheduling primitives into the programming language. Thus real-time program specification and Schedulability can be considered in the same framework and the timing properties of a program can be determined at the specification level. By separating the specification of the scheduler from that of the program, the feasibility of an implementation can be proved by considering a scheduling policy rather than its implementation details.     

Formal derivation of rule-based programs

It is shown that a combination of specification and program refinement may be applied to deriving efficient concurrent rule-based programs. Specification refinement is used to generate an initial rule-based program that is refined into a program which is highly concurrent and efficient. This program derivation strategy is divided into two major tasks. The first task relies on specification refinement. Techniques similar to those employed in the derivation of UNITY programs are used to produce a correct rule-based program having a static knowledge base. The second task involves program refinement and is specific to the development of concurrent rule-based programs. It relies heavily on the availability of a computational model, such as Swarm, that has the ability to dynamically restructure the knowledge base. The ways in which a Swarm program can be translated to OPS5 specifically, given some restrictions, while maintaining the correctness criteria are discussed     

Global cyclic scheduling: A method to guarantee the timing behavior of distributed real-time systems

The use of the global cyclic scheduling discipline in distributed real-time systems guarantees that the response time requirements of the environment are always met. The global scheduling discipline uses cyclic scheduling plans for its decisions. These plans are determined off-line. During the development phase of a real-time system deadlines are checked and the scheduling plans are generated. Software tools support the computation of the scheduling plans. In this paper we discuss the global cyclic scheduling discipline and present a software system to support the development of distributed real-time systems. Our software system consists of a specificaton tool for the real-time software and a schedule computation tool. Three different algorithms for the computation of the scheduling plans are presented.The research work was supported as an Ernst-von-Siemens scholarship of the Siemens AG.     

Specification and analysis of timing requirements for real-time systems in the CBD approach

In real-time software, not only computation errors but also timing errors can cause system failures, which eventually result in significant physical damages or threats to human life. To efficiently guarantee the timely execution of expected functions, it is necessary to clearly specify and formally verify timing requirements before performing detailed system design. With the expected benefit of reusability and extensibility, component technology has been gradually applied to developing industrial applications including real-time systems. However, most of component-based approaches applied to real-time systems lack in a systematic and rigorous approach to specifying and verifying timing requirements at an earlier development stage. This paper proposes a component-based approach to specifying and verifying timing requirements for real-time systems in a systematic and compositional manner. We first describe behaviors of the constituent components including timing requirements in UML diagrams, and then translate the UML diagrams into MTER nets, an extension of TER nets, to perform timing analysis in a compositional way. The merit of the proposed approach is that the specification and analysis results can be reused and independently maintained.     

分布式信任系统的形式化研究

分析了基于委托的信任模型和主观信任模型的信任系统的推导系统,提出了信任策略的形式化描述,并将二者统一于同一推导系统中.在此基础上给出了分布式系统中信任的传递与聚合的基本形式化表达,实现对信任目标的量化计算和分布式传递.最后给出了该方案的应用实例,用于表达分布式网络环境中基于直接信任和推荐信任的计算模型.