Graphical scenarios for specifying temporal properties: an automated approach

Temporal logics are commonly used for reasoning about concurrent systems. Model checkers and other finite-state verification techniques allow for automated checking of system model compliance to given temporal properties. These properties are typically specified as linear-time formulae in temporal logics. Unfortunately, the level of inherent sophistication required by these formalisms too often represents an impediment to move these techniques from “research theory” to “industry practice”. The objective of this work is to facilitate the nontrivial and error prone task of specifying, correctly and without expertise in temporal logic, temporal properties. In order to understand the basis of a simple but expressive formalism for specifying temporal properties we critically analyze commonly used in practice visual notations. Then we present a scenario-based visual language called Property Sequence Chart (PSC) that, in our opinion, fixes the highlighted lacks of these notations by extending a subset of UML 2.0 Interaction Sequence Diagrams. We also provide PSC with both denotational and operational semantics. The operational semantics is obtained via translation into Büchi automata and the translation algorithm is implemented as a plugin of our Charmy tool. Expressiveness of PSC has been validated with respect to well known property specification patterns. Preliminary results appeared in (Autili et al. 2006a).     

New insights on the analysis of nonlinear time-delay systems: Application to the triangular equivalence

In this paper we present recent advances towards an algebraic framework for the analysis and control of nonlinear systems with delays. We show the usefulness of these results by applying them to obtain a constructive characterization of the equivalence of a given system to the so-called triangular form.     

Specifying real-time properties with metric temporal logic

This paper is motivated by the need for a formal specification method for real-time systems. In these systemsquantitative temporal properties play a dominant role. We first characterize real-time systems by giving a classification of such quantitative temporal properties. Next, we extend the usual models for temporal logic by including a distance function to measure time and analyze what restrictions should be imposed on such a function. Then we introduce appropriate temporal operators to reason about such models by turning qualitative temporal operators into (quantitative) metric temporal operators and show how the usual quantitative temporal properties of real-time systems can be expressed in this metric temporal logic. After we illustrate the application of metric temporal logic to real-time systems by several examples, we end this paper with some conclusions.Part of this research has been performed at the Eindhoven University of Technology when the author was working in ESPRIT project 937: Debugging and Specification of Ada Real-Time Embedded Systems (DESCARTES).     

Bond-free DNA language classes

The absence of the ability to form a specified set of bonds in a collection of DNA strands is crucial in the design of experiments encoding algorithmic problems as single- or double-stranded DNA. Recently, the specification of the bonding types to be avoided has been formalized by defining bond-free properties. Bond-free properties generalize several bonding properties which have been studied in the context of DNA computing. In this paper, we consider a bond-free property as defining a class of languages. We study the properties of these classes of languages. We develop new unary operators on languages for characterizing bond-free properties exactly, using familiar code-theoretic equations. These new operators provide a new characterization of maximal bond-free properties as well. We also focus on relationships to classes of languages from the theory of codes. Research supported in part by a grant from NSERC.     

Validation of protocols with temporal constraints

Reachability analysis is the most popular and most used method in protocol validation. It consists in constructing a graph called a reachability graph, describing communication of machines exchanging messages through FIFO channels. The states and structure of this graph are then analysed according to given properties to validate the related communication protocol. In this paper, we deal with a generalization of reachability analysis to take into account quantitative temporal constraints in protocol validation. A temporal reachability graph is designed, and we show how it can be used to analyse new general properties of communication protocols submitted to temporal constraints.     

Generating online test oracles from temporal logic specifications

This paper is concerned with the problem of checking, by means of testing, that a software component satisfies a specification of temporal safety properties. Checking that an actual observed behavior conforms to the specification is performed by a test oracle, which can be either a human tester or a software module. We present a technique for automatically generating test oracles from specifications of temporal safety properties in a metric temporal logic. The logic can express quantitative timing properties, and can also express properties of data values by means of a quantification construct. The generated oracle works online in the sense that checking is performed simultaneously with observation. The technique has been implemented and used in case studies at Volvo Technical Development Corporation .     

A new characterization of the set of all intervals,based on the necessity to check consistency easily

The purpose of this paper is to present a new characterization of the set of all intervals. This characterization is based on several natural properies useful in mathematical modeling; the main of these properties is the necessity to easily check consistency of incompletes knowledge. This characterization is obtained both for one-dimensional and for multidimensional cases.     

Temporal XML: modeling, indexing, and query processing

