The Assume-guarantee verification using TL* algorithm implemented in Learner is an important method to alleviate the state space explosion problem in model checking of timed systems, thanks to its divide and conquer strategy. This paper presents an improvement for TL* learning algorithm of Learner by removing the first phase from the verification process and starting learning assumption from λ. This improvement reduces the time complexity and covers a number of cases where assumptions exist while the original TL* algorithm cannot. Besides, this paper adds a kind of bound to the candidate query answering algorithm of Teacher for it to return “don't know” result and prevent Learner from running endlessly. We give some discussions related to both of original algorithms and the improved ones in the paper.

Design by contract and relational interface theories are powerful for specifying component-based systems. We extend these theories with real-time properties so that our technique can model component-based real-time systems. In addition, we use linear temporal logic (LTL) for specifying the invariant properties of contracts. To specify the interaction between methods in a component, and the interaction between components, we use the timed regular expressions over a distributed alphabet. The correctness of a system model is based on the correctness by construction approach. We show several examples that our technique is powerful and useful to guarantee the correctness of component-based systems with real-time requirements.

Interaction Protocol specification is an important part for component interface specification. To use a component, the environment must conform to the interaction protocol specified in the interface of the component. We give a powerful technique to specify protocols which can capture the constraints on temporal order, concurrency, and timing. We also show that the problem of checking if a timed automaton conforms to a given real-time protocol is decidable and develop a decision procedure for solving the problem.

The present paper introduces the notion of distributed transition systems for modeling, designing and understanding distributed computing systems. The concurrency can be expressed explicitly in the model. Some of the global properties of the systems are discussed and determined. It is shown in the paper that by keeping knowledge of other processes in each process of a system, some of its global properties can be synthesized from only few local process states.

In this paper, we consider a subclass of Probabilistic Duration Cal- culus formula called Simple Probabilistic Duration Calculus (SPDC) as a language for specifying dependability requirements for real-time systems, and address the two problems: to decide if a probabilistic timed automaton satisfies a SPDC formula, and to decide if there is a strategy to choose an execution of a given automaton that satisfies a SPDC formula. We prove that the both problems are decidable for a class of SPDC called probabilistic linear duration invariants, and provide a model checking algorithm for solving these problems.

During the execution of multi-threaded and transactional programs, when new threads are created or new transactions are started, memory areas called logs are implicitly allocated to store copies of shared variables so that the threads can independently manipulate these variables. It is not easy to manually calculate the peak of memory allocated for logs when programs have arbitrary mixes of nested transactions and new thread creations. We develop a static analysis to compute the amount of memory used by logs in the worst execution scenarios of the programs. We prove the soundness of our analysis and we show a prototype tool to infer the memory bound.

Class models are often employed to represent domains. In order for class models to conform to their intended domain semantics, we need to ensure their precision and consistency. Precision can be achieved by augmenting the models with constraints, and consistency can be achieved by avoiding contradictory constraints. Model finding is a technique to maintain this kind of consistency. It automatically checks the satisfiability of models by using example instances. However, this technique is often inefficient when applied to large models due to the huge search space. In this paper, we propose a technique to narrow the search space by using patterns to represent constraints. Constraint patterns allow us to put further restrictions on the search space. Our case study illustrates that using constraint patterns in this way can improve the verification process.

We present a type system to estimate an upper bound for the resource consumption of nested and multi-threaded transactional programs. The resource is abstracted as transaction logs. In comparison to our previous work on type and effect systems for Transactional Featherweight Java, this work exploits the natural composition of thread creation to give types to sub-terms. As a result, our new type system is simpler and more effective than our previous one. More important, it is more precise than our previous type system. We also show a type inference algorithm that we have implemented in a prototype tool.

Interface modeling and specification are central issues of component-based software engineering. How a component will be used is specified in its interface. Real-time interfaces are interfaces with timing constraints relating the time of outputs with the time of inputs. The timing constraint of an interface may depend on the resource availability for the component. In this paper, we propose a general model for real-time interfaces. At a time during execution, an interface behaves according to a contract made with environment about its functionality as well as execution time to fulfill the contract. This contract is specified as a timed design using the UTP notations, and depends on the computation histories of the interface. We model this dependence as a partial function from computation histories of the interface to real-time contracts. How interfaces are composed to form new interfaces, how interfaces are refined, and how to represent interfaces finitely are also considered in this paper. We show that checking the consistency between an environment and an interface and checking the refinement between two interfaces when they are represented by an automaton can be done effectively.

This book constitutes the refereed proceedings of the 11th International Symposium on Automated Technology for Verification and Analysis, ATVA 2013, held at Hanoi, Vietnam, in October 2013. The 27 reg

