Formal verification of timed systems: a survey and perspective
---
paper_title: Verification of an audio protocol with bus collision using Uppaal

paper_content:

In this paper we apply the tool Uppaal1 to an automatic analysis of a version of the Philips Audio Control Protocol with two senders and bus collision handling. This case study is significantly larger than the real-time/hybrid systems previously analysed by automatic tools. During the case study the tool Uppaal was extended with a new feature, committed locations, allowing efficient modelling of broadcast communication.
---
paper_title: DESIGN AND SYNTHESIS OF SYNCHRONIZATION SKELETONS USING BRANCHING TIME TEMPORAL LOGIC

paper_content:

We Propose a method of constructing concurrent programs in which the synchronization skeletonof the program is automatically synthesized from a high-level (branching time) Temporal Logic specification. The synchronization skeleton is an abstraction of the actual program where detail irrelevant to synchronization is suppressed. For example, in the synchronization skeleton for a solution to the critical section problem each process's critical section may be viewed as a single node since the internal structure of the critical section is unimportant. Most solutions to synchronization problems in the literature are in fact given as synchronization skeletons. Because synchronization skeletons are in general finite state, the propositional version of Temporal Logic can be used to specify their properties.
---
paper_title: Symbolic Model Checking for Real-Time Systems

paper_content:

Abstract We describe finite-state programs over real-numbered time in a guarded-command language with real-valued clocks or, equivalently, as finite automata with real-valued clocks. Model checking answers the question which states of a real-time program satisfy a branching-time specification (given in an extension of CTL with clock variables). We develop an algorithm that computes this set of states symbolically as a fixpoint of a functional on state predicates, without constructing the state space. For this purpose, we introduce a μ-calculus on computation trees over real-numbered time. Unfortunately, many standard program properties, such as response for all nonzeno execution sequences (during which time diverges), cannot be characterized by fixpoints: we show that the expressiveness of the timed μ-calculus is incomparable to the expressiveness of timed CTL. Fortunately, this result does not impair the symbolic verification of "implementable" real-time programs-those whose safety constraints are machine-closed with respect to diverging time and whose fairness constraints are restricted to finite upper bounds on clock values. All timed CTL properties of such programs are shown to be computable as finitely approximable fixpoints in a simple decidable theory.
---
paper_title: Hybrid Automata: an algorithmic approach to the specification and verification of hybrid systems

paper_content:

We introduce the framework of hybrid automata as a model and specification language for hybrid systems. Hybrid automata can be viewed as a generalization of timed automata, in which the behavior of variables is governed in each state by a set of differential equations. We show that many of the examples considered in the workshop can be defined by hybrid automata. While the reachability problem is undecidable even for very restricted classes of hybrid automata, we present two semidecision procedures for verifying safety properties of piecewiselinear hybrid automata, in which all variables change at constant rates. The two procedures are based, respectively, on minimizing and computing fixpoints on generally infinite state spaces. We show that if the procedures terminate, then they give correct answers. We then demonstrate that for many of the typical workshop examples, the procedures do terminate and thus provide an automatic way for verifying their properties.
---
paper_title: Timed I/O automata: a mathematical framework for modeling and analyzing real-time systems

paper_content:

We describe the timed input/output automata (TIOA) framework, a general mathematical framework for modeling and analyzing real-time systems. It is based on timed I/O automata, which engage in both discrete transitions and continuous trajectories. The framework includes a notion of external behavior, and notions of composition and abstraction. We define safety and liveness properties for timed I/O automata, and a notion of receptiveness, and prove basic results about all of these notions. The TIOA framework is defined as a special case of the new hybrid I/O automata (HIOA) modeling framework for hybrid systems. Specifically, a TIOA is an HIOA with no external variables; thus, TIOAs communicate via shared discrete actions only, and do not interact continuously. This restriction is consistent with previous real-time system models, and gives rise to some simplifications in the theory (compared to HIOA). The resulting model is expressive enough to describe complex timing behavior, and to express the important ideas of previous timed automata frameworks.
---
paper_title: A Timed Verification of the IEEE 1394 Leader Election Protocol

paper_content:

The IEEE 1394 architecture standard defines a high performance serial multimedia bus that allows several components in a network to communicate with each other at high speed. In the physical layer of the architecture, a leader election protocol is used to find a spanning tree with a unique root in the network topology. If there is a cycle in the network, the protocol treats this as an error situation. This paper presents a formal model of the leader election protocol in the language IOA and a correctness proof. Hereby, it is shown that under certain timing restrictions the protocol behaves correctly. The timing parameters in the IEEE 1394 standard documentation obey the restrictions found in this proof.
---
paper_title: Timed Petri Nets and BQOs

paper_content:

We consider (unbounded) Timed Petri Nets (TPNs) where each token is equipped with a real-valued clock representing the "age" of the token. Each arc in the net is provided with a subinterval of the natural numbers, restricting the ages of the tokens travelling the arc. We apply a methodology developed in [AN00], based on the theory of better quasi orderings (BQOs), to derive an efficient constraint system for automatic verification of safety properties for TPNs. We have implemented a prototype based on our method and applied it for verification of a parametrized version of Fischer's protocol.
---
paper_title: Safety analysis of timing properties in real-time systems

paper_content:

The authors formalize the safety analysis of timing properties in real-time systems. The analysis is based on a formal logic, RTL (real-time logic), which is especially suitable for reasoning about the timing behavior of systems. Given the formal specification of a system and a safety assertion to be analyzed, the goal is to relate the safety assertion to the systems specification. There are three distinct cases: (1) the safety assertion is a theorem derivable from the systems specification; (2) the safety assertion is unsatisfiable with respect to the systems specification; or (3) the negation of the safety assertion is satisfiable under certain conditions. A systematic method for performing safety analysis is presented.
---
paper_title: Model-checking for Probabilistic Real-time Systems

paper_content:

Model-checking is a method of verifying concurrent systems in which a state-graph model of the system behavior is compared with a temporal logic formula. This paper extends model-checking to stochastic real-time systems, whose behavior depends on probabilistic choice and quantitative time. The specification language is TCTL, a branching-time temporal logic for expressing real-time properties. We interpret the formulas of the logic over generalized semi-Markov processes. Our model can express constraints like “the delay between the request and the response is distributed uniformly between 2 to 4 seconds”.
---
paper_title: Formal methods for the specification and design of real-time safety critical systems

paper_content:

Abstract Safety-critical computers increasingly affect nearly every aspect of our lives. Computers control the planes we fly on, monitor our health in hospitals and do our work in hazardous environments. Computers with software deficiencies that fail to meet stringent timing constraints have resulted in catastrophic failures. This article surveys formal methods for specifying, designing, and verifying real-time systems so as to improve their safety and reliability.
---
paper_title: Using HyTech to Verify an Automotive Control System

paper_content:

This paper shows how HyTech, a symbolic model checker for linear hybrid systems, can be used to verify a part of an abstracted automotive control system. The system controls the height of an automobile by a pneumatic suspension system and has been proposed by BMW AG as a case study taken from a current industrial development. For a system which controls one wheel we verify safety properties, such as that the height of the car maintains within desired bounds or that the height is not changed in curves, by reachability analysis. Furthermore, a property related to stability in the sense of control theory is verified. We believe that the case study can serve as a real-life benchmark problem for the formal analysis of embedded reactive systems.
---
paper_title: Formal Methods for Real-Time Computing

paper_content:

From the Publisher: ::: Focusing on formal methods, this book offers a complete coverage of new developments with emphasis on practical application. Starting with a survey of formal methods for real-time systems, topics include program specification, formal methods, analyzing, and design of real-time systems. The book is essential reading for developers of safety critical systems and researchers in the field.
---
paper_title: Automatic verification of finite-state concurrent systems using temporal logic specifications

paper_content:

We give an efficient procedure for verifying that a finite-state concurrent system meets a specification expressed in a (propositional, branching-time) temporal logic. Our algorithm has complexity linear in both the size of the specification and the size of the global state graph for the concurrent system. We also show how this approach can be adapted to handle fairness. We argue that our technique can provide a practical alternative to manual proof construction or use of a mechanical theorem prover for verifying many finite-state concurrent systems. Experimental results show that state machines with several hundred states can be checked in a matter of seconds.
---
paper_title: DESIGN AND SYNTHESIS OF SYNCHRONIZATION SKELETONS USING BRANCHING TIME TEMPORAL LOGIC

paper_content:

We Propose a method of constructing concurrent programs in which the synchronization skeletonof the program is automatically synthesized from a high-level (branching time) Temporal Logic specification. The synchronization skeleton is an abstraction of the actual program where detail irrelevant to synchronization is suppressed. For example, in the synchronization skeleton for a solution to the critical section problem each process's critical section may be viewed as a single node since the internal structure of the critical section is unimportant. Most solutions to synchronization problems in the literature are in fact given as synchronization skeletons. Because synchronization skeletons are in general finite state, the propositional version of Temporal Logic can be used to specify their properties.
---
paper_title: The temporal logic of programs

paper_content:

A unified approach to program verification is suggested, which applies to both sequential and parallel programs. The main proof method suggested is that of temporal reasoning in which the time dependence of events is the basic concept. Two formal systems are presented for providing a basis for temporal reasoning. One forms a formalization of the method of intermittent assertions, while the other is an adaptation of the tense logic system Kb, and is particularly suitable for reasoning about concurrent programs.
---
paper_title: Automatic verification of finite-state concurrent systems using temporal logic specifications

paper_content:

We give an efficient procedure for verifying that a finite-state concurrent system meets a specification expressed in a (propositional, branching-time) temporal logic. Our algorithm has complexity linear in both the size of the specification and the size of the global state graph for the concurrent system. We also show how this approach can be adapted to handle fairness. We argue that our technique can provide a practical alternative to manual proof construction or use of a mechanical theorem prover for verifying many finite-state concurrent systems. Experimental results show that state machines with several hundred states can be checked in a matter of seconds.
---
paper_title: DESIGN AND SYNTHESIS OF SYNCHRONIZATION SKELETONS USING BRANCHING TIME TEMPORAL LOGIC

paper_content:

We Propose a method of constructing concurrent programs in which the synchronization skeletonof the program is automatically synthesized from a high-level (branching time) Temporal Logic specification. The synchronization skeleton is an abstraction of the actual program where detail irrelevant to synchronization is suppressed. For example, in the synchronization skeleton for a solution to the critical section problem each process's critical section may be viewed as a single node since the internal structure of the critical section is unimportant. Most solutions to synchronization problems in the literature are in fact given as synchronization skeletons. Because synchronization skeletons are in general finite state, the propositional version of Temporal Logic can be used to specify their properties.
---
paper_title: Symbolic Model Checking for Real-Time Systems

paper_content:

Abstract We describe finite-state programs over real-numbered time in a guarded-command language with real-valued clocks or, equivalently, as finite automata with real-valued clocks. Model checking answers the question which states of a real-time program satisfy a branching-time specification (given in an extension of CTL with clock variables). We develop an algorithm that computes this set of states symbolically as a fixpoint of a functional on state predicates, without constructing the state space. For this purpose, we introduce a μ-calculus on computation trees over real-numbered time. Unfortunately, many standard program properties, such as response for all nonzeno execution sequences (during which time diverges), cannot be characterized by fixpoints: we show that the expressiveness of the timed μ-calculus is incomparable to the expressiveness of timed CTL. Fortunately, this result does not impair the symbolic verification of "implementable" real-time programs-those whose safety constraints are machine-closed with respect to diverging time and whose fairness constraints are restricted to finite upper bounds on clock values. All timed CTL properties of such programs are shown to be computable as finitely approximable fixpoints in a simple decidable theory.
---
paper_title: On-the-Fly Analysis of Systems with Unbounded, Lossy FIFO Channels

paper_content:

We consider symbolic on-the-fly verification methods for systems of finite-state machines that communicate by exchanging messages via unbounded and lossy FIFO queues. We propose a novel representation formalism, called simple regular expressions (SREs), for representing sets of states of protocols with lossy FIFO channels. We show that the class of languages representable by SREs is exactly the class of downward closed languages that arise in the analysis of such protocols. We give methods for (i) computing inclusion between SREs, (ii) an SRE representing the set of states reachable by executing a single transition in a system, and (iii) an SRE representing the set of states reachable by an arbitrary number of executions of a control loop of a program. All these operations are rather simple and can be carried out in polynomial time. With these techniques, one can construct a semi-algorithm which explores the set of reachable states of a protocol, in order to check various safety properties.
---
paper_title: Parking can get you there faster - Model Augmentation to Speed up Real-Time Model-Checking

paper_content:

Abstract We present an approximation technique, that can render real-time model checking of safety and universal path properties more efficient. It is beneficial, when loops lead to repetition of control situations. Basically we augment a timed automata model with carefully selected extra transitions. This increases the size of the state-space, but potentially decreases the number of symbolic states to be explored by orders of magnitude. We give a formal definition of a timed automata formalism, enriched with basic data types, hand-shake synchronization, urgency, and committed locations. We prove by means of a trace semantics, that if a safety property can be established in the augmented model, it also holds for the original model. We extend our technique to a richer set of properties, that can be decided via a set of traces (universal path properties). In order for universal path properties to carry over to the original model, the semantics of the timed automata formalism is formulated relative to the applied augmentation. Our technique is particularly useful in systems, where a scheduler dictates repetition of control over elapsing time. As a typical example we mention translations of LEGO® RCX™ programs to U ppaal models, where the Round-Robin scheduler is a static entity. We allow scheduler and associated tasks to “park”, until some timing or environmental conditions are met. We apply our technique on a brick-sorter model for a safety property and report run-time data.
---
paper_title: The temporal logic of programs

paper_content:

A unified approach to program verification is suggested, which applies to both sequential and parallel programs. The main proof method suggested is that of temporal reasoning in which the time dependence of events is the basic concept. Two formal systems are presented for providing a basis for temporal reasoning. One forms a formalization of the method of intermittent assertions, while the other is an adaptation of the tense logic system Kb, and is particularly suitable for reasoning about concurrent programs.
---
paper_title: “Sometimes” and “not never” revisited: on branching versus linear time temporal logic

paper_content:

The differences between and appropriateness of branching versus linear time temporal logic for reasoning about concurrent programs are studied. These issues have been previously considered by Lamport. To facilitate a careful examination of these issues, a language, CTL * , in which a universal or existential path quantifier can prefix an arbitrary linear time assertion, is defined. The expressive power of a number of sublanguages is then compared. CTL* is also related to the logics MPL of Abrahamson and PL of Harel, Kozen, and Parikh. The paper concludes with a comparison of the utility of branching and linear time temporal logics.
---
paper_title: A really temporal logic

paper_content:

A real-time temporal logic for the specification of reactive systems is introduced. The novel feature of the logic, TPTL, is the adoption of temporal operators as quantifiers over time variables; every modality binds a variable to the time(s) it refers to. TPTL is demonstrated to be both a natural specification language and a suitable formalism for verification and synthesis. A tableau-based decision procedure and model-checking algorithm for TPTL are presented. Several generalizations of TPTL are shown to be highly undecidable. >
---
paper_title: Real-time logics: complexity and expressiveness

paper_content:

A unifying framework for the study of real-time logics is developed. In analogy to the untimed case, the underlying classical theory of timed state sequences is identified, it is shown to be nonelementarily decidable, and its complexity and expressiveness are used as a point of reference. Two orthogonal extensions of PTL (timed propositional temporal logic and metric temporal logic) that inherit its appeal are defined: they capture elementary, yet expressively complete, fragments of the theory of timed state sequences, and thus are excellent candidates for practical real-time specification languages. >
---
paper_title: Conjoining Specifications

paper_content:

We show how to specify components of concurrent systems. The specification of a system is the conjunction of its components' specifications. Properties of the system are proved by reasoning about its components. We consider both the decomposition of a given system into parts, and the composition of given parts to form a system.
---
paper_title: Explicit clock temporal logic

paper_content:

The authors present a single exponent decision procedure for the validity of XCTL formulas, and a double exponent decision procedure for the validity of XCTL formulas over finite state programs (model checking). The expressive power of XCTL is compared with that of some other logics proposed for the expression of real time properties. It is shown that it is incomparable with the expressive power of the recently proposed logic TPTL (timed propositional temporal logic). >
---
paper_title: Quantitative temporal reasoning

paper_content:

A substantially large class of programs operate in distributed and real-time environments, and an integral part of their correctness specification requires the expression of time-critical properties that relate the occurrence of events of the system. We focus on the formal specification and reasoning about the correctness of such programs. We propose a system of temporal logic, RTCTL (Real-Time Computation Tree Logic), that allows the melding of qualitative temporal assertions together with real-time constraints to permit specification and reasoning at the twin levels of abstraction: qualitative and quantitative. We argue that many practically useful correctness properties of temporal systems, which need to express timing as an essential part of their functionality requirements, can be expressed in RTCTL. We develop a model-checking algorithm for RTCTL whose complexity is linear in the size of the RTCTL specification formula and in the size of the structure. We also present an essentially optimal, exponential time tableau-based decision procedure for the satisfiability of RTCTL formulae. Finally, we consider several variants and extensions of RTCTL for real-time reasoning.
---
paper_title: Automatic verification of finite-state concurrent systems using temporal logic specifications

paper_content:

We give an efficient procedure for verifying that a finite-state concurrent system meets a specification expressed in a (propositional, branching-time) temporal logic. Our algorithm has complexity linear in both the size of the specification and the size of the global state graph for the concurrent system. We also show how this approach can be adapted to handle fairness. We argue that our technique can provide a practical alternative to manual proof construction or use of a mechanical theorem prover for verifying many finite-state concurrent systems. Experimental results show that state machines with several hundred states can be checked in a matter of seconds.
---
paper_title: Symbolic Model Checking for Real-Time Systems

paper_content:

Abstract We describe finite-state programs over real-numbered time in a guarded-command language with real-valued clocks or, equivalently, as finite automata with real-valued clocks. Model checking answers the question which states of a real-time program satisfy a branching-time specification (given in an extension of CTL with clock variables). We develop an algorithm that computes this set of states symbolically as a fixpoint of a functional on state predicates, without constructing the state space. For this purpose, we introduce a μ-calculus on computation trees over real-numbered time. Unfortunately, many standard program properties, such as response for all nonzeno execution sequences (during which time diverges), cannot be characterized by fixpoints: we show that the expressiveness of the timed μ-calculus is incomparable to the expressiveness of timed CTL. Fortunately, this result does not impair the symbolic verification of "implementable" real-time programs-those whose safety constraints are machine-closed with respect to diverging time and whose fairness constraints are restricted to finite upper bounds on clock values. All timed CTL properties of such programs are shown to be computable as finitely approximable fixpoints in a simple decidable theory.
---
paper_title: Safety analysis of timing properties in real-time systems