In this paper we address the problem of modeling and implementing temporal data in XML. We propose a data model for tracking historical information in an XML document and for recovering the state of the document as of any given time. We study the temporal constraints imposed by the data model, and present algorithms for validating a temporal XML document against these constraints, along with methods for fixing inconsistent documents. In addition, we discuss different ways of mapping the abstract representation into a temporal XML document, and introduce TXPath, a temporal XML query language that extends XPath 2.0. In the second part of the paper, we present our approach for summarizing and indexing temporal XML documents. In particular we show that by indexing continuous paths, i.e., paths that are valid continuously during a certain interval in a temporal XML graph, we can dramatically increase query performance. To achieve this, we introduce a new class of summaries, denoted TSummary, that adds the time dimension to the well-known path summarization schemes. Within this framework, we present two new summaries: LCP and Interval summaries. The indexing scheme, denoted TempIndex, integrates these summaries with additional data structures. We give a query processing strategy based on TempIndex and a type of ancestor-descendant encoding, denoted temporal interval encoding. We present a persistent implementation of TempIndex, and a comparison against a system based on a non-temporal path index, and one based on DOM. Finally, we sketch a language for updates, and show that the cost of updating the index is compatible with real-world requirements.     

A complete characterization of deterministic regular liveness properties

Many systems can be modeled formally by nondeterministic Büchi-automata. The complexity of model checking then essentially depends on deciding subset conditions on languages that are recognizable by these automata and that represent the system behavior and the desired properties of the system. The involved complementation process may lead to an exponential blow-up in the size of the automata. We investigate a rich subclass of properties, called deterministic regular liveness properties, for which complementation at most doubles the automaton size if the properties are represented by deterministic Büchi-automata. In this paper, we will present a decomposition theorem for this language class that entails a complete characterization of the deterministic regular liveness properties, and extend an existing incomplete result which then, too, characterizes the deterministic regular liveness properties completely.     

Timed Property Sequence Chart

Property Sequence Chart (PSC) is a novel scenario-based notation, which has been recently proposed to represent temporal properties of concurrent systems. This language balances expressive power and simplicity of use. However, the current version of PSC just represents the order of events and lacks the ability to express timing properties. In real-time systems, it is well known that these timing requirements are very important and need to be specified clearly. Thus, in this paper, we define timed PSC (TPSC) and give the semantics of TPSC in terms of Timed Büchi Automaton (TBA). Then, we measure the expressive power of TPSC based on the recently proposed real-time specification patterns. Finally, we illustrate the use of TPSC in the context of a web service application which requires timing requirements.     

Simulations Up-to and Canonical Preorders: (Extended Abstract)

In this paper we define simulations up-to a preorder and show how we can use them to provide a coinductive, simulation-like, characterization of semantic preorders for processes. The result applies to a wide class of preorders, in particular to all semantic preorders coarser than the ready simulation preorder in the linear time-branching time spectrum. An interesting but unexpected result is that, when built from an equivalence relation, the simulation up-to is a canonical preorder whose kernel is the given equivalence relation. These canonical preorders have several nice properties, the main being that since all of them are defined in a homogeneous way, their properties can be proved in a generic way. In particular, we present an axiomatic characterization of each of these canonical preorders, that is obtained just by adding a single axiom to the axiomatization of the original equivalence relation. This gives us an alternative axiomatization for every axiomatizable preorder in the linear time-branching time spectrum, whose correctness and completeness can be proved once and for all.     

A formal approach for the development of reactive systems

Context

This paper deals with the development and verification of liveness properties on reactive systems using the Event-B method. By considering the limitation of the Event-B method to invariance properties, we propose to apply the language TLA⁺ to verify liveness properties on Event-B models.

Objective

This paper deals with the use of two verification approaches: theorem proving and model-checking, in the construction and verification of safe reactive systems. The theorem prover concerned is part of the Click_n_Prove tool associated to the Event-B method and the model checker is TLC for TLA⁺ models.

Method

To verify liveness properties on Event-B systems, we extend first the expressivity and the semantics of a B model (called temporal B model) to deal with the specification of fairness and eventuality properties. Second, we propose semantics of the extension over traces, in the same spirit as TLA⁺ does. Third, we give verification rules in the axiomatic way of the Event-B method. Finally, we give transformation rules from a temporal B model into a TLA⁺ module. We present in particular, our prototype system called B2TLA⁺, that we have developed to support this transformation; then we can verify liveness properties thanks to the model checker TLC on finite state systems. For the verification of infinite-state systems, we propose the use of the predicate diagrams and its associated tool DIXIT. As the B refinement preserves invariance properties through refinement steps, we propose some rules to get the preservation of liveness properties by the B refinement.

Results

The proposed approach is applied for the development of some reactive systems examples and our prototype system B2TLA⁺ is successfully used to transform a temporal B model into a TLA⁺ module.

Conclusion

The paper successfully defines an approach for the specification and verification of safety and liveness properties for the development of reactive systems using the Event-B method, the language TLA⁺ and the predicate diagrams with their associated tools. The approach is illustrated on a case study of a parcel sorting system.     

Extending temporal query languages to handle imprecise time intervals

