356 Result(s)
within
Conference Paper
**aochen **
English
-
Chapter and Conference Paper
Specifying communicating systems with temporal logic
We introduce a temporal logic for specifying external behaviour of systems. Predicates INT, PASS and CLD are the primitives of the logic to record temporal states of a communication channel, intending to do a com...
-
Chapter and Conference Paper
A Model for Synchronous Switching Circuits and its Theory of Correctness
Following Bryant [2], an algorithm is given for translating a switching circuit design into a program which simulates its dynamic behaviour. A theory of assertions based on Dijkstra [4] and UNITY [3] is then d...
-
Chapter and Conference Paper
Duration specifications for shared processors
We present a specification oriented real-time semantics for real-time programs consisting of communicating sequential processes running on a shared processor configuration. The semantics, which is given in Dur...
-
Chapter and Conference Paper
Semantics and completeness of Duration Calculus
Duration Calculus was introduced in [1] as a notation to specify real-time systems, and as a calculus to verify theorems about such systems. Its distinctive feature is reasoning about durations of states within a...
-
Chapter and Conference Paper
Decidability and undecidability results for duration calculus
-
Chapter and Conference Paper
Duration Calculi: An overview
The Duration Calculi are calculi for designing real-time software embedded systems. The Calculi overviewed in the paper include the Duration Calculus, the Extended Duration Calculus, the Mean Value Calculus an...
-
Chapter and Conference Paper
An extended duration calculus for hybrid real-time systems
Duration Calculus is a real-time interval logic which can be used to specify and reason about timing and logical constraints on discrete states in a dynamic system. It has been used to specify and verify desig...
-
Chapter and Conference Paper
Formal design of hybrid systems
A hybrid system is a system containing both of time-evolving components and event-driven components. A formal approach is explored in this paper, based on Extended Duration Calculus (EDC), for the development of ...
-
Chapter and Conference Paper
A formal proof of the Deadline Driven scheduler
This paper presents an approach to formalizing and proving real-time properties of schedulers. The formal logic that we propose to use is the Duration Calculus [1], and the scheduler that we select here to ser...
-
Chapter and Conference Paper
Linear duration invariants
This paper is to present an algorithm to decide whether a real-time system satisfies a set of invariants which are constructed from linear inequalities of integrated durations of system states. Real-time syste...
-
Chapter and Conference Paper
A duration calculus with infinite intervals
This paper introduces infinite intervals into the Duration Calculus [33]. The extended calculus defines a state duration over an infinite interval by a property which specifies the limit of the state duration ...
-
Chapter and Conference Paper
A formal description of hybrid systems
Inspired by [He94], a language to describe hybrid systems, i.e. networks of communicating discrete and continuous processes, is proposed. A semantics of the language is given in Extended Duration Calculus [ZRH...
-
Chapter and Conference Paper
An Adequate First Order Interval Logic
This paper introduces left and right neighbourhoods as primitive interval modalities to deFine other unary and binary modalities of intervals in a first order logic with interval length. A complete first order lo...
-
Chapter and Conference Paper
Duration Calculus, a Logical Approach to Real-Time Systems
The Duration Calculus (DC) represents a logical approach to formal design of real-time systems. DC is based on interval logic, and uses real numbers to model time, and Boolean-valued (i.e. 0,1-valued) function...
-
Chapter and Conference Paper
Completeness of Neighbourhood Logic
This paper presents a completeness result for a first-order interval temporal logic, called Neighbourhood Logic (NL) which has two neighbourhood modalities. NL can support the specification of liveness and fai...
-
Chapter and Conference Paper
Sign Correlation Detector for Blind Image Watermarking in the DCT Domain
Digital watermarking is a key technique for protecting intellectual property of digital media. Due to the ability to detect watermark without the original image, blind watermarking is very useful if there are ...
-
Chapter and Conference Paper
Evaluation of the Image Degradation for a Typical Watermarking Algorithm in the Block-DCT Domain
Digital watermarking is a key technique for protecting intellectual property of digital media. As a number of methods have been proposed in recent years to embed watermarks in images for various applications, ...
-
Chapter and Conference Paper
Optimization of Spatial Joins on Mobile Devices
Mobile devices like PDAs are capable of retrieving information from various types of services. In many cases, the user requests cannot directly be processed by the service providers, if their hosts have limite...
-
Chapter and Conference Paper
Minimum-Cost Optimization in Multicommodity Logistic Chain Network
This paper presents a method of modeling and solving a very complicated real logistic problem in the management of transportation and sales. The problem to be addressed is a large-scale multicommodity, multi-s...
-
Chapter and Conference Paper
Towards an Agile Process for Building Software Product Lines
Software product lines are sets of software systems that share common features. Product lines are built as if they were a family of products, identifying those features that change and those that can be reused...