Real-time systems are usually modelled with timed automata and real-time requirements relating to the state durations of the system are often specifiable using Linear Duration Invariants, which is a decidable subclass of Duration Calculus formulas. Various algorithms have been developed to check timed automata or real-time automata for linear duration invariants, but each needs complicated preprocessing and exponential calculation. To the best of our knowledge, these algorithms have not been implemented. In this paper, we present an approximate model checking technique based on a genetic algorithm to check real-time automata for linear durration invariants in reasonable times. Genetic algorithm is a good optimization method when a problem needs massive computation and it works particularly well in our case because the fitness function which is derived from the linear duration invariant is linear. ACM Computing Classification System (1998): D.2.4, C.3.

DC has proved to be a promising tool for the specification and verification of functional requirements on the design of hard real-time systems. Many works were devoted to develop effective techniques for checking the models of hard real-time systems against DC specifications. DC model checking theory is still evolving and yet there is no available tools supporting practical verifications due to the high undecidability of calculus and the great complexity of model checking. Present situation of PDC model checking is much worse than the one of DC model checking. In view of the results so far achieved, it is desirable to develop approximate model checking techniques for DC and PDC specifications. This work was motivated to develop approximate techniques checking automata models of hard real-time systems for DC and PDC specifications. Unlike previous works which only deal with decidable formulas, we want to develop approximate techniques covering whole DC and PDC formulas. The first results of our work, namely, approximate techniques checking real-time automata models of systems for LDI and PLDI specifications, are described in this paper.

This paper proposes a method for specification and verification of distributed real-time systems using timed traces. The key idea of the proposed method is to extend distributed transition systems and linear temporal logic over Foata configurations with time. We show that systems are easily specified and verified with this method. The system behaviors are specified by a distributed duration transition system and the system properties are specified by a formula of our proposed timed logic over timed traces. We give an algorithm for solving the verification problem automatically. We also give an example to illustrate how our algorithm work.

In this paper we propose a formal model for real-time interfaces to support interface specification, composition and refinement with various features. We introduce a practical class of finitely representable interfaces with duration automata as their finite representation. With this sort of representation we can verify component-based systems in a compositional way, and the verification can be started at early stages of the development process for small pieces of the developed systems.

The notion of contract was introduced to component-based software development in order to facilitate the semantically correct composition of components. We extend the form of this notion which is based on designs to capture probabilistic requirements on execution time. We show how reasoning about such requirements can be done in an infinite-interval-based system of probabilistic duration calculus.

This paper proposes a method for specification of concurrency and timing constraints of real-time systems. The key idea of the proposed method is to extend the Mazurkiewicz Traces with time in order to capture the concurrency and timing constraints among the services of systems. The method is formal, effective for abstracting and supporting automated checking.

Linear duration invariants (LDI) are important safety properties of real-time systems. They can be easily formulated in terms of a class of chop-free formulas in the Duration Calculus (DC). Compared to other temporal logics, the specification in DC is simpler, neater and more importantly easier to understand. However, directly model checking them is more difficult than model checking properties formulated in the computation tree logic (CTL). In this paper, we present a technique for the verification of the satisfaction of a LDI D by a timed automaton A by model checking a CTL property. For this, we construct an untimed automaton G from A , and prove that A satisfies D iff D is is satisfied by the set of all paths of G. To Verify that all paths of G satisfy D , we construct a CTL formula ψ and simply check if G satisfies ψ. By this, we convert the problem of verification of the LDI to the problem of model checking CTL formula. As a result, the CTL model checking techniques and tools, such as UPPAAL, can be used for verification of LDI specified in the DC.

In the paper we present a formal model of real-time database (RTDB) systems using Duration Calculus (DC). First, we give a formal speciication of the correctness criterion for the executions of transaction systems and of the Two Phase Locking Concurrency Control Protocol (2PL-CCP). We also give a formal proof for the correctness of the 2PL-CCP using the DC proof system. Then, we present a formal description of the real-time database model by extending the model for untimed DB with state variables expressing temporal objects and with DC formulas to express their behaviour. A formal description of correctness criterion of the parallel executions of transaction systems in RTDBs is then given as the combination of the correctness criterion for the untimed case and the time constraints for the transactions and their read data.

Duration Calculus of Weakly Monotonic Time (WDC) is an extension of DC to allow description of discrete processes where several steps of computation can occur at the same time point. In this paper, we introduce Linear Occurrence Invariants (LOI) using WDC and give an algorithm to check real-time automata for LOI by solving integer programming problems. LOI can be used effectively to specify system requirements in some cases including when the system is considered under the true synchrony assumption. We also extend WDC probabilistically to express dependability requirements of real-time systems and develop a technique to check deterministic probabilistic real-time automata for a class of probabilistic WDC formulas.