paper_content:

The authors formalize the safety analysis of timing properties in real-time systems. The analysis is based on a formal logic, RTL (real-time logic), which is especially suitable for reasoning about the timing behavior of systems. Given the formal specification of a system and a safety assertion to be analyzed, the goal is to relate the safety assertion to the systems specification. There are three distinct cases: (1) the safety assertion is a theorem derivable from the systems specification; (2) the safety assertion is unsatisfiable with respect to the systems specification; or (3) the negation of the safety assertion is satisfiable under certain conditions. A systematic method for performing safety analysis is presented.
---
paper_title: Automatic symbolic verification of embedded systems

paper_content:

Presents a model-checking procedure and its implementation for the automatic verification of embedded systems. The system components are described as hybrid automata-communicating machines with finite control and real-valued variables that represent continuous environment parameters such as time, pressure and temperature. The system requirements are specified in a temporal logic with stop-watches, and verified by symbolic fixpoint computation. The verification procedure-implemented in the Cornell Hybrid Technology tool, HyTech-applies to hybrid automata whose continuous dynamics is governed by linear constraints on the variables and their derivatives. We illustrate the method and the tool by checking safety, liveness, time-bounded and duration requirements of digital controllers, schedulers and distributed algorithms.
---
paper_title: Timing Assumptions and Verification of Finite-State Concurrent Systems

paper_content:

We have described a scheme that allows timing assumptions to be incorporated into automatic proofs of arbitrary finite-state temporal properties. The obvious extension is to be able to prove timing properties, not just assume them. This would provide a verification framework for finite-state hard real-time systems. We conjecture that the method presented can, in fact, be extended in this way.
---
paper_title: A really temporal logic

paper_content:

A real-time temporal logic for the specification of reactive systems is introduced. The novel feature of the logic, TPTL, is the adoption of temporal operators as quantifiers over time variables; every modality binds a variable to the time(s) it refers to. TPTL is demonstrated to be both a natural specification language and a suitable formalism for verification and synthesis. A tableau-based decision procedure and model-checking algorithm for TPTL are presented. Several generalizations of TPTL are shown to be highly undecidable. >
---
paper_title: Real-time logics: complexity and expressiveness

paper_content:

A unifying framework for the study of real-time logics is developed. In analogy to the untimed case, the underlying classical theory of timed state sequences is identified, it is shown to be nonelementarily decidable, and its complexity and expressiveness are used as a point of reference. Two orthogonal extensions of PTL (timed propositional temporal logic and metric temporal logic) that inherit its appeal are defined: they capture elementary, yet expressively complete, fragments of the theory of timed state sequences, and thus are excellent candidates for practical real-time specification languages. >
---
paper_title: DESIGN AND SYNTHESIS OF SYNCHRONIZATION SKELETONS USING BRANCHING TIME TEMPORAL LOGIC

paper_content:

We Propose a method of constructing concurrent programs in which the synchronization skeletonof the program is automatically synthesized from a high-level (branching time) Temporal Logic specification. The synchronization skeleton is an abstraction of the actual program where detail irrelevant to synchronization is suppressed. For example, in the synchronization skeleton for a solution to the critical section problem each process's critical section may be viewed as a single node since the internal structure of the critical section is unimportant. Most solutions to synchronization problems in the literature are in fact given as synchronization skeletons. Because synchronization skeletons are in general finite state, the propositional version of Temporal Logic can be used to specify their properties.
---
paper_title: Safety analysis of timing properties in real-time systems

paper_content:

The authors formalize the safety analysis of timing properties in real-time systems. The analysis is based on a formal logic, RTL (real-time logic), which is especially suitable for reasoning about the timing behavior of systems. Given the formal specification of a system and a safety assertion to be analyzed, the goal is to relate the safety assertion to the systems specification. There are three distinct cases: (1) the safety assertion is a theorem derivable from the systems specification; (2) the safety assertion is unsatisfiable with respect to the systems specification; or (3) the negation of the safety assertion is satisfiable under certain conditions. A systematic method for performing safety analysis is presented.
---
paper_title: State/event-based software model checking

paper_content:

We present a framework for model checking concurrent software systems which incorporates both states and events. Contrary to other state/event approaches, our work also integrates two powerful verification techniques, counterexample-guided abstraction refinement and compositional reasoning. Our specification language is a state/event extension of linear temporal logic, and allows us to express many properties of software in a concise and intuitive manner. We show how standard automata-theoretic LTL model checking algorithms can be ported to our framework at no extra cost, enabling us to directly benefit from the large body of research on efficient LTL verification. We have implemented this work within our concurrent C model checker, MAGIC, and checked a number of properties of OpenSSL-0.9.6c (an open-source implementation of the SSL protocol) and Micro-C OS version 2 (a real-time operating system for embedded applications). Our experiments show that this new approach not only eases the writing of specifications, but also yields important gains both in space and in time during verification. In certain cases, we even encountered specifications that could not be verified using traditional pure event-based or state-based approaches, but became tractable within our state/event framework. We report a bug in the source code of Micro-C OS version 2, which was found during our experiments.
---
paper_title: The temporal logic of programs

paper_content:

A unified approach to program verification is suggested, which applies to both sequential and parallel programs. The main proof method suggested is that of temporal reasoning in which the time dependence of events is the basic concept. Two formal systems are presented for providing a basis for temporal reasoning. One forms a formalization of the method of intermittent assertions, while the other is an adaptation of the tense logic system Kb, and is particularly suitable for reasoning about concurrent programs.
---
paper_title: Three logics for branching bisimulation

paper_content:

Three temporal logics are introduced that induce on labeled transition systems the same identifications as branching bisimulation, a behavioral equivalence that aims at ignoring invisible transitions while preserving the branching structure of systems. The first logic is an extension of Hennessy-Milner Logic with an “until” operator. The second one is another extension of Hennessy-Milner Logic, which exploits the power of backward modalities. The third logic is CTL* without the next-time operator. A relevant side-effect of the last characterization is that it sets a bridge between the state- and action-based approaches to the semantics of concurrent systems.
---
paper_title: Modal Transition Systems: A Foundation for Three-Valued Program Analysis

paper_content:

We present Kripke modal transition systems (Kripke MTSs), a generalization of modal transition systems [27, 26], as a foundation for three-valued program analysis. The semantics of Kripke MTSs are presented by means of a mixed power domain of states; soundness and consistency are proved. Two major applications, model checking partial state spaces and three-valued program shape analysis, are presented as evidence of the suitability of Kripke MTSs as a foundation for three-valued analyses.
---
paper_title: Real-time logics: complexity and expressiveness

paper_content:

A unifying framework for the study of real-time logics is developed. In analogy to the untimed case, the underlying classical theory of timed state sequences is identified, it is shown to be nonelementarily decidable, and its complexity and expressiveness are used as a point of reference. Two orthogonal extensions of PTL (timed propositional temporal logic and metric temporal logic) that inherit its appeal are defined: they capture elementary, yet expressively complete, fragments of the theory of timed state sequences, and thus are excellent candidates for practical real-time specification languages. >
---
paper_title: ESTL: A Temporal Logic for Events and States

paper_content:

In some phases of system development state-based methods are adequate; in others event-based methods are adequate. Petri nets provide a system model which supports both methods and thus allow a smooth transition between the different phases of system development. Most temporal logics for Petri nets, however, do not support both methods. ::: ::: In this paper we introduce a temporal logic for Petri nets which allows to argue about states as well as to argue about events. This way, specifications in the early phases can be event-based and verification in later phases can be state-based within a single formalism.
---
paper_title: Quantitative temporal reasoning

paper_content:

A substantially large class of programs operate in distributed and real-time environments, and an integral part of their correctness specification requires the expression of time-critical properties that relate the occurrence of events of the system. We focus on the formal specification and reasoning about the correctness of such programs. We propose a system of temporal logic, RTCTL (Real-Time Computation Tree Logic), that allows the melding of qualitative temporal assertions together with real-time constraints to permit specification and reasoning at the twin levels of abstraction: qualitative and quantitative. We argue that many practically useful correctness properties of temporal systems, which need to express timing as an essential part of their functionality requirements, can be expressed in RTCTL. We develop a model-checking algorithm for RTCTL whose complexity is linear in the size of the RTCTL specification formula and in the size of the structure. We also present an essentially optimal, exponential time tableau-based decision procedure for the satisfiability of RTCTL formulae. Finally, we consider several variants and extensions of RTCTL for real-time reasoning.
---
paper_title: Symbolic model checking for event-driven real-time systems

paper_content:

We consider symbolic model-checking for event-driven real-time systems. The concrete syntax of these systems is given in terms of a graphical programming language called Modechart. We propose a logic, Synchronous Real-Time Event logic (SREL) for specifying the timing properties of these systems. We then present a symbolic model-checking algorithm which checks a modechart against an SREL formula, and discuss several implementation issues. In particular, we give an efficient solution to the problem of encoding timing and event counting functions based on Binary Decision Diagram (BDD). This solution has been incorported into the SMV system v2.3 and has been able to achieve one to two orders of magnitude in speedup and space saving when compared to the solution based on the integer operations provided by the SMV system. >
---
paper_title: Automatic verification of finite-state concurrent systems using temporal logic specifications

paper_content:

We give an efficient procedure for verifying that a finite-state concurrent system meets a specification expressed in a (propositional, branching-time) temporal logic. Our algorithm has complexity linear in both the size of the specification and the size of the global state graph for the concurrent system. We also show how this approach can be adapted to handle fairness. We argue that our technique can provide a practical alternative to manual proof construction or use of a mechanical theorem prover for verifying many finite-state concurrent systems. Experimental results show that state machines with several hundred states can be checked in a matter of seconds.
---
paper_title: Symbolic Model Checking for Real-Time Systems

paper_content:

Abstract We describe finite-state programs over real-numbered time in a guarded-command language with real-valued clocks or, equivalently, as finite automata with real-valued clocks. Model checking answers the question which states of a real-time program satisfy a branching-time specification (given in an extension of CTL with clock variables). We develop an algorithm that computes this set of states symbolically as a fixpoint of a functional on state predicates, without constructing the state space. For this purpose, we introduce a μ-calculus on computation trees over real-numbered time. Unfortunately, many standard program properties, such as response for all nonzeno execution sequences (during which time diverges), cannot be characterized by fixpoints: we show that the expressiveness of the timed μ-calculus is incomparable to the expressiveness of timed CTL. Fortunately, this result does not impair the symbolic verification of "implementable" real-time programs-those whose safety constraints are machine-closed with respect to diverging time and whose fairness constraints are restricted to finite upper bounds on clock values. All timed CTL properties of such programs are shown to be computable as finitely approximable fixpoints in a simple decidable theory.
---
paper_title: Communicating real-time state machines

paper_content:

Communicating real-time state machines (CRSMs), a complete and executable notation for specifying concurrent real-time systems including the monitored and controlled physical environment, are introduced. They are essentially state machines that communicate synchronously in a manner much like the input-output in Hoare's CSP. In addition, CRSMs have a novel and small set of facilities for describing timing properties and accessing real time. The author defines the CRSM language, gives many examples of its use in requirements specification, outlines an algorithm for executing or simulating CRSMs, introduces some techniques for reasoning about the specifications, and discusses some open problems and issues. >
---
paper_title: Efficient Data Structure for Fully Symbolic Verification of Real-Time Software Systems

paper_content:

A new data-structure called RED (Re gion-Encoding Diagram) for the fully symbolic model-checking of real-time software systems is proposed. RED is a BDD-like data-structure for the encoding of regions. Unlike DBM which records differences between pairs of clock readings, RED only uses one auxiliary binary variable for each clock. Thus the number of variables used in RED is always linear to the number of clocks declared in the input system description. Experiment has been carried out to compare RED with previous technologies.
---
paper_title: Communicating sequential processes

paper_content:

This paper suggests that input and output are basic primitives of programming and that parallel composition of communicating sequential processes is a fundamental program structuring method. When combined with a development of Dijkstra's guarded command, these concepts are surprisingly versatile. Their use is illustrated by sample solutions of a variety of familiar programming exercises.
---
paper_title: Timed I/O automata: a mathematical framework for modeling and analyzing real-time systems

paper_content:

We describe the timed input/output automata (TIOA) framework, a general mathematical framework for modeling and analyzing real-time systems. It is based on timed I/O automata, which engage in both discrete transitions and continuous trajectories. The framework includes a notion of external behavior, and notions of composition and abstraction. We define safety and liveness properties for timed I/O automata, and a notion of receptiveness, and prove basic results about all of these notions. The TIOA framework is defined as a special case of the new hybrid I/O automata (HIOA) modeling framework for hybrid systems. Specifically, a TIOA is an HIOA with no external variables; thus, TIOAs communicate via shared discrete actions only, and do not interact continuously. This restriction is consistent with previous real-time system models, and gives rise to some simplifications in the theory (compared to HIOA). The resulting model is expressive enough to describe complex timing behavior, and to express the important ideas of previous timed automata frameworks.
---
paper_title: The Tool KRONOS

paper_content:

Both approaches presented in this paper considerably improve Kronos performance and functionalities.
---
paper_title: UPPAAL - a Tool Suite for Automatic Verification of Real-Time Systems

paper_content:

Uppaal is a tool suite for automatic verification of safety and bounded liveness properties of real-time systems modeled as networks of timed automata. It includes: a graphical interface that supports graphical and textual representations of networks of timed automata, and automatic transformation from graphical representations to textual format, a compiler that transforms a certain class of linear hybrid systems to networks of timed automata, and a model-checker which is implemented based on constraint-solving techniques. Uppaal also supports diagnostic model-checking providing diagnostic information in case verification of a particular real-time systems fails.
---
paper_title: Automatic symbolic verification of embedded systems

paper_content:

Presents a model-checking procedure and its implementation for the automatic verification of embedded systems. The system components are described as hybrid automata-communicating machines with finite control and real-valued variables that represent continuous environment parameters such as time, pressure and temperature. The system requirements are specified in a temporal logic with stop-watches, and verified by symbolic fixpoint computation. The verification procedure-implemented in the Cornell Hybrid Technology tool, HyTech-applies to hybrid automata whose continuous dynamics is governed by linear constraints on the variables and their derivatives. We illustrate the method and the tool by checking safety, liveness, time-bounded and duration requirements of digital controllers, schedulers and distributed algorithms.
---
paper_title: User-Friendly Verification

paper_content:

Model checking often faces the problem of reducing the large exponential sizes of state-space representations. Several reduction techniques such as bisimulation equivalence, partial-order semantics, and symmetry-based reduction have been proposed, but existing tools do not completely allow a user the flexibility in manipulating state spaces. We propose a new user-friendly verification environment where a user has full control on what techniques to apply and in what sequences to apply them. We have implemented the environment in a tool called State-Graph Manipulators (SGM). SGM packages verification techniques into efficient, reusable, modular manipulators, that act on high-level state-space representations called state-graphs. Further, we are also proposing four new state-space reduction techniques, namely variable shielding, read-write analysis, internal transitions bypassing, and sibling transition multiplicity reduction. They are implemented into SGM and experiments have been conducted to show their usefulness.
---
paper_title: Symbolic Verification of Complex Real-Time Systems with Clock-Restriction Diagram

paper_content:

Real-world real-time systems may involve many complex structures, which are difficult to verify. We experiment with the model-checking of an application-layer html-based web-camera which involves structures like event queues, high-layer communication channels, and time-outs. To contain the complexity, we implement our verification tool with a newly developed BDD-like data-structure, reduced CRD (Clock-Restriction Diagram), which has enhanced the verification performance through intensive data-sharing in a previous report. However, the representation of reduced CRD does not allow for quick test of zone containment. To this purpose, we thus have designed a new CRD-based representation, cascade CRD, which has given us enough performance enhancement to successfully verifying several implementations of the web-camera.
---
paper_title: Automatic verification on the large

paper_content:

An automatic verification method from a high level resource management standpoint is presented. Various manipulators can be incorporated in the method to construct, refine, reduce, and model-check state space representation. Proper combinations of manipulators can then be picked strategically by users or computers for less resource (time and space) consumption. An algorithm based on group theory to pick a manipulator combination is presented. Verification sessions are conducted to illustrate our idea.
---
paper_title: Compiling Real-Time Specifications into Extended Automata

paper_content:

A method for the implementation and analysis of real-time systems, based on the compilation of specification extended automata is proposed. The method is illustrated for a simple specification language that can be viewed as the extension of a language for the description of systems of communicating processes, by adding timeout and watchdog constructs. The main result is that such a language can be compiled into timed automata, which are extended automata with timers. Timers are special state variables that can be set to zero by transitions, and whose values measure the time elapsed since their last reset. Timed automata do not make any assumption about the nature of time and adopt an event-driven execution mode. Their complexity does not depend on the values of the parameters of timeouts and watchdogs used in specifications. These features allow the application on timed automata of efficient code generation and analysis techniques. In particular, it is shown how symbolic model-checking of real-time properties can be directly applied to this model. >
---
paper_title: Automatic symbolic verification of embedded systems

paper_content:

Presents a model-checking procedure and its implementation for the automatic verification of embedded systems. The system components are described as hybrid automata-communicating machines with finite control and real-valued variables that represent continuous environment parameters such as time, pressure and temperature. The system requirements are specified in a temporal logic with stop-watches, and verified by symbolic fixpoint computation. The verification procedure-implemented in the Cornell Hybrid Technology tool, HyTech-applies to hybrid automata whose continuous dynamics is governed by linear constraints on the variables and their derivatives. We illustrate the method and the tool by checking safety, liveness, time-bounded and duration requirements of digital controllers, schedulers and distributed algorithms.
---
paper_title: Safety analysis of timing properties in real-time systems

paper_content:

The authors formalize the safety analysis of timing properties in real-time systems. The analysis is based on a formal logic, RTL (real-time logic), which is especially suitable for reasoning about the timing behavior of systems. Given the formal specification of a system and a safety assertion to be analyzed, the goal is to relate the safety assertion to the systems specification. There are three distinct cases: (1) the safety assertion is a theorem derivable from the systems specification; (2) the safety assertion is unsatisfiable with respect to the systems specification; or (3) the negation of the safety assertion is satisfiable under certain conditions. A systematic method for performing safety analysis is presented.
---
paper_title: HOL: A Proof Generating System for Higher-Order Logic

paper_content:

HOL is a version of Robin Milner’s LCF theorem proving system for higher-order logic. It is currently being used to investigate (1) how various levels of hardware behaviour can be rigorously modelled and (2) how the resulting behavioral representations can be the basis for verification by mechanized formal proof. This paper starts with a tutorial introduction to the meta-language ML. The version of higher-order logic implemented in the HOL system is then described. This is followed by an introduction to goal-directed proof with tactics and tacticals. Finally, there is a little example of the system in action which illustrates how HOL can be used for hardware verification.
---
paper_title: Isabelle: The Next 700 Theorem Provers

paper_content:

Isabelle is a generic theorem prover, designed for interactive reasoning in a variety of formal theories. At present it provides useful proof procedures for Constructive Type Theory, various first-order logics, Zermelo-Fraenkel set theory, and higher-order logic. This survey of Isabelle serves as an introduction to the literature. It explains why generic theorem proving is beneficial. It gives a thorough history of Isabelle, beginning with its origins in the LCF system. It presents an account of how logics are represented, illustrated using classical logic. The approach is compared with the Edinburgh Logical Framework. Several of the Isabelle object-logics are presented.
---
paper_title: The Algorithmic Analysis of Hybrid Systems

paper_content:

We present a general framework for the formal specification and algorithmic analysis of hybrid systems. A hybrid system consists of a discrete program with an analog environment. We model hybrid systems as finite automata equipped with variables that evolve continuously with time according to dynamical laws. For verification purposes, we restrict ourselves to linear hybrid systems, where all variables follow piecewise-linear trajectories. We provide decidability and undecidability results for classes of linear hybrid systems, and we show that standard program-analysis techniques can be adapted to linear hybrid systems. In particular, we consider symbolic model-checking and minimization procedures that are based on the reachability analysis of an infinite state space. The procedures iteratively compute state sets that are definable as unions of convex polyhedra in multidimensional real space. We also present approximation techniques for dealing with systems for which the iterative procedures do not converge.
---
paper_title: An interval logic for real-time system specification

paper_content:

Formal techniques for the specification of real time systems must be capable of describing system behavior as a set of relationships expressing the temporal constraints among events and actions, including properties of invariance, precedence, periodicity, liveness, and safety conditions. The paper describes a Temporal-Interval Logic with Compositional Operators (TILCO) designed expressly for the specification of real time systems. TILCO is a generalization of classical temporal logics based on the operators, eventually and henceforth; it allows both qualitative and quantitative specification of time relationships. TILCO is based on time intervals and can concisely express temporal constraints with time bounds, such as those needed to specify real time systems. This approach can be used to verify the completeness and consistency of specifications, as well as to validate system behavior against its requirements and general properties. TILCO has been formalized by using the theorem prover Isabelle/HOL. TILCO specifications satisfying certain properties are executable by using a modified version of the Tableaux algorithm. The paper defines TILCO and its axiomatization, highlights the tools available for proving properties of specifications and for their execution, and provides an example of system specification and validation.
---
paper_title: A timed model for communicating sequential processes

paper_content:

The parallel language CSP [9], an earlier version of which was described in [7], has become a major tool for the analysis of structuring methods and proof systems involving parallelism. The significance of CSP is in the elegance by which a few simply stated constructs (e.g., sequential and parallel composition, nondeterministic choice, concealment, and recursion) lead to a language capable of expressing the full complexity of distributed computing. The difficulty in achieving satisfactory semantic models containing these constructs has been in providing an adequate treatment of nondeterminism, deadlock, and divergence. Fortunately, as a result of an evolutionay development in [S], [lo], [15], [l], [14], [2], and [4] we now have several such models. The purpose of this paper is to report the development of the first real-time models of CSP to be compatible with the properties and proof systems of the abovementioned untimed models. Our objective in this development is the construction of a timed CSP model which satisfies the following: (1) Continuous with respect to time. The time domain should consist of all nonnegative real numbers, and there should be no lower bound on the time difference between consecutive observable events from two processes operating asynchronously in parallel. (2) Realistic. A given process should engage in only finitely many events in a bounded period of time. (3) Continuous and distributive with respect to semantic operators. All semantic operators should be continuous, and all the basic operators as defined in [2], except recursion, should distribute over nondeterministic choice. (4) Verijiable design. The model should provide a basis for the definition, specification, and verification of time critical processes with an adequate treatment of nondeterminism, which assists in avoidance of deadlock and divergence.
---
paper_title: Probabilistic Resource Failure in Real-Time Process Algebra ?

paper_content:

PACSR, a probabilistic extension of the real-time process algebra ACSR, is presented. The extension is built upon a novel treatment of the notion of a resource. In ACSR, resources are used to model contention in accessing physical devices. Here, resources are invested with the ability to fail and are associated with a probability of failure. The resulting formalism allows one to perform probabilistic analysis of real-time system specifications in the presence of resource failures. A probabilistic variant of Hennessy-Milner logic with until is presented. The logic features an until operator which is parameterized by both a probabilistic constraint and a regular expression over observable actions. This style of parameterization allows the application of probabilistic constraints to complex execution fragments. A model-checking algorithm for the proposed logic is also given. Finally, PACSR and the logic are illustrated with a telecommunications example.
---
paper_title: A Process Algebraic Approach to the Specification and Analysis of Resource-Bound Real-Time Systems

paper_content:

Recently, significant progress has been made in the development of timed process algebras for the specification and analysis of real-time systems. This paper describes a timed process algebra called ACSR, which supports synchronous timed actions and asynchronous instantaneous events. Timed actions are used to represent the usage of resources and to model the passage of time. Events are used to capture synchronization between processes. To be able to specify real systems accurately, ACSR supports a notion of priority that can be used to arbitrate among timed actions competing for the use of resources and among events that are ready for synchronization. The paper also includes a brief overview of other timed process algebras and discusses similarities and differences between them and ACSR. >
---
paper_title: Real Time Process Algebra with Infinitesimals

paper_content:

We consider a model of the real time process algebra of [1,2,3] based on the nonstandard reals. As a subalgebra, we obtain a theory in which the urgent actions of ATP, TiCCS, TeCCS can be modeled.
---
paper_title: A temporal calculus of communicating systems

paper_content:

In this paper, we introduce a calculus of communicating systems which allows for the expression and analysis of timing constraints, for example as is important for real-time processes. We present the language, along with its formal semantics, and derive algebraic laws for reasoning about processes in the language. Though the core language is simple, we show that the language has several powerful derived operators which we demonstrate to be useful in several examples.
---
paper_title: A brief history of Timed CSP

paper_content:

Abstract This paper is a comprehensive introduction to the language of Timed CSP, proposed by Reed and Roscoe (1986). A brief description of the notation is followed by a detailed survey of timed and untimed models for the language. A compositional proof system is included, together with an account of timed refinement. The paper ends with a list of the changes made to the theory in recent years, and a brief discussion of other timed process algebras.
---
paper_title: Process algebra with timing: real time and discrete time

paper_content:

Abstract We present real time and discrete time versions of ACP with absolute timing and relative timing. The starting-point is a new real time version with absolute timing, called ACPsat, featuring urgent actions and a delay operator. The discrete time versions are conservative extensions of the discrete time versions of ACP being known as ACPdat and ACPdrt. The principal version is an extension of ACPsat with integration and initial abstraction to allow for choices over an interval of time and relative timing to be expressed. Its main virtue is that it generalizes ACP without timing and most other versions of ACP with timing in a smooth and natural way. This is shown for the real time version with relative timing and the discrete time version with absolute timing.
---
paper_title: Concurrent And Real Time Systems The Csp Approach

paper_content:

Thank you very much for downloading concurrent and real time systems the csp approach. Maybe you have knowledge that, people have search hundreds times for their chosen readings like this concurrent and real time systems the csp approach, but end up in infectious downloads. Rather than enjoying a good book with a cup of coffee in the afternoon, instead they cope with some malicious virus inside their desktop computer.
---
paper_title: Modeling and verification of time dependent systems using time Petri nets

paper_content:

A description and analysis of concurrent systems, such as communication systems, whose behavior is dependent on explicit values of time is presented. An enumerative method is proposed in order to exhaustively validate the behavior of P. Merlin's time Petri net model, (1974). This method allows formal verification of time-dependent systems. It is applied to the specification and verification of the alternating bit protocol as a simple illustrative example. >
---
paper_title: Timed Petri Nets and BQOs

paper_content:

We consider (unbounded) Timed Petri Nets (TPNs) where each token is equipped with a real-valued clock representing the "age" of the token. Each arc in the net is provided with a subinterval of the natural numbers, restricting the ages of the tokens travelling the arc. We apply a methodology developed in [AN00], based on the theory of better quasi orderings (BQOs), to derive an efficient constraint system for automatic verification of safety properties for TPNs. We have implemented a prototype based on our method and applied it for verification of a parametrized version of Fischer's protocol.
---
paper_title: Application and Theory of Petri Nets

paper_content:

This book constitutes the refereed proceedings of the 33rd International Conference on Applications and Theory of Petri Nets and Concurrency, PETRI NETS 2012, held in Hamburg, Germany, in June 2012. The 18 regular papers and 3 tool papers presented were carefully reviewed and selected from 55 submissions. The book also contains 2 invited talks. All current issues on research and development in the area of Petri nets and related models of concurrent systems are addressed.
---
paper_title: Parallel program schemata

paper_content:

This paper introduces a model called the parallel program schema for the representation and study of programs containing parallel sequencing. The model is related to Ianov's program schema, but extends it, both by modelling memory structure in more detail and by admitting parallel computation. The emphasis is on decision procedures, both for traditional properties, such as equivalence, and for new properties particular to parallel computation, such as determinacy and boundedness.
---
paper_title: Performance analysis using timed Petri Nets

paper_content:

Petri Nets have been successfully used to model and evaluate the performance of distributed systems. Several researchers have extended the basic Petri Net model to include time, and have demonstrated that restricted classes of Petri Nets can be analyzed efficiently. Unfortunately, the restrictions prohibit the techniques from being applied to many interesting systems, e.g. communication protocols. This paper proposes a version of timed Petri Nets which accurately models communication protocols, and which can be analyzed using Timed Reachability Graphs. Procedures for constructing and analyzing these graphs are presented. The analysis is shown to be applicable to a larger class of Timed Petri Nets than previously thought. The model and the analysis technique are demonstrated using a simple communication protocol.
---
paper_title: A unified high-level Petri net formalism for time-critical systems

paper_content:

The authors introduce a high-level Petri net formalism-environment/relationship (ER) nets-which can be used to specify control, function, and timing issues. In particular, they discuss how time can be modeled via ER nets by providing a suitable axiomatization. They use ER nets to define a time notation that is shown to generalize most time Petri-net-based formalisms which appeared in the literature. They discuss how ER nets can be used in a specification support environment for a time-critical system and, in particular, the kind of analysis supported. >
---
paper_title: Remarks on blind and partially blind one-way multicounter machines☆

paper_content:

We consider one-way nondeterministic machines which have counters allowed to hold positive or negative integers and which accept by final state with all counters zero. Such machines are called blind if their action depends on state and input alone and not on the counter configuration. They are partially blind if they block when any counter is negative (i.e., only nonnegative counter contents are permissible) but do not know whether or not any of the counters contain zero. Blind multicounter machines are equivalent in power to the reversal bounded multicounter machines of Baker and Book [1], and for both blind and reversal bounded multicounter machines, the quasirealtime family is as powerful as the full family. The family of languages accepted by blind multicounter machines is the least intersection closed semiAFL containing {anbn|n⩾0} and also the least intersection closed semiAFL containing the two-sided Dyck set on one letter. Blind multicounter machines are strictly less powerful than quasirealtime partially blind multicounter machines. Quasirealtime partially blind multicounter machines accept the family of computation state sequences or Petri net languages which is equal to the least intersection closed semiAFL containing the one-sided Dyck set on one letter but is not a principal semiAFL. For partially blind multicounter machines, as opposed to blind machines, linear time is more powerful than quasirealtime. Assuming that the reachability problem for vector addition systems is decidable [16], partially blind multicounter machines accept only recursive sets and do not accept even {anbn|n⩾0∗, and quasirealtime partially blind multicounter machines are less powerful than general quasirealtime multicounter machines.
---
paper_title: Petri Nets For Systems Engineering: A Guide to Modeling, Verification, and Applications

paper_content:

From the Publisher: ::: Formal methods for the specification and verification of hardware and software systems are becoming more and more important as systems increase in size and complexity. The aim of the book is to illustrate progress in formal methods, based on Petri net formalisms. It contains a collection of examples arising from different fields, such as flexible manufacturing, telecommunication and workflow management systems. The book covers the main phases in the life cycle of design and implementation of a system, i.e., specification, model checking techniques for verification, analysis of properties, code generation, and execution of models. These techniques and their tool support are discussed in detail including practical issues. Amongst others, fundamental concepts such as composition, abstraction, and reusability of models, model verification, and verification of properties are systematically introduced.
---
paper_title: Checking Regular Properties of Petri Nets

paper_content:

In this paper we consider the problem of comparing an arbitrary Petri net against one whose places may contain only a bounded number of tokens (that is, against a regular behaviour), with respect to trace set inclusion and equivalence, as well as simulation and bisimulation. In contrast to the known result that language equivalence is undecidable, we find that all of the above are in fact decidable. We furthermore demonstrate that it is undecidable whether a given Petri net is either trace equivalent or simulation equivalent to any (unspecified) bounded net.
---
paper_title: On the reachability problem for 5-dimensional vector addition systems

paper_content:

The reachability set for vector addition systems of dimension less than or equal to five are shown to be effectively computable semilinear sets. Thus reachability, equvalence and containment are decidable up to dimension 5. An example of a non-semilinear reachability set is given for dimension 6. Keywords and phrases: Vector addition system, Petri net, semilinear set, algorithms, decidability.
---
paper_title: Time-Based Expressivity of Time Petri Nets for System Specification

paper_content:

Various models of time Petri Nets have been successfully used to adequately specify time-critical systems. For such systems correctness depends not only on the actions that are performed, but also on the times when they are performed. Therefore, the semantics must take explicitly into account the timings of actions, and also concepts of time-based expressivity are needed to compare the expressive power of the various models. In the paper we introduce a general framework that includes many Petri net models, present in the literature, which differ from one another with respect to timing location, timing strength and time domain. Then we introduce an operational semantics that takes into account both sequentialization and timing of actions. When abstracting time away we reobtain previously reported results, which are useful when one is interested in modelling systems that are not time-critical. On the other hand, when abstracting the sequentialization of actions away we define a new kind of expressivity in terms of which we compare the various models we have considered.
---
paper_title: Recoverability of Communication Protocols--Implications of a Theoretical Study

paper_content:

A study is presented which permits the formal analysis and synthesis of recoverable computer communication protocols. This study is based on a formal representation of processes by a model of computation, the Petri nets (PN's). The PN model is generalized to include a representation of the possible failures, and then, the concept of "recoverability" is formally defined. A set of necessary and sufficient conditions which a process must satisfy in order to be recoverable is derived. In the PN model, the processes that satisfy these conditions are shown to have some practical limitations. A new model, the time-Petri net (TPN), is introduced to remove these limitations. This new model allows the introduction of constraints in the execution times of its part. As shown in this paper, the TPN appears to be a suitable model for the study of practical recoverable processes. Several practical communication protocols are formally designed and analyzed using this new model, and some interesting properties of these protocols are formally derived.
---
paper_title: A Compositional Real-time Semantics of STATEMATE Designs

paper_content:

This paper presents a reference semantics for a verication tool currently under development allowing to verify temporal properties of embedded control sys- tems modelled using the StateMate system. The semantics reported divert from others reported in the literature [24] by faithfully modelling the semantics as supported in the StateMate simulation tool. It divers from the recent paper by Harel and Naamad [8] by providing a compositional semantics, a prerequisite for the support of compositional verication methods, and by the degree of math- ematical rigour. We use a variant of synchronous transition systems introduced by Manna and Pnueli [18] as base model for our semantics.
---
paper_title: Model Checking and Modular Verification

paper_content:

We describe a framework for compositional verification of finite state processes. The framework is based on two ideas: a subset of the logic CTL for which satisfaction is preserved under composition; and a preorder on structures which captures the relation between a component and a system containing the component. Satisfaction of a formula in the logic corresponds to being below a particular structure (a tableau for the formula) in the preorder. We show how to do assume-guarantee style reasoning within this framework. In addition, we demonstrate efficient methods for model checking in the logic and for checking the preorder in several special cases. We have implemented a system based on these methods, and we use it to give a compositional verification of a CPU controller.
---
paper_title: A Proof Technique for Rely/Guarantee Properties

paper_content:

A rely/guarantee specification for a program P is a specification of the form R ⊃ G (R implies G), where R is a rely condition and G is a guarantee condition. A rely condition expresses the conditions that P relies on its environment to provide, and a guarantee condition expresses what P guarantees to provide in return. This paper presents a proof technique that permits us to infer that a program P satisfies a rely/guarantee specification R ⊃ G, given that we know P satisfies a finite collection of rely/guarantee specifications R i ⊃ G i , (i ∈ I). The utility of the proof technique is illustrated by using it to derive global liveness properties of a system of concurrent processes from a collection of local liveness properties satisfied by the component processes. The use of the proof rule as a design principle is also considered.
---
paper_title: Safety analysis of timing properties in real-time systems

paper_content:

The authors formalize the safety analysis of timing properties in real-time systems. The analysis is based on a formal logic, RTL (real-time logic), which is especially suitable for reasoning about the timing behavior of systems. Given the formal specification of a system and a safety assertion to be analyzed, the goal is to relate the safety assertion to the systems specification. There are three distinct cases: (1) the safety assertion is a theorem derivable from the systems specification; (2) the safety assertion is unsatisfiable with respect to the systems specification; or (3) the negation of the safety assertion is satisfiable under certain conditions. A systematic method for performing safety analysis is presented.
---
paper_title: Modular refinement of hierarchic reactive machines

paper_content:

Scalable formal analysis of reactive programs demands integration of modular reasoning techniques with existing analysis tools. Principles such as abstraction, compositional refinement, and assume-guarantee reasoning are well understood for architectural hierarchy that describes the communication structure between component processes, and have been shown to be useful. In this paper, we develop the theory of modular reasoning for behavior hierarchy that describes control structure using hierarchic modes. From STATECHARTS to UML, behavior hierarchy has been an integral component of many software design languages, but only syntactically. We present the hierarchic reactive modules language that retains powerful features such as nested modes, mode reuse, exceptions, group transitions, history, and conjunctive modes, and yet has a semantic notion of mode hierarchy. We present an observational trace semantics for modes that provides the basis for mode refinement. We show the refinement to be compositional with respect to the mode constructors, and develop an assume-guarantee reasoning principle.
---
paper_title: Model Checking Timed UML State Machines and Collaborations

paper_content:

We describe a prototype tool, HUGO/RT, that is designed to automatically verify whether the timed state machines in a UML model interact according to scenarios specified by time-annotated UML collaborations. Timed state machines are compiled into timed automata that exchange signals and operations via a network automaton. A collaboration with time constraints is translated into an observer timed automaton. The model checker UPPAAL is called upon to verify the timed automata representing the model against the observer timed automaton.
---
paper_title: Conjoining Specifications

paper_content:

We show how to specify components of concurrent systems. The specification of a system is the conjunction of its components' specifications. Properties of the system are proved by reasoning about its components. We consider both the decomposition of a given system into parts, and the composition of given parts to form a system.
---
paper_title: A Compositional Rule for Hardware Design Refinement

paper_content:

We present an approach to designing verified digital systems by a sequence of small local refinements. Refinements in this approach are not limited to a library of predefined transformations for which theorems have been previously established. Rather, the approach relies on localizing the refinement steps in such a way that they can be verified efficiently by model checking. Toward this end, a compositional rule is proposed by which each design refinement may be verified independently, in an abstract environment. This rule supports the use of downward refinement maps, which translate abstract behavior detailed behavior. These maps may involve temporal transformations, including delay. The approach is supported by a verification tool based on symbolic model checking.
---
paper_title: Modechart: a specification language for real-time systems

paper_content:

Present a specification language for real-time systems called Modechart. The semantics of Modechart is given in terms of real-time logic (RTL), which is especially amenable to reasoning about the absolute (real-time clock) timing of events. The semantics of Modechart has an important property that the translation of a Modechart specification into RTL formulas results in a hierarchical organization of the resulting RTL assertions. This gives us significant leverage in reasoning about properties of a system by allowing us to filter out assertions that concern lower levels of abstraction. Some results about desirable properties of Modechart specifications are given. A graphical implementation of Modechart has been completed. >
---
paper_title: Real-time reactive system development: a formal approach based on uml and pvs

paper_content:

The notion of real-time reactive behavior encompasses concurrency, communication through sensors and actuators, and relations between input and output over time. Real-time reactive systems are inherently complex, and often used in safety-critical contexts. Application domains include control systems for nuclear reactors, air traffic, railroad crossing, telecommunications, and medical devices. Applying formal methods in the development process is seen as a means for dealing with the complexity, and for quality assurance. One of the goals is to formally verify time-dependent safety properties in the design. The scope of this thesis encompasses three major components. We develop a visual technique for object-oriented modeling of real-time reactive systems, based on a minimal set of extensions to UML, along with a set of well-formedness rules for the real-time models. We then present a formalization of the Real-Time rules of UML metamodel, and provide formal denotational and operational semantics for RTUML. Finally, we introduce a methodology for mechanized verification of time-dependent properties in the RTUML design of real-time reactive systems, within the PVS verification environment. The formal semantics of RTUML provides a foundation for the verification methodology, and for rigorous analysis and validation techniques. The novelty of the development methodology for real-time systems lies in the mechanized verification approach superimposed on the object-oriented modeling technique.
---
paper_title: Hierarchical modeling and analysis of embedded systems

paper_content:

This paper describes the modeling language CHARON for modular design of interacting hybrid systems. The language allows specification of architectural as well as behavioral hierarchy and discrete as well as continuous activities. The modular structure of the language is not merely syntactic, but is exploited by analysis tools and is supported by a formal semantics with an accompanying compositional theory of refinement. We illustrate the benefits of CHARON in the design of embedded control software using examples from automated highways concerning vehicle coordination.
---
paper_title: Timed Sequence Diagrams and Tool-Based Analysis - A Case Study

paper_content:

We use UML timed Sequence Diagrams to specify the realtime behaviour of a communication protocol of audio/video components. The Sequence Diagrams build the requirements specification against which an implementation of the protocol developed by the Bang & Olufsen company is proven correct. ::: ::: To obtain a complete requirements specification, we have to mark the UML Sequence Diagrams as optional or mandatory behaviour. Then the Sequence Diagram interactions with their timing constraints and periods are transferred to a setting of timed automata. We use the Uppaal tool for verification. In particular, we show that the implementation of the protocol conforms to the Sequence Diagram specification concerning the correct data transfer on the bus.
---
paper_title: A really temporal logic

paper_content:

A real-time temporal logic for the specification of reactive systems is introduced. The novel feature of the logic, TPTL, is the adoption of temporal operators as quantifiers over time variables; every modality binds a variable to the time(s) it refers to. TPTL is demonstrated to be both a natural specification language and a suitable formalism for verification and synthesis. A tableau-based decision procedure and model-checking algorithm for TPTL are presented. Several generalizations of TPTL are shown to be highly undecidable. >
---
paper_title: Real-time logics: complexity and expressiveness

paper_content:

A unifying framework for the study of real-time logics is developed. In analogy to the untimed case, the underlying classical theory of timed state sequences is identified, it is shown to be nonelementarily decidable, and its complexity and expressiveness are used as a point of reference. Two orthogonal extensions of PTL (timed propositional temporal logic and metric temporal logic) that inherit its appeal are defined: they capture elementary, yet expressively complete, fragments of the theory of timed state sequences, and thus are excellent candidates for practical real-time specification languages. >
---
paper_title: DESIGN AND SYNTHESIS OF SYNCHRONIZATION SKELETONS USING BRANCHING TIME TEMPORAL LOGIC

paper_content:

We Propose a method of constructing concurrent programs in which the synchronization skeletonof the program is automatically synthesized from a high-level (branching time) Temporal Logic specification. The synchronization skeleton is an abstraction of the actual program where detail irrelevant to synchronization is suppressed. For example, in the synchronization skeleton for a solution to the critical section problem each process's critical section may be viewed as a single node since the internal structure of the critical section is unimportant. Most solutions to synchronization problems in the literature are in fact given as synchronization skeletons. Because synchronization skeletons are in general finite state, the propositional version of Temporal Logic can be used to specify their properties.
---
paper_title: Symbolic Model Checking for Real-Time Systems

paper_content:

Abstract We describe finite-state programs over real-numbered time in a guarded-command language with real-valued clocks or, equivalently, as finite automata with real-valued clocks. Model checking answers the question which states of a real-time program satisfy a branching-time specification (given in an extension of CTL with clock variables). We develop an algorithm that computes this set of states symbolically as a fixpoint of a functional on state predicates, without constructing the state space. For this purpose, we introduce a μ-calculus on computation trees over real-numbered time. Unfortunately, many standard program properties, such as response for all nonzeno execution sequences (during which time diverges), cannot be characterized by fixpoints: we show that the expressiveness of the timed μ-calculus is incomparable to the expressiveness of timed CTL. Fortunately, this result does not impair the symbolic verification of "implementable" real-time programs-those whose safety constraints are machine-closed with respect to diverging time and whose fairness constraints are restricted to finite upper bounds on clock values. All timed CTL properties of such programs are shown to be computable as finitely approximable fixpoints in a simple decidable theory.
---
paper_title: A really temporal logic

paper_content:

A real-time temporal logic for the specification of reactive systems is introduced. The novel feature of the logic, TPTL, is the adoption of temporal operators as quantifiers over time variables; every modality binds a variable to the time(s) it refers to. TPTL is demonstrated to be both a natural specification language and a suitable formalism for verification and synthesis. A tableau-based decision procedure and model-checking algorithm for TPTL are presented. Several generalizations of TPTL are shown to be highly undecidable. >
---
paper_title: Real-time logics: complexity and expressiveness

paper_content:

A unifying framework for the study of real-time logics is developed. In analogy to the untimed case, the underlying classical theory of timed state sequences is identified, it is shown to be nonelementarily decidable, and its complexity and expressiveness are used as a point of reference. Two orthogonal extensions of PTL (timed propositional temporal logic and metric temporal logic) that inherit its appeal are defined: they capture elementary, yet expressively complete, fragments of the theory of timed state sequences, and thus are excellent candidates for practical real-time specification languages. >
---
paper_title: Automatic verification of finite-state concurrent systems using temporal logic specifications

paper_content:

We give an efficient procedure for verifying that a finite-state concurrent system meets a specification expressed in a (propositional, branching-time) temporal logic. Our algorithm has complexity linear in both the size of the specification and the size of the global state graph for the concurrent system. We also show how this approach can be adapted to handle fairness. We argue that our technique can provide a practical alternative to manual proof construction or use of a mechanical theorem prover for verifying many finite-state concurrent systems. Experimental results show that state machines with several hundred states can be checked in a matter of seconds.
---
paper_title: Timed I/O automata: a mathematical framework for modeling and analyzing real-time systems

paper_content:

We describe the timed input/output automata (TIOA) framework, a general mathematical framework for modeling and analyzing real-time systems. It is based on timed I/O automata, which engage in both discrete transitions and continuous trajectories. The framework includes a notion of external behavior, and notions of composition and abstraction. We define safety and liveness properties for timed I/O automata, and a notion of receptiveness, and prove basic results about all of these notions. The TIOA framework is defined as a special case of the new hybrid I/O automata (HIOA) modeling framework for hybrid systems. Specifically, a TIOA is an HIOA with no external variables; thus, TIOAs communicate via shared discrete actions only, and do not interact continuously. This restriction is consistent with previous real-time system models, and gives rise to some simplifications in the theory (compared to HIOA). The resulting model is expressive enough to describe complex timing behavior, and to express the important ideas of previous timed automata frameworks.
---
paper_title: Decidability of Strong Bisimilarity for Timed BPP

paper_content:

We investigate a timed extension of the class of Basic Parallel Processes (BPP), in which actions are durational and urgent and parallel components have independent local clocks. The main result is decidability of strong bisimilarity, known also as performance equivalence, in this class. This extends the earlier decidability result for plain BPP [8] as well as decidability for timed BPP with strictly positive durations of actions [3]. Both ill-timed and well-timed semantics are treated. Our decision procedure is based on decidability of the validity problem for Presburger arithmetic.
---
paper_title: Model Reduction of Discrete Real-Time Systems

paper_content:

In many Discrete-Event Systems (DES) both state and event information are of importance to the systems designer. To obtain compositionally consistent hierarchical models of systems, the behavior of Discrete-Event Systems with unobservable transitions and state output maps is considered. Observers for deterministic DES are generalized to nondeterministic DES and characterized using the join semilattice of compatible partitions of a transition system. This characterization points to efficient algorithms for computing both strong and weak state-event observers as solutions to the Relational Coarsest Partition problem (RCP). The strong and weak observation equivalences of Milner are shown to be special cases of our observers under the trivial (constant) state output map. The state-event equivalence based upon the observers is shown to be a congruence for a parallel composition operator, allowing the replacement of modules by their quotient systems. Logics such as Ostroff’s RTTL allow for the specification and verification of a system’s state-event behavior. To make realistic problems amenable to analysis, a designer must typically decompose the system into subsystems (modules) and use algebraic abstraction (quotient systems) to obtain hierarchical system models that preserve the properties to be verified. In this thesis we use state-event observational equivalence to perform compositionally consistent model reduction for a subclass of formulas of state-event linear temporal logics, with particular attention to a discrete time temporal logic that is a simplification of RTTL. The reduction technique allows limited use of immediate operators. In the process, we develop a method of specifying modules’ input/output behavior by defining observable satisfaction for RTTL-style temporal logics. The results are applied to the shut-down system of a nuclear reactor.
---
paper_title: Forward and Backward Simulations Part II: Timing-Based Systems

paper_content:

A general automaton model for timing-based systems is presented and is used as the context for developing a variety of simulation proof techniques for such systems. As a first step, a comprehensive overview of simulation techniques for simple untimed automata is given. In particular, soundness and completeness results for (1) refinements, (2) forward and backward simulations, (3) forward-backward and backward-forward simulations, and (4) history and prophecy relations are given. History and prophecy relations are new and are abstractions of the history variables of Owicki and Gries and the prophecy variables of Abadi and Lamport, respectively. As a subsequent step, it is shown how most of the results for untimed automata can be carried over to the setting of timed automata. In fact many of the results for the timed case are obtained as consequences of the analogous results for the untimed case.
---
paper_title: The generalized railroad crossing: a case study in formal verification of real-time systems

paper_content:

A new solution to the generalized railroad crossing problem, based on timed automata, invariants and simulation mappings, is presented and evaluated. The solution shows formally the correspondence between four system descriptions: an axiomatic specification, an operational specification, a discrete system implementation, and a system implementation that works with a continuous gate model. >
---
paper_title: Verifying timing properties of concurrent algorithms

paper_content:

This paper presents a method for computer-aided verification of timing properties of real-time systems. A timed automaton model, along with invariant assertion and simulation techniques for proving properties of real-time systems, is formalized within the Larch Shared Language. This framework is then used to prove time bounds for two sample algorithms—a simple counter and Fischer’s mutual exclusion protocol. The proofs are checked using the Larch Prover.
---
paper_title: Verification of an Audio Control Protocol

paper_content:

We analyze a simple version of a protocol developed by Philips for the physical layer of an interface bus that connects the various devices of some stereo equipment (tuner, CD player,...). The protocol, which uses Manchester encoding, has to deal with a significant uncertainty in the timing of events, due to both hardware and software constraints. We present a formal specification of the protocol, and a proof of correctness for the case where the tolerance of the clocks used within the system is less than 1/17. A counterexample shows that the protocol fails for tolerances greater than or equal to this value. The verification is carried out using a model of linear hybrid systems, which is similar to the phase transition system model of Manna and Pnueli, and the model of linear hybrid automata of Alur, Henzinger and Ho. The semantics of linear hybrid systems is defined via a translation to the timed I/O automata model of Lynch and Vaandrager.
---
paper_title: Symbolic Simulation of Industrial Real-Time and Embedded Systems-Experiments with the Bluetooth Baseband Communication Protocol

paper_content:

We introduce the symbolic simulation function implemented in our model-checker/simulator RED 4.0 for dense-time concurrent systems. By representing and manipulating state-spaces as logic predicates, the technique of symbolic simulation can lead to high performance by encoding even a dense amount of traces in traditional simulation into one symbolic trace. Symbolic simulation adds the dimension of width to a trace of state-spaces. By controlling the width of traces, we have a much better chance to find bugs using fewer traces. ::: ::: Our main contribution is the design of symbolic simulation function in RED 4.0 for dense-time concurrent systems. In our tool, users can strongly control the width of traces and the generation of traces. We discuss how to generate traces using various policies, how to manipulate the state-predicate, and how to manage the trace trees. Moreover, we design a C-like language whose programs can be mechanically translated into the optimized communicating timed automata(CTA). Engineers can also put down comment-line assertions as specifications in their verification tasks. Finally, experiments using our simulator to verify the Bluetooth baseband protocol justify the usefulness of our tool. The tool is available at http://cc.ee.ntu.edu.tw/~farn/.
---
paper_title: Hierarchical modeling and analysis of embedded systems

paper_content:

This paper describes the modeling language CHARON for modular design of interacting hybrid systems. The language allows specification of architectural as well as behavioral hierarchy and discrete as well as continuous activities. The modular structure of the language is not merely syntactic, but is exploited by analysis tools and is supported by a formal semantics with an accompanying compositional theory of refinement. We illustrate the benefits of CHARON in the design of embedded control software using examples from automated highways concerning vehicle coordination.
---
paper_title: Forward and Backward Simulations for Timing-Based Systems

paper_content:

A general automaton model for timing-based systems is presented and is used as the context for developing a variety of simulation proof techniques for such systems. These techniques include (1) refinements, (2) forward and backward simulations, (3) hybrid forward?backward and backward?forward simulations, and (4) history and prophecy relations. Relationships between the different types of simulations, as well as soundness and completeness results, are stated and proved. These results are (with one exception) analogous to the results for untimed systems in Part I of this paper. In fact, many of the results for the timed case are obtained as consequences of the analogous results for the untimed case.
---
paper_title: MT: A toolset for specifying and analyzing real-time systems

paper_content:

This paper introduces MT, a collection of integrated tools for specifying and analyzing real-time systems using the Modechart language. The toolset includes facilities for creating and editing Modechart specifications. Users may symbolically execute the specifications with an automatic simulation tool to make sure that the specified behavior is what was intended. They may also invoke a verifier that uses model-checking to determine whether the specifications imply (satisfy) any of a broad class of safety assertions. To illustrate the toolset's capabilities as well as several issues that arise when formal methods are applied to real-world systems, the paper includes specifications and analysis procedures for a software component taken from an actual Naval real-time system. >
---
paper_title: Decidability of Bisimulation Equivalences for Parallel Timer Processes

paper_content:

In this paper an abstract model of parallel timer processes (PTPs), allowing specification of temporal quantitative constraints on the behaviour of real time systems, is introduced. The parallel timer processes are defined in a dense time domain and are able to model both concurrent (with delay intervals overlapping on the time axis) and infinite behaviour. Both the strong and weak (abstracted from internal actions) bisimulation equivalence problems for PTPs are proved decidable. It is proved also that, if one provides the PTP model additionally with memory cells for moving timer value information along the time axis, the bisimulation equivalence (and even the vertex reachability) problems become undecidable.
---
paper_title: Simplification by Cooperating Decision Procedures

paper_content:

A method for combining decision procedures for several theories into a single decision procedure for their combination is described, and a simplifier based on this method is discussed. The simplifier finds a normal form for any expression formed from individual variables, the usual Boolean connectives, the equality predicate =, the conditional function if-then-else, the integers, the arithmetic functions and predicates +, -, and ≤, the Lisp functions and predicates car, cdr, cons, and atom, the functions store and select for storing into and selecting from arrays, and uninterpreted function symbols. If the expression is a theorem it is simplified to the constant true, so the simplifier can be used as a decision procedure for the quantifier-free theory containing these functions and predicates. The simplifier is currently used in the Stanford Pascal Verifier.
---
paper_title: TAME: A specialized specification and verification system for timed automata

paper_content:

Abstract : Assuring the correctness of specifications of real-time systems can involve significant human effort. The use of a mechanical theorem prover to encode such specifications and to verify their properties could significantly reduce this effort. A barrier to routinely encoding and mechanically verifying specifications has been the need first to master the specification language and logic of a general theorem proving system. Our approach to overcoming this barrier is to provide mechanical support for producing specifications and verifying proofs, specialized for particular mathematical models and proof techniques. We are currently developing a mechanical verification system called TAME (Timed Automata Modeling Environment) that provides this specialized support using SRI's Prototype Verification System (PVS). Our system is intended to permit steps in reasoning similar to those in hand proofs that use model-specific techniques. TAME has recently been used to detect errors in a realistic example.
---
paper_title: Compositional Verification of Real-Time Applications

paper_content:

To support top-down design of distributed real-time systems, a framework of mixed terms has been incorporated in the verification system PVS. Programs and assertional specifications are treated in a uniform way. We focus on the timed behaviour of parallel composition and hiding, presenting several alternatives for the definition of a denotational semantics. This forms the basis of compositional proof rules for parallel composition and hiding. The formalism is applied to an example of a hybrid system, which also serves to illustrate our ideas on platform-independent programming.
---
paper_title: Symbolic Logic and Mechanical Theorem Proving

paper_content:

This book contains an introduction to symbolic logic and a thorough discussion of mechanical theorem proving its applications. The book consists of three major parts. Chapters 2 and 3 constitute an introduction to symbolic logic. Chapters 4-9 introduce several techniques in mechanical theorem proving, and Chapters 10 an 11 show how theorem proving can be applied to various areas such as question answering, problem solving, program analysis, and program synthesis.
---
paper_title: Counter-example guided predicate abstraction of hybrid systems

paper_content:

Predicate abstraction has emerged to be a powerful technique for extracting finite-state models from infinite-state systems, and has been recently shown to enhance the effectiveness of the reachability computation techniques for hybrid systems. Given a hybrid system with linear dynamics and a set of linear predicates, the verifier performs an on-the-fly search of the finite discrete quotient whose states correspond to the truth assignments to the input predicates. The success of this approach depends on the choice of the predicates used for abstraction. In this paper, we focus on identifying these predicates automatically by analyzing spurious counter-examples generated by the search in the abstract state-space. We present the basic techniques for discovering new predicates that will rule out closely related spurious counter-examples, optimizations of these techniques, implementation of these in the verification tool, and case studies demonstrating the promise of the approach.
---
paper_title: Deciding Linear Inequalities by Computing Loop Residues

paper_content:

V R Pratt has shown that the real and integer feastbdlty of sets of linear mequallUes of the form x _< y + c can be decided quickly by examining the loops m certain graphs Pratt's method is generahzed, first to real feaslbdlty of mequahues m two variables and arbitrary coefficients, and ultimately to real feaslbdlty of arbitrary sets of hnear mequahtles The method is well suited to apphcatlons m program verification
---
paper_title: TAME: Using PVS strategies for special-purpose theorem proving

paper_content:

TAME (Timed Automata Modeling Environment), an interface to the theorem proving system PVS, is designed for proving properties of three classes of automata: I/O automata, Lynch–Vaandrager timed automata, and SCR automata. TAME provides templates for specifying these automata, a set of auxiliary theories, and a set of specialized PVS strategies that rely on these theories and on the structure of automata defined using the templates. Use of the TAME strategies simplifies the process of proving automaton properties, particularly state and transition invariants. TAME provides two types of strategies: strategies for “automatic” proof and strategies designed to implement “natural” proof steps, i.e., proof steps that mimic the high-level steps in typical natural language proofs. TAME's “natural” proof steps can be used both to mechanically check hand proofs in a straightforward way and to create proof scripts that can be understood without executing them in the PVS proof checker. Several new PVS features can be used to obtain better control and efficiency in user-defined strategies such as those used in TAME. This paper describes the TAME strategies, their use, and how their implementation exploits the structure of specifications and various PVS features. It also describes several features, currently unsupported in PVS, that would either allow additional “natural” proof steps in TAME or allow existing TAME proof steps to be improved. Lessons learned from TAME relevant to the development of similar specialized interfaces to PVS or other theorem provers are discussed.
---
paper_title: Transformational design of real-time systems Part I: From requirements to program specifications

paper_content:

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.
---
paper_title: The Tool KRONOS

paper_content:

Both approaches presented in this paper considerably improve Kronos performance and functionalities.
---
paper_title: UPPAAL - a Tool Suite for Automatic Verification of Real-Time Systems

paper_content:

Uppaal is a tool suite for automatic verification of safety and bounded liveness properties of real-time systems modeled as networks of timed automata. It includes: a graphical interface that supports graphical and textual representations of networks of timed automata, and automatic transformation from graphical representations to textual format, a compiler that transforms a certain class of linear hybrid systems to networks of timed automata, and a model-checker which is implemented based on constraint-solving techniques. Uppaal also supports diagnostic model-checking providing diagnostic information in case verification of a particular real-time systems fails.
---
paper_title: Timing Assumptions and Verification of Finite-State Concurrent Systems

paper_content:

We have described a scheme that allows timing assumptions to be incorporated into automatic proofs of arbitrary finite-state temporal properties. The obvious extension is to be able to prove timing properties, not just assume them. This would provide a verification framework for finite-state hard real-time systems. We conjecture that the method presented can, in fact, be extended in this way.
---
paper_title: Symbolic Techniques for Parametric Reasoning about Counter and Clock Systems

paper_content:

We address the problem of automatic analysis of parametric counter and clock automata. We propose a semi-algorithmic approach based on using (1) expressive symbolic representation structures called Parametric DBM's and (2) accurate extrapolation techniques allowing to speed up the reachability analysis and help its termination. The techniques we propose consist in guessing automatically the effect of iterating a control loop an arbitray number of times, and in checking that this guess is exact. Our approach can deal uniformly with systems that generate linear or nonlinear sets of configurations. We have implemented our techniques and experimented them on nontrivial examples such as a parametric timed version of the Bounded Retransmission Protocol.
---
paper_title: Efficient Data Structure for Fully Symbolic Verification of Real-Time Software Systems

paper_content:

A new data-structure called RED (Re gion-Encoding Diagram) for the fully symbolic model-checking of real-time software systems is proposed. RED is a BDD-like data-structure for the encoding of regions. Unlike DBM which records differences between pairs of clock readings, RED only uses one auxiliary binary variable for each clock. Thus the number of variables used in RED is always linear to the number of clocks declared in the input system description. Experiment has been carried out to compare RED with previous technologies.
---
paper_title: Timed Petri Nets and BQOs

paper_content:

We consider (unbounded) Timed Petri Nets (TPNs) where each token is equipped with a real-valued clock representing the "age" of the token. Each arc in the net is provided with a subinterval of the natural numbers, restricting the ages of the tokens travelling the arc. We apply a methodology developed in [AN00], based on the theory of better quasi orderings (BQOs), to derive an efficient constraint system for automatic verification of safety properties for TPNs. We have implemented a prototype based on our method and applied it for verification of a parametrized version of Fischer's protocol.
---
paper_title: Difference Decision Diagrams

paper_content:

This paper describes a newdata structure, difference decision diagrams (DDDs), for representing a Boolean logic over inequalities of the form x-y ≤ c where the variables are integer or real-valued.We give algorithms for manipulating DDDs and for determining validity, satisfiability, and equivalence. DDDs enable an efficient verification of timed systems modeled as, for example, timed automata or timed Petri nets, since both the states and their associated timing information are represented symbolically, similar to how BDDs represent Boolean predicates. We demonstrate the efficiency of DDDs by analyzing a timed system and compare the results with the tools KRONOS and UPPAAL.
---
paper_title: Fully Symbolic Model Checking of Timed Systems using Difference Decision Diagrams

paper_content:

Abstract Current approaches for analyzing timed systems are based on an explicit enumeration of the discrete states and thus these techniques are only capable of analyzing systems with a handful of timers and a few thousand states. We address this limitation by describing how to analyze a timed system fully symbolically, i.e., by representing sets of discrete states and their associated timing information implicitly. We demonstrate the efficiency of the symbolic technique by computing the set of reachable states for a non-trivial timed system and compare the results with the state-of-the-art tools Kronos and Uppaal . With an implementation based on difference decision diagrams, the runtimes are several orders of magnitudes better. The key operation in obtaining these results is the ability to advance time symbolically. We show how to do this efficiently by essentially quantifying out a special variable z which is used to represent the constant zero. The symbolic manipulations given in this paper are sufficient to verify TCTL-formulae fully symbolically.
---
paper_title: Efficient Timed Reachability Analysis using Clock Difference Diagrams

paper_content:

One of the major problems in applying automatic verication tools to industrial-size systems is the excessive amount of memory required during the state-space exploration of a model. In the setting of real-time, this problem of state-explosion requires extra attention as information must be kept not only on the discrete control structure but also on the values of continuous clock variables. In this paper, we present Clock Dierence Diagrams, CDD's, a BDD-like data-structure for representing and eectively manipulating certain non-convex subsets of the Euclidean space, notably those encountered during verication of timed automata. A version of the real-time verication tool Uppaal using CDD's as a compact datastructure for storing explored symbolic states has been implemented. Our experimental results demonstrate signicant space-savings: for 8 industrial examples, the savings are between 46% and 99% with moderate increase in runtime. We further report on how the symbolic state-space exploration itself may be carried out using CDD's.
---
paper_title: Region Encoding Diagram for fully symbolic verification of real-time systems

paper_content:

RED (Region Encoding Diagram), first reported by F.Wang (2000), is a BDD-like data structure for fully symbolic verification of symmetric real time systems with single clock per process. We propose to extend RED for asymmetric real time systems with an unrestricted number of global or local clocks. Unlike in DBM which records differences between pairs of clock readings, we record the ordering among fractional parts of clock readings into integer sequences encoded in RED's. Like BDD, the new RED is also a minimal canonical form for its target system state-space representations. The number of variables used in RED is O(|X|log|X|) where X is the clock set in the input system description. Experimentation has been carried out to compare RED's performance with the tools: UPPAAL2K and Kronos. Accordingly, we found out that RED is the most efficient real time system safety analyzer as long as concurrency complexity is considered.
---
paper_title: Symbolic Verification of Complex Real-Time Systems with Clock-Restriction Diagram

paper_content:

Real-world real-time systems may involve many complex structures, which are difficult to verify. We experiment with the model-checking of an application-layer html-based web-camera which involves structures like event queues, high-layer communication channels, and time-outs. To contain the complexity, we implement our verification tool with a newly developed BDD-like data-structure, reduced CRD (Clock-Restriction Diagram), which has enhanced the verification performance through intensive data-sharing in a previous report. However, the representation of reduced CRD does not allow for quick test of zone containment. To this purpose, we thus have designed a new CRD-based representation, cascade CRD, which has given us enough performance enhancement to successfully verifying several implementations of the web-camera.
---
paper_title: Approximate reachability analysis of timed automata

paper_content:

A promising approach to formal verification of real-time systems is to use timed automata to model systems, and then to check whether certain "unsafe" states are reachable. Although theoretically appealing, this approach has significant practical problems because it requires expensive computation of reachable states. Fortunately computing a superset of reachable states is sometimes much cheaper. Replacing the set of reachable states with its superset is a conservative approximation, in the sense that it can occasionally cause a correct system to be declared incorrect, but can never cause an incorrect system to be declared correct. We propose two algorithms for computing a superset of reachable states of a timed automaton. Both algorithms involve only manipulation of Boolean functions, which are used to represent both sets of discrete state components and timing information. The algorithms offer different trade-offs between accuracy of approximation and efficiency of computation. Initial experimental results show that they are competitive with the best published results, but that further improvements are necessary to scale up to realistic systems.
---
paper_title: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints

paper_content:

A program denotes computations in some universe of objects. Abstract interpretation of programs consists in using that denotation to describe computations in another universe of abstract objects, so that the results of abstract execution give some information on the actual computations. An intuitive example (which we borrow from Sintzoff [72]) is the rule of signs. The text -1515 * 17 may be understood to denote computations on the abstract universe {(+), (-), (±)} where the semantics of arithmetic operators is defined by the rule of signs. The abstract execution -1515 * 17 → -(+) * (+) → (-) * (+) → (-), proves that -1515 * 17 is a negative number. Abstract interpretation is concerned by a particular underlying structure of the usual universe of computations (the sign, in our example). It gives a summary of some facets of the actual executions of a program. In general this summary is simple to obtain but inaccurate (e.g. -1515 + 17 → -(+) + (+) → (-) + (+) → (±)). Despite its fundamentally incomplete results abstract interpretation allows the programmer or the compiler to answer questions which do not need full knowledge of program executions or which tolerate an imprecise answer, (e.g. partial correctness proofs of programs ignoring the termination problems, type checking, program optimizations which are not carried in the absence of certainty about their feasibility, …).
---
paper_title: The Algorithmic Analysis of Hybrid Systems

paper_content:

We present a general framework for the formal specification and algorithmic analysis of hybrid systems. A hybrid system consists of a discrete program with an analog environment. We model hybrid systems as finite automata equipped with variables that evolve continuously with time according to dynamical laws. For verification purposes, we restrict ourselves to linear hybrid systems, where all variables follow piecewise-linear trajectories. We provide decidability and undecidability results for classes of linear hybrid systems, and we show that standard program-analysis techniques can be adapted to linear hybrid systems. In particular, we consider symbolic model-checking and minimization procedures that are based on the reachability analysis of an infinite state space. The procedures iteratively compute state sets that are definable as unions of convex polyhedra in multidimensional real space. We also present approximation techniques for dealing with systems for which the iterative procedures do not converge.
---
paper_title: An interleaving model for real-time

paper_content:

Real-time is incorporated into the interleaving model, which is used for the practical specification and verification of many properties of concurrent systems, by defining the abstract notion of a real-time transition system as a conservative extension of traditional transition systems. Qualitative fairness requirements are replaced (and superseded) by quantitative lower-bound and upper-bound real-time requirements for transitions. Proof rules are presented and used to establish lower and upper real-time bounds for response properties of real-time transition systems. This proof system can be used to verify bounded-invariance and bounded-response properties, such as timely termination of shared-variables multiprocessing systems whose semantics is defined in terms of real-time transition systems. >
---
paper_title: Symbolic Model Checking for Real-Time Systems

paper_content:

Abstract We describe finite-state programs over real-numbered time in a guarded-command language with real-valued clocks or, equivalently, as finite automata with real-valued clocks. Model checking answers the question which states of a real-time program satisfy a branching-time specification (given in an extension of CTL with clock variables). We develop an algorithm that computes this set of states symbolically as a fixpoint of a functional on state predicates, without constructing the state space. For this purpose, we introduce a μ-calculus on computation trees over real-numbered time. Unfortunately, many standard program properties, such as response for all nonzeno execution sequences (during which time diverges), cannot be characterized by fixpoints: we show that the expressiveness of the timed μ-calculus is incomparable to the expressiveness of timed CTL. Fortunately, this result does not impair the symbolic verification of "implementable" real-time programs-those whose safety constraints are machine-closed with respect to diverging time and whose fairness constraints are restricted to finite upper bounds on clock values. All timed CTL properties of such programs are shown to be computable as finitely approximable fixpoints in a simple decidable theory.
---
paper_title: Timing Assumptions and Verification of Finite-State Concurrent Systems

paper_content:

We have described a scheme that allows timing assumptions to be incorporated into automatic proofs of arbitrary finite-state temporal properties. The obvious extension is to be able to prove timing properties, not just assume them. This would provide a verification framework for finite-state hard real-time systems. We conjecture that the method presented can, in fact, be extended in this way.
---
paper_title: You Assume, We Guarantee: Methodology and Case Studies

paper_content:

Assume-guarantee reasoning has long been advertised as an important method for decomposing proof obligations in system verification. Refinement mappings (homomorphisms) have long been advertised as an important method for solving the language-inclusion problem in practice. When confronted with large verification problems, we therefore attempted to make use of both techniques. We soon found that rather than offering instant solutions, the success of assume-guarantee reasoning depends critically on the construction of suitable abstraction modules, and the success of refinement checking depends critically on the construction of suitable witness modules. Moreover, as abstractions need to be witnessed, and witnesses abstracted, the process must be iterated. We present here the main lessons we learned from our experiments, in form of a systematic and structured discipline for the compositional verification of reactive modules. An infrastructure to support this discipline, and automate parts of the verification, has been implemented in the tool MOCHA.
---
paper_title: CMC: A Tool For Compositional Model-Checking Of Real-Time Systems

paper_content:

In this paper we present a tool (CMC) for compositional model-checking of real-time systems. CMC is based on a completely different method compared to existing real-time verification tools (HYTECH, KRONOS, UPPAAL). After a description of the method, we illustrate its efficiency by considering two examples: the Fischer’s mutual exclusion protocol and a railroad crossing system.
---
paper_title: Compositional and symbolic model-checking of real-time systems

paper_content:

Efficient automatic model-checking algorithms for real-time systems have been obtained in recent years based on the state-region graph technique of Alur, Courcoubetis and Dill (1990). However, these algorithms are faced with two potential types of explosion arising from parallel composition: explosion in the space of control nodes, and explosion in the region space over clock-variables. In this paper we attack these explosion problems by developing and combining compositional and symbolic model-checking techniques. The presented techniques provide the foundation for a new automatic verification tool UPPAAL. Experimental results indicate that UPPAAL performs time- and space-wise favorably compared with other real-time verification tools.
---
paper_title: A Space-Efficient On-the-fly Algorithm for Real-Time Model Checking

paper_content:

In temporal-logic model checking, we verify the correctness of a program with respect to a desired behavior by checking whether a structure that models the program satisfies a temporal-logic formula that specifies the behavior. The main practical limitation of model checking is caused by the size of the state space of the program, which grows exponentially with the number of concurrent components. This problem, known as the state-explosion problem, becomes more difficult when we consider real-time model checking, where the program and the specification involve quantitative references to time. In particular, when use timed automata to describe real-time programs and we specify timed behaviors in the logic TCTL, a real-time extension of the temporal logic CTL with clock variables, then the state space under consideration grows exponentially not only with the number of concurrent components, but also with the number of clocks and the length of the clock constraints used in the program and the specification. Two powerful methods for coping with the state-explosion problem are on-the-fly and space-efficient model checking. In on-the-fly model checking, we explore only the portion of the state space of the program whose exploration is essential for determining the satisfaction of the specification. In space-efficient model checking, we store in memory the minimal information required, preferring to spend time on reconstructing information rather than spend space on storing it. In this work we develop an automata-theoretic approach to TCTL model checking that combines both methods. We suggest, for the first time, a PSPACE on-the-fly model-checking algorithm for TCTL.
---
paper_title: On-the-fly symbolic model checking for real-time systems

paper_content:

This paper presents an on-the-fly and symbolic algorithm for checking whether a timed automaton satisfies a formula of a timed temporal logic which is more expressive than TCTL. The algorithm is on-the-fly in the sense that the state-space is generated dynamically and only the minimal amount of information required by the verification procedure is stored in memory. The algorithm is symbolic in the sense that it manipulates sets of states, instead of states, which are represented as boolean combinations of linear inequalities of clocks. We show how a prototype implementation of our algorithm has improved the performances of the tool KRONOS for the verification of the FDDI protocol.
---
paper_title: Efficient Data Structure for Fully Symbolic Verification of Real-Time Software Systems

paper_content:

A new data-structure called RED (Re gion-Encoding Diagram) for the fully symbolic model-checking of real-time software systems is proposed. RED is a BDD-like data-structure for the encoding of regions. Unlike DBM which records differences between pairs of clock readings, RED only uses one auxiliary binary variable for each clock. Thus the number of variables used in RED is always linear to the number of clocks declared in the input system description. Experiment has been carried out to compare RED with previous technologies.
---
paper_title: Efficient conflict driven learning in a Boolean satisfiability solver

paper_content:

One of the most important features of current state-of-the-art SAT solvers is the use of conflict based backtracking and learning techniques. In this paper, we generalize various conflict driven learning strategies in terms of different partitioning schemes of the implication graph. We re-examine the learning techniques used in various SAT solvers and propose an array of new learning schemes. Extensive experiments with real world examples show that the best performing new learning scheme has at least a 2/spl times/ speedup compared with learning schemes employed in state-of-the-art SAT solvers.
---
paper_title: Difference Decision Diagrams

paper_content:

This paper describes a newdata structure, difference decision diagrams (DDDs), for representing a Boolean logic over inequalities of the form x-y ≤ c where the variables are integer or real-valued.We give algorithms for manipulating DDDs and for determining validity, satisfiability, and equivalence. DDDs enable an efficient verification of timed systems modeled as, for example, timed automata or timed Petri nets, since both the states and their associated timing information are represented symbolically, similar to how BDDs represent Boolean predicates. We demonstrate the efficiency of DDDs by analyzing a timed system and compare the results with the tools KRONOS and UPPAAL.
---
paper_title: Timing Assumptions and Verification of Finite-State Concurrent Systems

paper_content:

We have described a scheme that allows timing assumptions to be incorporated into automatic proofs of arbitrary finite-state temporal properties. The obvious extension is to be able to prove timing properties, not just assume them. This would provide a verification framework for finite-state hard real-time systems. We conjecture that the method presented can, in fact, be extended in this way.
---
paper_title: Fully Symbolic Model Checking of Timed Systems using Difference Decision Diagrams

paper_content:

Abstract Current approaches for analyzing timed systems are based on an explicit enumeration of the discrete states and thus these techniques are only capable of analyzing systems with a handful of timers and a few thousand states. We address this limitation by describing how to analyze a timed system fully symbolically, i.e., by representing sets of discrete states and their associated timing information implicitly. We demonstrate the efficiency of the symbolic technique by computing the set of reachable states for a non-trivial timed system and compare the results with the state-of-the-art tools Kronos and Uppaal . With an implementation based on difference decision diagrams, the runtimes are several orders of magnitudes better. The key operation in obtaining these results is the ability to advance time symbolically. We show how to do this efficiently by essentially quantifying out a special variable z which is used to represent the constant zero. The symbolic manipulations given in this paper are sufficient to verify TCTL-formulae fully symbolically.
---
paper_title: Efficient Timed Reachability Analysis using Clock Difference Diagrams

paper_content:

One of the major problems in applying automatic verication tools to industrial-size systems is the excessive amount of memory required during the state-space exploration of a model. In the setting of real-time, this problem of state-explosion requires extra attention as information must be kept not only on the discrete control structure but also on the values of continuous clock variables. In this paper, we present Clock Dierence Diagrams, CDD's, a BDD-like data-structure for representing and eectively manipulating certain non-convex subsets of the Euclidean space, notably those encountered during verication of timed automata. A version of the real-time verication tool Uppaal using CDD's as a compact datastructure for storing explored symbolic states has been implemented. Our experimental results demonstrate signicant space-savings: for 8 industrial examples, the savings are between 46% and 99% with moderate increase in runtime. We further report on how the symbolic state-space exploration itself may be carried out using CDD's.
---
paper_title: Deciding Separation Formulas with SAT

paper_content:

We show a reduction to propositional logic from a Boolean combination of inequalities of the form vi ? vj + c and vi > vj + c, where c is a constant and vi, vj are variables of type real or integer. Equalities and uninterpreted functions can be expressed in this logic as well. We discuss the advantages of using this reduction as compared to competing methods, and present experimental results that support our claims.
---
paper_title: Efficient verification of real-time systems: compact data structure and state-space reduction

paper_content:

During the past few years, a number of verification tools have been developed for real-time systems in the framework of timed automata (e.g. KRONOS and UPPAAL). One of the major problems in applying these tools to industrial-size systems is the huge memory-usage for the exploration of the state-space of a network (or product) of timed automata, as the model-checkers must keep information on not only the control structure of the automata but also the clock values specified by clock constraints. In this paper, we present a compact data structure for representing clock constraints. The data structure is based on an O(n/sup 3/) algorithm which, given a constraint system over real-valued variables consisting of bounds on differences, constructs an equivalent system with a minimal number of constraints. In addition, we have developed an on-the-fly, reduction technique to minimize the space-usage. Based on static analysis of the control structure of a network of timed automata, we are able to compute a set of symbolic states that cover all the dynamic loops of the network in an on-the-fly searching algorithm, and thus ensure termination in reachability analysis. The two techniques and their combination have been implemented in the tool UPPAAL. Our experimental results demonstrate that the techniques result in truly significant space-reductions: for six examples from the literature, the space saving is between 75% and 94%, and in (nearly) all examples time-performance is improved. Also noteworthy is the observation that the two techniques are completely orthogonal.
---
paper_title: The Quest for Efficient Boolean Satisfiability Solvers

paper_content:

The classical NP-complete problem of Boolean Satisfiability (SAT) has seen much interest in not just the theoretical computer science community, but also in areas where practical solutions to this problem enable significant practical applications. Since the first development of the basic search based algorithm proposed by Davis, Putnam, Logemann and Loveland (DPLL) about forty years ago, this area has seen active research effort with many interesting contributions that have culminated in state-of-the-art SAT solvers today being able to handle problem instances with thousands, and in same cases even millions, of variables. In this paper we examine some of the main ideas along this passage that have led to our current capabilities. Given the depth of the literature in this field, it is impossible to do this in any comprehensive way; rather we focus on techniques with consistent demonstrated efficiency in available solvers. For the most part, we focus on techniques within the basic DPLL search framework, but also briefly describe other approaches and look at some possible future research directions.
---
paper_title: Symbolic Verification of Complex Real-Time Systems with Clock-Restriction Diagram

paper_content:

Real-world real-time systems may involve many complex structures, which are difficult to verify. We experiment with the model-checking of an application-layer html-based web-camera which involves structures like event queues, high-layer communication channels, and time-outs. To contain the complexity, we implement our verification tool with a newly developed BDD-like data-structure, reduced CRD (Clock-Restriction Diagram), which has enhanced the verification performance through intensive data-sharing in a previous report. However, the representation of reduced CRD does not allow for quick test of zone containment. To this purpose, we thus have designed a new CRD-based representation, cascade CRD, which has given us enough performance enhancement to successfully verifying several implementations of the web-camera.
---
paper_title: Reducing the number of clock variables of timed automata

paper_content:

We propose a method for reducing the number of clocks of a timed automaton by combining two algorithms. The first one consists in detecting active clocks, that is, those clocks whose values are relevant for the evolution of the system. The second one detects sets of clocks that are always equal. We implemented the algorithms and applied them to several case studies. These experimental results show that an appropriate encoding of the state space, based on the output of the algorithms, leads to a considerable reduction of the memory space allowing a more eficient Verification.
---
paper_title: An improvement in formal verification

paper_content:

Critical safety and liveness properties of a concurrent system can often be proven with the help of a reachability analysis of a finite state model. This type of analysis is usually implemented as a depthfirst search of the product statespace of all components in the system, with each (finite state) component modeling the behavior of one asynchronously executing process. Formal verification is achieved by coupling the depthfirst search with a method for identifying those states or sequences of states that violate the correct- ness requirements. It is well known, however, that an exhaustive depthfirst search of this type performs redundant work. The redundancy is caused by the many possible interleavings of inde- pendent actions in a concurrent system. Few of these interleavings can alter the truth or falsity of the correctness properties being studied. The standard depthfirst search algorithm can be modified to track additional information about the interleavings that have already been inspected, and use this information to avoid the exploration of redundant interleavings. Care must be taken to perform the reductions in such a way that the capability to prove both safety and liveness properties is fully pre- served. Not all known methods have this property. Another potential drawback of the existing methods is that the additional computations required to enforce a reduction dur- ing the search can introduce overhead that diminishes the benefits. In this paper we dis- cuss a new reduction method that solves some of these problems.
---
paper_title: Combining partial order reductions with on-the-fly model-checking

paper_content:

Partial order model-checking is an approach to reduce time and memory in model-checking concurrent programs. On-the-fly model-checking is a technique to eliminate part of the search by intersecting an automaton representing the (negation of the) checked property with the state during its generation. We prove conditions under which these two methods can be combined in order to gain reduction from both. An extension of the model-checker SPIN, which implements this combination, is studied, showing substantial reduction over traditional search, not only in the number of reachable states, but directly in the amount of memory and time used. We also describe how to apply partial-order model-checking under given fairness assumptions.
---
paper_title: Partial Order reduction for Model Checking of Timed Automata

paper_content:

The paper presents a partial order reduction method applicable to networks of timed automata. The advantage of the method is that it reduces both the number of explored control states and the number of generated time zones. The approach is based on a local-time semantics for networks of timed automata defined by Bengtsson et al. [1998]. and used originally for local reachability analysis. In this semantics, each component automaton executes asynchronously, in its own local time scale, which is tracked by an auxiliary reference clock. On communication transitions, the automata synchronize their time scales. We show how this model can be used to perform model checking for an extension of linear temporal logic, which can express timing relations between events. We also show how for a class of timed automata, the local-time model can be implemented using difference bound matrices without any space penalty despite the need to represent local time. Furthermore, we analyze the dependence relation between transitions in the new model and give practical conditions for selecting a reduced set of transitions.
---
paper_title: Partial Orders and Verification of Real-Time systems

paper_content:

We show in this paper how the verification method of timed graphs ([1], [6]) can be substantially improved by the use of a partialorder technique. In [5] and [4] is presented an efficient model-checking algorithm for concurrent systems that avoids most of the state explosion due to the modeling of concurrency by interleaving. We adapt this work to timed graphs, by defining a dependency relation on transitions and an equivalence on executions, taking into account quantitative aspects of time. We then propose a selective search algorithm that computes a reduced accessibility graph, in the framework of deadlock detection.
---
paper_title: Partial Order Reductions for Timed Systems

paper_content:

In this paper, we present a partial-order reduction method for timed systems based on a local-time semantics for networks of timed automata. The main idea is to remove the implicit clock synchronization between processes in a network by letting local clocks in each process advance independently of clocks in other processes, and by requiring that two processes resynchronize their local time scales whenever they communicate. A symbolic version of this new semantics is developed in terms of predicate transformers, which enjoys the desired property that two predicate transformers are independent if they correspond to disjoint transitions in different processes. Thus we can apply standard partial order reduction techniques to the problem of checking reachability for timed systems, which avoid exploration of unnecessary interleavings of independent transitions. The price is that we must introduce extra machinery to perform the resynchronization operations on local clocks. Finally, we present a variant of DBM representation of symbolic states in the local time semantics for efficient implementation of our method.
---
paper_title: Communicating sequential processes

paper_content:

This paper suggests that input and output are basic primitives of programming and that parallel composition of communicating sequential processes is a fundamental program structuring method. When combined with a development of Dijkstra's guarded command, these concepts are surprisingly versatile. Their use is illustrated by sample solutions of a variety of familiar programming exercises.
---
paper_title: Saving Space by Fully Exploiting Invisible Transitions

paper_content:

Checking that a given finite state program satisfies a linear temporal logic property suffers from the state explosion problem. Often the resulting lack of available memory is more significant than any time limitations. One way to cope with this is to reduce the state graph used for model checking. We present an algorithm for constructing a state graph that is a projection of the program‘s state graph. The algorithm maintains the transitions and states that affect the truth of the property to be checked. Especially in conjunction with known partial order reduction algorithms, we show a substantial reduction in memory over using partial order methods alone, both in the precomputation stage, and in the result presented to a model checker. The price of the space reduction is a single additional traversal of the graph obtained with partial order reduction. As part of our space-saving methods, we present a new way to exploit Holzmann‘s Bit Hash Table, which assists us in solving the revisiting problem.
---
paper_title: Model Reduction of Modules for State-Event Temporal Logics

paper_content:

In many Discrete-Event Systems (DES) both state and event information are of importance to the systems designer. Logics such as Ostroff’s RTTL allow for the specification and verification of a system’s state-event behavior. To make realistic problems amenable to analysis, a designer must typically decompose the system into subsystems (modules) and use algebraic abstraction (quotient systems) to obtain hierarchical system models that preserve the properties to be verified. In this paper we use state-event observational equivalence to perform model reduction for a subclass of formulas of state-event linear temporal logics, with particular attention being paid to a discrete time temporal logic that is a simplification of RTTL. The reduction technique allows limited use of immediate operators.
---
paper_title: Efficient Data Structure for Fully Symbolic Verification of Real-Time Software Systems

paper_content:

A new data-structure called RED (Re gion-Encoding Diagram) for the fully symbolic model-checking of real-time software systems is proposed. RED is a BDD-like data-structure for the encoding of regions. Unlike DBM which records differences between pairs of clock readings, RED only uses one auxiliary binary variable for each clock. Thus the number of variables used in RED is always linear to the number of clocks declared in the input system description. Experiment has been carried out to compare RED with previous technologies.
---
paper_title: Utilizing Symmetry when Model Checking under Fairness Assumptions: An Automata-theoretic Approach

paper_content:

One useful technique for combating the state explosion problem is to exploit symmetry [ID93, CFJ93, ES93] when performing temporal logic model checking [CE81, CES86]. In [CFJ93] [ES93] it is shown how, using some basic notions of group theory, symmetry may be exploited for the full range of correctness properties expressible in the very expressive temporal logic CTL*. Surprisingly, while fairness properties are readily expressible in CTL*, these methods are not powerful enough to admit any amelioration of state explosion, when fairness assumptions are involved. We show that it is nonetheless possible to handle fairness efficiently by trading some group theory for automata theory. Our automata-theoretic approach [VW86] depends on detecting fair paths subtly encoded in a permutation annotated quotient structure, using a threaded structure to “physically” reflect coordinate permutations.
---
paper_title: Verification of Hybrid Systems Based on Counterexample-Guided Abstraction Refinement

paper_content:

Hybrid dynamic systems include both continuous and discrete state variables. Properties of hybrid systems, which have an infinite state space, can often be verified using ordinary model checking together with a finite-state abstraction. Model checking can be inconclusive, however, in which case the abstraction must be refined. This paper presents a new procedure to perform this refinement operation for abstractions of infinite-state systems, in particular of hybrid systems. Following an approach originally developed for finite-state systems [1, 2], the refinement procedure constructs a new abstraction that eliminates a counterexample generated by the model checker. For hybrid systems, analysis of the counterexample requires the computation of sets of reachable states in the continuous state space.We showhowsuch reachability computations with varying degrees of complexity can be used to refine hybrid system abstractions efficiently. A detailed example illustrates our counterexample-guided refinement procedure. Experimental results for a prototype implementation of the procedure indicate its advantages over existing methods.
---
paper_title: The Tool KRONOS

paper_content:

Both approaches presented in this paper considerably improve Kronos performance and functionalities.
---
paper_title: UPPAAL - a Tool Suite for Automatic Verification of Real-Time Systems

paper_content:

Uppaal is a tool suite for automatic verification of safety and bounded liveness properties of real-time systems modeled as networks of timed automata. It includes: a graphical interface that supports graphical and textual representations of networks of timed automata, and automatic transformation from graphical representations to textual format, a compiler that transforms a certain class of linear hybrid systems to networks of timed automata, and a model-checker which is implemented based on constraint-solving techniques. Uppaal also supports diagnostic model-checking providing diagnostic information in case verification of a particular real-time systems fails.
---
paper_title: Counter-example guided predicate abstraction of hybrid systems

paper_content:

Predicate abstraction has emerged to be a powerful technique for extracting finite-state models from infinite-state systems, and has been recently shown to enhance the effectiveness of the reachability computation techniques for hybrid systems. Given a hybrid system with linear dynamics and a set of linear predicates, the verifier performs an on-the-fly search of the finite discrete quotient whose states correspond to the truth assignments to the input predicates. The success of this approach depends on the choice of the predicates used for abstraction. In this paper, we focus on identifying these predicates automatically by analyzing spurious counter-examples generated by the search in the abstract state-space. We present the basic techniques for discovering new predicates that will rule out closely related spurious counter-examples, optimizations of these techniques, implementation of these in the verification tool, and case studies demonstrating the promise of the approach.
---
paper_title: Symbolic approximations for verifying real-time systems

paper_content:

Real-time systems are appearing in more and more applications where their proper operation is critical, e.g. transport controllers and medical equipment. However they are extremely difficult to design correctly: one must consider the sequencing and coordination of events in different processes, as well as the times they occur. One approach to this problem is the use of formal description techniques and automatic verification. Unfortunately automatic verification suffers from the state-real-time explosion problem and is computationally expensive even without real-time. The addition of timing information makes the problem much harder. This thesis proposes a state-based approximation scheme as a heuristic for reducing the effort required in verification. ::: We first describe a generic iterative approximation algorithm for checking safety properties of a transition system. It is designed to exploit the fact that not all the details of a system need to be considered in order to prove it correct. Successively more accurate approximations of the reachable states are generated until it can be determined whether the specification is satisfied or not. The algorithm automatically decides where the analysis needs to be more exact, and uses state partitioning to force the approximations to converge towards a solution. In the case of finite-state systems, the method is complete. ::: The algorithm is used to verify that systems with hard real-time bounds satisfy timed safety properties. State approximations are performed over both timing information and control information. We describe some examples of successful verification, and successful error-detection. Case studies include some timing properties of the MAC sublayer of the Ethernet protocol, and a timing-based communication protocol where the sender's and receiver's clocks advance at variable rates.
---
paper_title: Counterexample-guided abstraction refinement for symbolic model checking

paper_content:

The state explosion problem remains a major hurdle in applying symbolic model checking to large hardware designs. State space abstraction, having been essential for verifying designs of industrial complexity, is typically a manual process, requiring considerable creativity and insight.In this article, we present an automatic iterative abstraction-refinement methodology that extends symbolic model checking. In our method, the initial abstract model is generated by an automatic analysis of the control structures in the program to be verified. Abstract models may admit erroneous (or "spurious") counterexamples. We devise new symbolic techniques that analyze such counterexamples and refine the abstract model correspondingly. We describe aSMV, a prototype implementation of our methodology in NuSMV. Practical experiments including a large Fujitsu IP core design with about 500 latches and 10000 lines of SMV code confirm the effectiveness of our approach.
---
paper_title: Symbolic Simulation of Industrial Real-Time and Embedded Systems-Experiments with the Bluetooth Baseband Communication Protocol

paper_content:

We introduce the symbolic simulation function implemented in our model-checker/simulator RED 4.0 for dense-time concurrent systems. By representing and manipulating state-spaces as logic predicates, the technique of symbolic simulation can lead to high performance by encoding even a dense amount of traces in traditional simulation into one symbolic trace. Symbolic simulation adds the dimension of width to a trace of state-spaces. By controlling the width of traces, we have a much better chance to find bugs using fewer traces. ::: ::: Our main contribution is the design of symbolic simulation function in RED 4.0 for dense-time concurrent systems. In our tool, users can strongly control the width of traces and the generation of traces. We discuss how to generate traces using various policies, how to manipulate the state-predicate, and how to manage the trace trees. Moreover, we design a C-like language whose programs can be mechanically translated into the optimized communicating timed automata(CTA). Engineers can also put down comment-line assertions as specifications in their verification tasks. Finally, experiments using our simulator to verify the Bluetooth baseband protocol justify the usefulness of our tool. The tool is available at http://cc.ee.ntu.edu.tw/~farn/.
---
paper_title: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints

paper_content:

A program denotes computations in some universe of objects. Abstract interpretation of programs consists in using that denotation to describe computations in another universe of abstract objects, so that the results of abstract execution give some information on the actual computations. An intuitive example (which we borrow from Sintzoff [72]) is the rule of signs. The text -1515 * 17 may be understood to denote computations on the abstract universe {(+), (-), (±)} where the semantics of arithmetic operators is defined by the rule of signs. The abstract execution -1515 * 17 → -(+) * (+) → (-) * (+) → (-), proves that -1515 * 17 is a negative number. Abstract interpretation is concerned by a particular underlying structure of the usual universe of computations (the sign, in our example). It gives a summary of some facets of the actual executions of a program. In general this summary is simple to obtain but inaccurate (e.g. -1515 + 17 → -(+) + (+) → (-) + (+) → (±)). Despite its fundamentally incomplete results abstract interpretation allows the programmer or the compiler to answer questions which do not need full knowledge of program executions or which tolerate an imprecise answer, (e.g. partial correctness proofs of programs ignoring the termination problems, type checking, program optimizations which are not carried in the absence of certainty about their feasibility, …).
---
paper_title: Approximate reachability analysis of timed automata

paper_content:

A promising approach to formal verification of real-time systems is to use timed automata to model systems, and then to check whether certain "unsafe" states are reachable. Although theoretically appealing, this approach has significant practical problems because it requires expensive computation of reachable states. Fortunately computing a superset of reachable states is sometimes much cheaper. Replacing the set of reachable states with its superset is a conservative approximation, in the sense that it can occasionally cause a correct system to be declared incorrect, but can never cause an incorrect system to be declared correct. We propose two algorithms for computing a superset of reachable states of a timed automaton. Both algorithms involve only manipulation of Boolean functions, which are used to represent both sets of discrete state components and timing information. The algorithms offer different trade-offs between accuracy of approximation and efficiency of computation. Initial experimental results show that they are competitive with the best published results, but that further improvements are necessary to scale up to realistic systems.
---
paper_title: Implementing a verifier for real-time systems

paper_content:

The SARTOR project has as one of its goals the development of an environment for the development of correct real-time systems. Modechart is a specification language for real-time systems developed as part of this project. Verify4 is an implementation of a verifier for certain classes of properties of systems specified using Modechart. The author describes the program Verify4 and addresses implementation issues surrounding three of the key algorithms used in the program. >
---
paper_title: Safety analysis of timing properties in real-time systems

paper_content:

The authors formalize the safety analysis of timing properties in real-time systems. The analysis is based on a formal logic, RTL (real-time logic), which is especially suitable for reasoning about the timing behavior of systems. Given the formal specification of a system and a safety assertion to be analyzed, the goal is to relate the safety assertion to the systems specification. There are three distinct cases: (1) the safety assertion is a theorem derivable from the systems specification; (2) the safety assertion is unsatisfiable with respect to the systems specification; or (3) the negation of the safety assertion is satisfiable under certain conditions. A systematic method for performing safety analysis is presented.
---
paper_title: Modechart Toolset User's Guide

paper_content:

Abstract : This document describes how to use the Modechart Toolset (MT). MT is a set of tools designed to facilitate the specification, modeling, and analysis of real-time embedded systems using the Modechart language. MT supports the creation, modification, and storage of Modechart specifications. It also supports the analysis of Modechart specifications via a consistency and completeness checker, a simulator and a verifier. Modechart Toolset(MT), Simulation, Verification, Real-time systems consistency and completeness.
---
paper_title: A flexible, extensible simulation environment for testing real-time specifications

paper_content:

This paper describes MTSim, an extensible, customizable simulation platform for the Modechart toolset (MT). MTSim provides support for "plugging in" user-defined viewers useful an simulating system behavior in different ways, including application-specific ways. MTSim also supports full user participation in the generation of simulations by allowing users to inject events into the execution trace. Moreover, MTSim provides monitoring and assertion checking of execution traces and the invocation of user-specified handlers upon assertion violation. This paper also introduces a MTSim component called WebSim, a suite of simulation tools for MT, and an an application-specific component of MTSim, which displays the cockpit of an F-18 aircraft and models its bomb release function.
---
paper_title: Modechart: a specification language for real-time systems

paper_content:

Present a specification language for real-time systems called Modechart. The semantics of Modechart is given in terms of real-time logic (RTL), which is especially amenable to reasoning about the absolute (real-time clock) timing of events. The semantics of Modechart has an important property that the translation of a Modechart specification into RTL formulas results in a hierarchical organization of the resulting RTL assertions. This gives us significant leverage in reasoning about properties of a system by allowing us to filter out assertions that concern lower levels of abstraction. Some results about desirable properties of Modechart specifications are given. A graphical implementation of Modechart has been completed. >
---
paper_title: Semantics of Modechart in real time logic

paper_content:

The authors present a specification language called Modechart, which is especially amenable to the specification of real-time systems by graphical means. In addition to the behavioral description, Modechart permits the specification of timing constraints, an important element in real-time systems. A formal semantics for Modechart is provided in terms of real-time logic. >
---
paper_title: MT: A toolset for specifying and analyzing real-time systems

paper_content:

This paper introduces MT, a collection of integrated tools for specifying and analyzing real-time systems using the Modechart language. The toolset includes facilities for creating and editing Modechart specifications. Users may symbolically execute the specifications with an automatic simulation tool to make sure that the specified behavior is what was intended. They may also invoke a verifier that uses model-checking to determine whether the specifications imply (satisfy) any of a broad class of safety assertions. To illustrate the toolset's capabilities as well as several issues that arise when formal methods are applied to real-world systems, the paper includes specifications and analysis procedures for a software component taken from an actual Naval real-time system. >
---
paper_title: Modeling And Verification Of Parallel Processes

paper_content:

Thank you for reading modeling and verification of parallel processes. Maybe you have knowledge that, people have search numerous times for their favorite novels like this modeling and verification of parallel processes, but end up in infectious downloads. Rather than reading a good book with a cup of coffee in the afternoon, instead they are facing with some malicious virus inside their computer. modeling and verification of parallel processes is available in our book collection an online access to it is set as public so you can download it instantly. Our digital library spans in multiple locations, allowing you to get the most less latency time to download any of our books like this one. Merely said, the modeling and verification of parallel processes is universally compatible with any devices to read.
---
paper_title: Subtypes for Specifications: Predicate Subtyping in PVS

paper_content:

A specification language used in the context of an effective theorem prover can provide novel features that enhance precision and expressiveness. In particular, type checking for the language can exploit the services of the theorem prover. We describe a feature called "predicate subtyping" that uses this capability and illustrate its utility as mechanized in PVS.
---
paper_title: Automatic symbolic verification of embedded systems

paper_content:

Presents a model-checking procedure and its implementation for the automatic verification of embedded systems. The system components are described as hybrid automata-communicating machines with finite control and real-valued variables that represent continuous environment parameters such as time, pressure and temperature. The system requirements are specified in a temporal logic with stop-watches, and verified by symbolic fixpoint computation. The verification procedure-implemented in the Cornell Hybrid Technology tool, HyTech-applies to hybrid automata whose continuous dynamics is governed by linear constraints on the variables and their derivatives. We illustrate the method and the tool by checking safety, liveness, time-bounded and duration requirements of digital controllers, schedulers and distributed algorithms.
---
paper_title: The Tool KRONOS

paper_content:

Both approaches presented in this paper considerably improve Kronos performance and functionalities.
---
paper_title: UPPAAL - a Tool Suite for Automatic Verification of Real-Time Systems

paper_content:

Uppaal is a tool suite for automatic verification of safety and bounded liveness properties of real-time systems modeled as networks of timed automata. It includes: a graphical interface that supports graphical and textual representations of networks of timed automata, and automatic transformation from graphical representations to textual format, a compiler that transforms a certain class of linear hybrid systems to networks of timed automata, and a model-checker which is implemented based on constraint-solving techniques. Uppaal also supports diagnostic model-checking providing diagnostic information in case verification of a particular real-time systems fails.
---
paper_title: Parking can get you there faster - Model Augmentation to Speed up Real-Time Model-Checking

paper_content:

Abstract We present an approximation technique, that can render real-time model checking of safety and universal path properties more efficient. It is beneficial, when loops lead to repetition of control situations. Basically we augment a timed automata model with carefully selected extra transitions. This increases the size of the state-space, but potentially decreases the number of symbolic states to be explored by orders of magnitude. We give a formal definition of a timed automata formalism, enriched with basic data types, hand-shake synchronization, urgency, and committed locations. We prove by means of a trace semantics, that if a safety property can be established in the augmented model, it also holds for the original model. We extend our technique to a richer set of properties, that can be decided via a set of traces (universal path properties). In order for universal path properties to carry over to the original model, the semantics of the timed automata formalism is formulated relative to the applied augmentation. Our technique is particularly useful in systems, where a scheduler dictates repetition of control over elapsing time. As a typical example we mention translations of LEGO® RCX™ programs to U ppaal models, where the Round-Robin scheduler is a static entity. We allow scheduler and associated tasks to “park”, until some timing or environmental conditions are met. We apply our technique on a brick-sorter model for a safety property and report run-time data.
---
paper_title: Static guard analysis in timed automata verification

paper_content:

By definition Timed Automata have an infinite state-space, thus for verification purposes, an exact finite abstraction is required. We propose a location-based finite zone abstraction, which computes an abstraction based on the relevant guards for a particular state of the model (as opposed to all guards).We show that the location-based zone abstraction is sound and complete with respect to location reachability; that it generalises active-clock reduction, in the sense that an inactive clock has no relevant guards at all; that it enlarges the class of timed automata, that can be verified. We generalise the new abstraction to the case of networks of timed automata, and experimentally demonstrate a potentially exponential speedup compared to the usual abstraction.
---
paper_title: Probabilistic Resource Failure in Real-Time Process Algebra ?

paper_content:

PACSR, a probabilistic extension of the real-time process algebra ACSR, is presented. The extension is built upon a novel treatment of the notion of a resource. In ACSR, resources are used to model contention in accessing physical devices. Here, resources are invested with the ability to fail and are associated with a probability of failure. The resulting formalism allows one to perform probabilistic analysis of real-time system specifications in the presence of resource failures. A probabilistic variant of Hennessy-Milner logic with until is presented. The logic features an until operator which is parameterized by both a probabilistic constraint and a regular expression over observable actions. This style of parameterization allows the application of probabilistic constraints to complex execution fragments. A model-checking algorithm for the proposed logic is also given. Finally, PACSR and the logic are illustrated with a telecommunications example.
---
paper_title: A Process Algebraic Approach to the Specification and Analysis of Resource-Bound Real-Time Systems

paper_content:

Recently, significant progress has been made in the development of timed process algebras for the specification and analysis of real-time systems. This paper describes a timed process algebra called ACSR, which supports synchronous timed actions and asynchronous instantaneous events. Timed actions are used to represent the usage of resources and to model the passage of time. Events are used to capture synchronization between processes. To be able to specify real systems accurately, ACSR supports a notion of priority that can be used to arbitrate among timed actions competing for the use of resources and among events that are ready for synchronization. The paper also includes a brief overview of other timed process algebras and discusses similarities and differences between them and ACSR. >
---
paper_title: MOCHA: Modularity in Model Checking

paper_content:

R. Alur1, T.A. Henzinger2, F.Y.C. Mang2, S. Qadeer2, S.K. Rajamani2, and S. Tasiran2 1 Computer & Information Science Department, University of Pennsylvania, Philadelphia, PA 19104. Computing Science Research Center, Bell Laboratories, Murray Hill, NJ 07974. alur@cis.upenn.edu 2 Electrical Engineering & Computer Sciences Department, University of California, Berkeley, CA 94720. ftah,fmang,shaz,sriramr,serdarg@eecs.berkeley.edu
---
paper_title: VIS: A System for Verification and Synthesis

paper_content:

ion Manual abstraction can be performed by giving a file containing the names of variables to abstract. For each variable appearing in the file, a new primary input node is created to drive all the nodes that were previously driven by the variable. Abstracting a net effectively allows it to take any value in its range, at every clock cycle. Fair CTL model checking and language emptiness check VIS performs fair CTL model checking under Buchi fairness constraints. In addition, VIS can perform language emptiness checking by model checking the formula EG true. The language of a design is given by sequences over the set of reachable states that do not violate the fairness constraint. The language emptiness check can be used to perform language containment by expressing the set of bad behaviors as another component of the system. If model checking or language emptiness fail, VIS reports the failure with a counterexample, (i.e., behavior seen in the system that does not satisfy the property for model checking, or valid behavior seen in the system for language emptiness). This is called the “debug” trace. Debug traces list a set of states that are on a path to a fair cycle and fail the CTL formula. Equivalence checking VIS provides the capability to check the combinational equivalence of two designs. An important usage of combinational equivalence is to provide a sanity check when re-synthesizing portions of a network. VIS also provides the capability to test the sequential equivalence of two designs. Sequential verification is done by building the product finite state machine, and checking whether a state where the values of two corresponding outputs differ, can be reached from the set of initial states of the product machine. If this happens, a debug trace is provided. Both combinational and sequential verification are implemented using BDD-based routines. Simulation VIS also provides traditionaldesign verification in the form of a cycle-based simulator that uses BDD techniques. Since VIS performs both formal verification and simulation using the same data structures, consistency between them is ensured. VIS can generate random input patterns or accept user-specified input patterns. Any subtree of the specified hierarchy may be simulated.
---
paper_title: Timed I/O automata: a mathematical framework for modeling and analyzing real-time systems

paper_content:

We describe the timed input/output automata (TIOA) framework, a general mathematical framework for modeling and analyzing real-time systems. It is based on timed I/O automata, which engage in both discrete transitions and continuous trajectories. The framework includes a notion of external behavior, and notions of composition and abstraction. We define safety and liveness properties for timed I/O automata, and a notion of receptiveness, and prove basic results about all of these notions. The TIOA framework is defined as a special case of the new hybrid I/O automata (HIOA) modeling framework for hybrid systems. Specifically, a TIOA is an HIOA with no external variables; thus, TIOAs communicate via shared discrete actions only, and do not interact continuously. This restriction is consistent with previous real-time system models, and gives rise to some simplifications in the theory (compared to HIOA). The resulting model is expressive enough to describe complex timing behavior, and to express the important ideas of previous timed automata frameworks.
---
paper_title: Larch: Languages and Tools for Formal Specification

paper_content:

This monograph addresses the use of formal specification languages and supporting tools. Concentrating on the Larch specification work taking place at DEC and MIT, it discusses the use of formal specifications in program development and introduces the notation of mathematical logic.
---
paper_title: Symbolic Verification of Lossy Channel Systems: Application to the Bounded Retransmission Protocol

paper_content:

We consider the problem of verifying automatically infinitestate systems that are systems of finite machines that communicate by exchanging messages through unbounded lossy fifo channels. In a previous work [1], we proposed an algorithmic approach based on constructing a symbolic representation of the set of reachable configurations of a system by means of a class of regular expressions (SREs). The construction of such a representation consists of an iterative computation with an acceleration technique which enhances the chance of convergence. This technique is based on the analysis of the effect of iterating control loops. In the work we present here, we experiment our approach and show how it can be effectively applied. For that, we developed a tool prototype based on the results in [1]. Using this tool, we provide an automatic verification of (the parameterized version of) the Bounded Retransmission Protocol.
---
paper_title: On-the-Fly Analysis of Systems with Unbounded, Lossy FIFO Channels

paper_content:

We consider symbolic on-the-fly verification methods for systems of finite-state machines that communicate by exchanging messages via unbounded and lossy FIFO queues. We propose a novel representation formalism, called simple regular expressions (SREs), for representing sets of states of protocols with lossy FIFO channels. We show that the class of languages representable by SREs is exactly the class of downward closed languages that arise in the analysis of such protocols. We give methods for (i) computing inclusion between SREs, (ii) an SRE representing the set of states reachable by executing a single transition in a system, and (iii) an SRE representing the set of states reachable by an arbitrary number of executions of a control loop of a program. All these operations are rather simple and can be carried out in polynomial time. With these techniques, one can construct a semi-algorithm which explores the set of reachable states of a protocol, in order to check various safety properties.
---
paper_title: TReX: A Tool for Reachability Analysis of Complex Systems

paper_content:

Finite-state model-checkers such as Smv [13] and Spin [11] do not allow to deal with important aspects that appear in modelling and analysing complex systems, e.g., communication protocols. Among these aspects: real-time constraints, manipulation of unbounded data structures like counters, communication through unbounded channels, parametric reasoning, etc.
---
paper_title: Symbolic Techniques for Parametric Reasoning about Counter and Clock Systems

paper_content:

We address the problem of automatic analysis of parametric counter and clock automata. We propose a semi-algorithmic approach based on using (1) expressive symbolic representation structures called Parametric DBM's and (2) accurate extrapolation techniques allowing to speed up the reachability analysis and help its termination. The techniques we propose consist in guessing automatically the effect of iterating a control loop an arbitray number of times, and in checking that this guess is exact. Our approach can deal uniformly with systems that generate linear or nonlinear sets of configurations. We have implemented our techniques and experimented them on nontrivial examples such as a parametric timed version of the Bounded Retransmission Protocol.
---
paper_title: CMC: A Tool For Compositional Model-Checking Of Real-Time Systems

paper_content:

In this paper we present a tool (CMC) for compositional model-checking of real-time systems. CMC is based on a completely different method compared to existing real-time verification tools (HYTECH, KRONOS, UPPAAL). After a description of the method, we illustrate its efficiency by considering two examples: the Fischer’s mutual exclusion protocol and a railroad crossing system.
---
paper_title: Compositional and symbolic model-checking of real-time systems

paper_content:

Efficient automatic model-checking algorithms for real-time systems have been obtained in recent years based on the state-region graph technique of Alur, Courcoubetis and Dill (1990). However, these algorithms are faced with two potential types of explosion arising from parallel composition: explosion in the space of control nodes, and explosion in the region space over clock-variables. In this paper we attack these explosion problems by developing and combining compositional and symbolic model-checking techniques. The presented techniques provide the foundation for a new automatic verification tool UPPAAL. Experimental results indicate that UPPAAL performs time- and space-wise favorably compared with other real-time verification tools.
---
paper_title: Efficient Data Structure for Fully Symbolic Verification of Real-Time Software Systems

paper_content:

A new data-structure called RED (Re gion-Encoding Diagram) for the fully symbolic model-checking of real-time software systems is proposed. RED is a BDD-like data-structure for the encoding of regions. Unlike DBM which records differences between pairs of clock readings, RED only uses one auxiliary binary variable for each clock. Thus the number of variables used in RED is always linear to the number of clocks declared in the input system description. Experiment has been carried out to compare RED with previous technologies.
---
paper_title: Numerical Coverage Estimation for the Symbolic Simulation of Real-Time Systems

paper_content:

Three numerical coverage metrics for the symbolic simulation of dense-time systems and their estimation methods are presented. Special techniques to derive numerical estimations of dense-time state-spaces have also been developed. Properties of the metrics are also discussed with respect to four criteria. Implementation and experiments are then reported.
---
paper_title: Automatic Verification of Real-time Systems with Discrete Probability Distributions

paper_content:

We consider the timed automata model of [3], which allows the analysis of real-time systems expressed in terms of quantitative timing constraints. Traditional approaches to real-time system description express the model purely in terms of nondeterminism; however, we may wish to express the likelihood of the system making certain transitions. In this paper, we present a model for real-time systems augmented with discrete probability distributions. Furthermore, using the algorithm of [5] with fairness, we develop a model checking method for such models against temporal logic properties which can refer both to timing properties and probabilities, such as, "with probability 0.6 or greater, the clock x remains below 5 until clock y exceeds 2".
---
paper_title: Principles of Verifiable Rtl Design: A Functional Coding Style Supporting Verification Processes in Verilog

paper_content:

Foreword. Preface. 1. Introduction. 2. The Verification Process. 3. Coverage, Events and Assertions. 4. RTL Methodology Basics. 5. RTL Logic Simulation. 6. RTL Formal Verification. 7. Verifiable RTL Style. 8. The Bad Stuff. 9. Verifiable RTL Tutorial. 10. Principles of Verifiable RTL Design. Bibliography. A. Comparing Verilog Construct Performance. B. Quick Reference. C. Assertion Monitors.
---
paper_title: Numerical Coverage Estimation for the Symbolic Simulation of Real-Time Systems

paper_content:

Three numerical coverage metrics for the symbolic simulation of dense-time systems and their estimation methods are presented. Special techniques to derive numerical estimations of dense-time state-spaces have also been developed. Properties of the metrics are also discussed with respect to four criteria. Implementation and experiments are then reported.
---
paper_title: Parametric Timing Analysis for Real-Time Systems

paper_content:

We extend a TCTL model-checking problem to a parametric timing analysis problem for real-time systems and develop new techniques for solving it. The algorithm we present here accepts timed transition system descriptions and parametric TCTL formulas with timing parameter variables of unknown sizes and can give back general linear equations of timing parameter variables whose solutions make the systems work.
---
paper_title: On-the-Fly Analysis of Systems with Unbounded, Lossy FIFO Channels

paper_content:

We consider symbolic on-the-fly verification methods for systems of finite-state machines that communicate by exchanging messages via unbounded and lossy FIFO queues. We propose a novel representation formalism, called simple regular expressions (SREs), for representing sets of states of protocols with lossy FIFO channels. We show that the class of languages representable by SREs is exactly the class of downward closed languages that arise in the analysis of such protocols. We give methods for (i) computing inclusion between SREs, (ii) an SRE representing the set of states reachable by executing a single transition in a system, and (iii) an SRE representing the set of states reachable by an arbitrary number of executions of a control loop of a program. All these operations are rather simple and can be carried out in polynomial time. With these techniques, one can construct a semi-algorithm which explores the set of reachable states of a protocol, in order to check various safety properties.
---
paper_title: Parametric quantitative temporal reasoning

paper_content:

We define Parameterized Real-Time Computation Tree Logic (PRTCTL), which allows quantitative temporal specifications to be parameterized over the natural numbers. Parameterized quantitative specifications are quantitative specifications in which concrete timing information has been abstracted away. Such abstraction allows designers to specify quantitative restrictions on the temporal ordering of events without having to use specific timing information from the model. A model checking algorithm for the logic is given which is polynomial for any fixed number of parameters. A subclass of formulae are identified for which the model checking problem is linear in the length of the formula and size of the structure. PRTCTL is generalised to allow quantitative reasoning about the number of occurrences of atomic events.
---
paper_title: Parametric temporal logic for “model measuring”

paper_content:

We extend the standard model checking paradigm of linear temporal logic, LTL, to a “model measuring” paradigm where one can obtain more quantitative information beyond a “Yes/No” answer. For this purpose, we define a <italic>parametric temporal logic</italic>, PLTL, which allows statements such as “a request <italic>p</italic> is followed in at most <italic>x</italic> steps by a response <italic>q</italic>,” where <italic>x</italic> is a free variable. We show how one can, given a formula ***(<italic>x<subscrpt>1</subscrpt>...,x<subsccrpt>k</subscrpt></italic>) of PLTL and a system model <italic>K</italic> satisfies the property ***, but if so find valuations which satisfy various optimality criteria. In particular, we present algorithms for finding valuations which minimize (or maximize) the maximum (or minimum) of all parameters. Theses algorithms exhibit the same PSPACE complexity as LTL model checking. We show that our choice of syntax for PLTL lies at the threshold of decidability for parametric temporal logics, in that several natural extensions have undecidable “model measuring” problems.
---
paper_title: Automatic symbolic verification of embedded systems

paper_content:

Presents a model-checking procedure and its implementation for the automatic verification of embedded systems. The system components are described as hybrid automata-communicating machines with finite control and real-valued variables that represent continuous environment parameters such as time, pressure and temperature. The system requirements are specified in a temporal logic with stop-watches, and verified by symbolic fixpoint computation. The verification procedure-implemented in the Cornell Hybrid Technology tool, HyTech-applies to hybrid automata whose continuous dynamics is governed by linear constraints on the variables and their derivatives. We illustrate the method and the tool by checking safety, liveness, time-bounded and duration requirements of digital controllers, schedulers and distributed algorithms.
---
paper_title: TReX: A Tool for Reachability Analysis of Complex Systems

paper_content:

Finite-state model-checkers such as Smv [13] and Spin [11] do not allow to deal with important aspects that appear in modelling and analysing complex systems, e.g., communication protocols. Among these aspects: real-time constraints, manipulation of unbounded data structures like counters, communication through unbounded channels, parametric reasoning, etc.
---
paper_title: Reachability solution characterization of parametric real-time systems

paper_content:

We investigate the problem of characterizing the solution spaces for timed automata augmented by unknown timing parameters (called timing parameter automata (TPA)). The main contribution of this paper is that we identify three non-trivial subclasses of TPAs, namely, upper-bound, lower-bound and bipartite TPAs, and analyze how hard it is to characterize the solution spaces. As it turns out, we are able to give complexity bounds for the sizes of the minimal (resp., maximal) elements which completely characterize the upward-closed (resp., downward-closed) solution spaces of upper-bound (resp., lower-bound) TPAs. For bipartite TPAs, it is shown that their solution spaces are not semilinear in general. We also extend our analysis to TPAs equipped with counters without zero-test capabilities.
---
paper_title: Linear Parametric Model Checking of Timed Automata

paper_content:

We present an extension of the model checker Uppaal capable of synthesizing linear parameter constraints for the correctness of parametric timed automata. The symbolic representation of the (parametric) state-space is shown to be correct. A second contribution of this paper is the identification of a subclass of parametric timed automata (L/U automata), for which the emptiness problem is decidable, contrary to the full class where it is know to be undecidable. Also we present a number of lemmas enabling the verification effort to be reduced for L/U automata in some cases. We illustrate our approach by deriving linear parameter constraints for a number of well-known case studies from the literature (exhibiting a flaw in a published paper).
---
paper_title: Parametric Optimization of Open Real-Time Systems

paper_content:

For controllable timed automata, a general parametric optimization framework based on automata-theory is proposed. The framework is general enough to incorporate both the parametric analysis problem and the controller synthesis problem of computer systems. We propose an algorithm for the construction of the characterization of the parameter constraints and controller synthesis, which in turn yields a linear programming solution to parametric optimization.
---
paper_title: Symbolic Techniques for Parametric Reasoning about Counter and Clock Systems

paper_content:

We address the problem of automatic analysis of parametric counter and clock automata. We propose a semi-algorithmic approach based on using (1) expressive symbolic representation structures called Parametric DBM's and (2) accurate extrapolation techniques allowing to speed up the reachability analysis and help its termination. The techniques we propose consist in guessing automatically the effect of iterating a control loop an arbitray number of times, and in checking that this guess is exact. Our approach can deal uniformly with systems that generate linear or nonlinear sets of configurations. We have implemented our techniques and experimented them on nontrivial examples such as a parametric timed version of the Bounded Retransmission Protocol.
---
paper_title: Supervisory control of timed discrete-event systems

paper_content:

The Ramadge-Wonham framework for control of discrete event systems is augmented with timing features by use of Ostroff's semantics for timed transition models. It is shown that the RW concept of controllability and the existence of maximally permissive supervisory controls can be suitably generalized. The enhanced setting admits subsystem composition and the concept of forcible event as an event that preempts the tick of a global clock. An example of a simple manufacturing cell illustrates how the new framework can be used to solve synthesis problems which may include logic-based, temporal and quantitative optimality specifications. >
---
paper_title: As Soon as Possible: Time Optimal Control for Timed Automata

paper_content:

In this work we tackle the following problem: given a timed automaton, and a target set F of configurations, restrict its transition relation in a systematic way so that from every state, the remaining behaviors reach F as soon as possible. This consists in extending the controller synthesis problem for timed automata, solved in [MPS95,AMPS98], to deal with quantitative properties of behaviors. The problem is formulated using the notion of a timed game automaton, and an optimal strategy is constructed as a fixed-point of an operator on the space of value functions defined on state-clock configurations.
---
paper_title: Supervisory Control of a Class of Discrete Event Processes

paper_content:

The paper studies the control of a class of discrete event processes, i.e., processes that are discrete, asynchronous and possibly nondeterministic. The controlled process is described as the generator of a formal language, while the controller, or supervisor, is constructed from a recognizer for a specified target language that incorporates the desired closed-loop system behavior. The existence problem for a supervisor is reduced to finding the largest controllable language contained in a given legal language. Two examples are provided.
---
paper_title: Parametric Optimization of Open Real-Time Systems

paper_content:

For controllable timed automata, a general parametric optimization framework based on automata-theory is proposed. The framework is general enough to incorporate both the parametric analysis problem and the controller synthesis problem of computer systems. We propose an algorithm for the construction of the characterization of the parameter constraints and controller synthesis, which in turn yields a linear programming solution to parametric optimization.
---
paper_title: Symbolic Controller Synthesis for Discrete and Timed Systems

paper_content:

This paper presents algorithms for the symbolic synthesis of discrete and real-time controllers. At the semantic level the controller is synthesized by finding a winning strategy for certain games defined by automata or by timed-automata. The algorithms for finding such strategies need, this way or another, to search the state-space of the system which grows exponentially with the number of components. Symbolic methods allow such a search to be conducted without necessarily enumerating the state-space. This is achieved by representing sets of states using formulae (syntactic objects) over state variables. Although in the worst case such methods are as bad as enumerative ones, many huge practical problems can be treated by fine-tuned symbolic methods. In this paper the scope of these methods is extended from analysis to synthesis and from purely discrete systems to real-time systems.
---
paper_title: Symbolic Model Checking for Real-Time Systems

paper_content:

Abstract We describe finite-state programs over real-numbered time in a guarded-command language with real-valued clocks or, equivalently, as finite automata with real-valued clocks. Model checking answers the question which states of a real-time program satisfy a branching-time specification (given in an extension of CTL with clock variables). We develop an algorithm that computes this set of states symbolically as a fixpoint of a functional on state predicates, without constructing the state space. For this purpose, we introduce a μ-calculus on computation trees over real-numbered time. Unfortunately, many standard program properties, such as response for all nonzeno execution sequences (during which time diverges), cannot be characterized by fixpoints: we show that the expressiveness of the timed μ-calculus is incomparable to the expressiveness of timed CTL. Fortunately, this result does not impair the symbolic verification of "implementable" real-time programs-those whose safety constraints are machine-closed with respect to diverging time and whose fairness constraints are restricted to finite upper bounds on clock values. All timed CTL properties of such programs are shown to be computable as finitely approximable fixpoints in a simple decidable theory.
---
paper_title: Automatic Verification of Real-time Systems with Discrete Probability Distributions

paper_content:

We consider the timed automata model of [3], which allows the analysis of real-time systems expressed in terms of quantitative timing constraints. Traditional approaches to real-time system description express the model purely in terms of nondeterminism; however, we may wish to express the likelihood of the system making certain transitions. In this paper, we present a model for real-time systems augmented with discrete probability distributions. Furthermore, using the algorithm of [5] with fairness, we develop a model checking method for such models against temporal logic properties which can refer both to timing properties and probabilities, such as, "with probability 0.6 or greater, the clock x remains below 5 until clock y exceeds 2".
---
paper_title: Model-checking for Probabilistic Real-time Systems

paper_content:

Model-checking is a method of verifying concurrent systems in which a state-graph model of the system behavior is compared with a temporal logic formula. This paper extends model-checking to stochastic real-time systems, whose behavior depends on probabilistic choice and quantitative time. The specification language is TCTL, a branching-time temporal logic for expressing real-time properties. We interpret the formulas of the logic over generalized semi-Markov processes. Our model can express constraints like “the delay between the request and the response is distributed uniformly between 2 to 4 seconds”.
---
paper_title: A really temporal logic

paper_content:

A real-time temporal logic for the specification of reactive systems is introduced. The novel feature of the logic, TPTL, is the adoption of temporal operators as quantifiers over time variables; every modality binds a variable to the time(s) it refers to. TPTL is demonstrated to be both a natural specification language and a suitable formalism for verification and synthesis. A tableau-based decision procedure and model-checking algorithm for TPTL are presented. Several generalizations of TPTL are shown to be highly undecidable. >
---
paper_title: Worst-case execution-time analysis for embedded real-time systems

paper_content:

In this article we give an overview of the worst-case execution time (WCET) analysis research performed by the WCET group of the ASTEC Competence Centre at Uppsala University. Knowing the WCET of a program is necessary when designing and verifying real-time systems. The WCET depends both on the program flow, such as loop iterations and function calls, and on hardware factors, such as caches and pipelines. WCET estimates should be both safe (no underestimation allowed) and tight (as little overestimation as possible). We have defined a modular architecture for a WCET tool, used both to identify the components of the overall WCET analysis problem, and as a starting point for the development of a WCET tool prototype. Within this framework we have proposed solutions to several key problems in WCET analysis, including representation and analysis of the control flow of programs, modeling of the behavior and timing of pipelines and other low-level timing aspects, integration of control flow information and low-level timing to obtain a safe and tight WCET estimate, and validation of our tools and methods. We have focussed on the needs of embedded real-time systems in designing our tools and directing our research. Our long-term goal is to provide WCET analysis as a part of the standard tool chain for embedded development (together with compilers, debuggers, and simulators). This is facilitated by our cooperation with the embedded systems programming-tools vendor IAR Systems.
---
paper_title: Numerical Coverage Estimation for the Symbolic Simulation of Real-Time Systems

paper_content:

Three numerical coverage metrics for the symbolic simulation of dense-time systems and their estimation methods are presented. Special techniques to derive numerical estimations of dense-time state-spaces have also been developed. Properties of the metrics are also discussed with respect to four criteria. Implementation and experiments are then reported.
---

Title: Formal verification of timed systems: a survey and perspective
Section 1: INTRODUCTION
Description 1: This section introduces the significance and challenges of formally verifying real-time systems and provides an overview of the paper's organization.

Section 2: MODELS
Description 2: This section discusses various models used in the formal verification of real-time systems, including linear versus branching time, discrete versus dense time, state-based versus event-driven models, timed automata, communicating timed automata, hybrid automata, logic formulas, timed process algebras, timed Petri nets, and graphical languages.

Section 3: VERIFICATION FRAMEWORK
Description 3: This section outlines the primary approaches to verifying timed systems, such as satisfiability checking, model checking, simulation, and theorem proving.

Section 4: REPRESENTATIONS OF STATE SPACES
Description 4: This section explores different data structures and techniques for representing state spaces in the verification process, including difference-bounded matrices, BDD-like data structures, and sets of constraints.

Section 5: CONSTRUCTION OF TIME-SPACE REPRESENTATIONS
Description 5: This section focuses on techniques for constructing time-space representations necessary to solve verification problems, including forward and backward analysis, compositional approaches, on-the-fly construction, and normalizations.

Section 6: REDUCTION TECHNIQUES
Description 6: This section reviews reduction methods to manage verification complexity, such as inactive variable elimination, partial-order reduction, internal transition bypassing, symmetry reduction, and approximation.

Section 7: TOOLS
Description 7: This section introduces various tools developed for the formal verification of timed systems, detailing their capabilities and features.

Section 8: OTHER ISSUES
Description 8: This section discusses additional topics relevant to formal verification of timed systems, including symbolic simulation, parametric analysis, controller synthesis, probabilistic analysis, and worst-case execution time (WCET) analysis.

Section 9: SUMMARY AND PERSPECTIVES
Description 9: This section summarizes the progress and future directions of formal verification for real-time systems, emphasizing the challenges and potential advancements in the field.