Previous work on temporal and historical databases has been mainly based on the assumption that the time intervals of temporal attributes and the start/finish points of modeled events are precisely known. In many real life situations, however, the time boundary of events and the duration of entity relationships may not be exactly known. Modeling these situations and providing a way to write queries dealing with time impreciseness represents a useful extension currently lacking in existing/proposed temporal database systems. In this paper, we discuss the problem of handling time impreciseness in temporal databases and present three models for the representation of imprecise time intervals. We illustrate the basic idea and motivation of each model, its underlying logic, tradeoffs, and important properties. We also propose query language extensions that can enrich the user interface with capabilities to formulate queries dealing with time impreciseness. Extensions to existing query constructs at both the transaction level and the operator level are presented. New operators related to time impreciseness are also presented. The models and extensions discussed in this paper enrich the flexibility of temporal databases and can be used to help users obtain more meaningful replies for their temporal queries.     

First-Order Temporal Verification in Practice

First-order temporal logic, the extension of first-order logic with operators dealing with time, is a powerful and expressive formalism with many potential applications. This expressive logic can be viewed as a framework in which to investigate problems specified in other logics. The monodic fragment of first-order temporal logic is a useful fragment that possesses good computational properties such as completeness and sometimes even decidability. Temporal logics of knowledge are useful for dealing with situations where the knowledge of agents in a system is involved. In this paper we present a translation from temporal logics of knowledge into the monodic fragment of first-order temporal logic. We can then use a theorem prover for monodic first-order temporal logic to prove properties of the translated formulas. This allows problems specified in temporal logics of knowledge to be verified automatically without needing a specialized theorem prover for temporal logics of knowledge. We present the translation, its correctness, and examples of its use. Partially supported by EPSRC project: Analysis and Mechanisation of Decidable First-Order Temporal Logics (GR/R45376/01).     

带数据约束的概率实时系统的验证

带数据约束的概率实时系统是指一种既带有概率时间约束又带有数据变量约束的计算系统。目前将离散数据约束和连续时间约束统一在一个概率模型中的规范及验证研究较少。提出了一种既带有连续数据约束又带有离散数据约束的规范——基于连续时间的概率ZIA规范,并给出了它的时序逻辑。对于CTL和PCTL而言,尽管这些逻辑很强大,但是只能反映时序性质,因此提出一个新的形式化语言CTML来表达度量性质查询,同时保留表达时序性质的能力并给出概率ZIA规范的验证算法。     

WG: A family of stream ciphers with designed randomness properties

In this paper we present a family of stream ciphers which generate a keystream with ideal two-level autocorrelation. The design also guarantees other randomness properties, i.e., balance, long period, ideal tuple distribution, and high and exact linear complexity. We discuss how these properties are achieved by the proposed design and show how to select various parameters to obtain an efficient stream cipher for the desired security level. We also show that the proposed generators are secure against time/memory/data tradeoff attacks, algebraic attacks and correlation attacks. Finally we present WG-128¹ as a concrete example of a WG stream cipher with a key size of 128 bits.     

A unified view of the apriori-based algorithms for frequent episode discovery

Frequent episode discovery framework is a popular framework in temporal data mining with many applications. Over the years, many different notions of frequencies of episodes have been proposed along with different algorithms for episode discovery. In this paper, we present a unified view of all the apriori-based discovery methods for serial episodes under these different notions of frequencies. Specifically, we present a unified view of the various frequency counting algorithms. We propose a generic counting algorithm such that all current algorithms are special cases of it. This unified view allows one to gain insights into different frequencies, and we present quantitative relationships among different frequencies. Our unified view also helps in obtaining correctness proofs for various counting algorithms as we show here. It also aids in understanding and obtaining the anti-monotonicity properties satisfied by the various frequencies, the properties exploited by the candidate generation step of any apriori-based method. We also point out how our unified view of counting helps to consider generalization of the algorithm to count episodes with general partial orders.     

Deriving real-time action systems in a sampling logic

Action systems have been shown to be applicable for modelling and constructing systems in both discrete and hybrid domains. We present a novel semantics for action systems using a sampling logic that facilitates reasoning about the truly concurrent behaviour between an action system and its environment. By reasoning over the apparent states, the sampling logic allows one to determine whether a state predicate is definitely or possibly true over an interval. We present a semantics for action systems that allows the time taken to sample inputs and evaluate expressions (and hence guards) into account. We develop a temporal logic based on the sampling logic that facilitates formalisation of safety, progress, timing and transient properties. Then, we incorporate this logic to the method of enforced properties, which facilitates stepwise refinement of action systems.     

Video summarization and retrieval using singular value decomposition

In this paper, we propose novel video summarization and retrieval systems based on unique properties from singular value decomposition (SVD). Through mathematical analysis, we derive the SVD properties that capture both the temporal and spatial characteristics of the input video in the singular vector space. Using these SVD properties, we are able to summarize a video by outputting a motion video summary with the user-specified length. The motion video summary aims to eliminate visual redundancies while assigning equal show time to equal amounts of visual content for the original video program. On the other hand, the same SVD properties can also be used to categorize and retrieve video shots based on their temporal and spatial characteristics. As an extended application of the derived SVD properties, we propose a system that is able to retrieve video shots according to their degrees of visual changes, color distribution uniformities, and visual similarities.