Please use this identifier to cite or link to this item:
Title: Verification of timed process algebra and beyond
Keywords: Timed Process Algebra,Formal Verification, Concurrent and Realtime Systems, Constraint Logic Programming, Refinement, Job-shop Scheduling Problem
Issue Date: 21-Apr-2011
Source: ZHANG XIAN (2011-04-21). Verification of timed process algebra and beyond. ScholarBank@NUS Repository.
Abstract: The design and verification of real-time systems are notoriously difficult problems. In this thesis, we study the modeling and verification of real-time systems using timed process algebra, particularly Timed CSP. Timed CSP is an elegant and intuitive modeling language for real-time systems. It has been widely accepted and applied to a wide arrange of systems. However the verification support for Timed CSP is limited. The first part of the thesis is to develop a reasoning mechanism for Timed CSP by using Constraint Logic Programming (CLP) as underlying reasoning engine. Our approach starts with a systematic translation of the syntax of Timed CSP into CLP. Powerful constraint solver like CLP(R) is then used to prove traditional safety properties and beyond, e.g., reachability, deadlock-freeness, timewise refinement relationship, lower or upper bound of a time interval, etc. Counterexamples are generated when properties are not satisfied. Based on this translation, an interactive tool, named HORAE, which provides composing and reasoning of Timed CSP process descriptions is developed. The second contribution of this thesis is the proposal of a formal language, named Timed Planning, for modeling real-time systems. Timed Planning extends Timed CSP with the capability of stating complicated timing behaviors. A Timed Planning model is made up of a hierarchical timed process and a set of constraints over processes, events and the data variables which are the requirements that the process should satisfy. Particularly, each process is associated with a set of localized timing/untiming requirements with keyword Where which can be specified in a compositional way. The full syntax and operational semantics of Timed Planning are formally defined. A reasoning mechanism for the Timed Planning is hence developed based on CLP by extending our reasoning engine HORAE. Feasibility checking and various property verification can be applied to check systems modeled in Timed Planning. To show the usefulness of Timed Planning, we apply Timed Planning and HORAE to solve three different application domains. Firstly, we use Timed Planning to model classical jobshop scheduling problems, in order to find a shortest execution in terms of elapsed time. In this case, the job-shop scheduling problem can be reduced to a problem of finding a complete execution (an execution that terminates) with the minimum execution time. Secondly, security protocols are widely used for secure application-level data transport crossing distributed systems. Designing security protocols is notoriously difficult and error-prone. The new challenges raise when different timing aspects are required in the security protocol design, such as timestamps, delays, timeout and a set of timing constraints. We focus on using Timed Planning to accomplish the modeling and analyzing of timed security protocols. The use of explicit timing information allows us to specify security protocols with timestamps, timeout and retransmissions which can be naturally modeled using Timed Planning specification. In the timing analysis, we could verify timed non-injective agreement authentication property which can be easily extended to other authentication property verification. Thirdly, pervasive computing environments encompass a spectrum of computation and communication devices that seamlessly augment human thoughts and activities. They have been used to assist elders with mild dementia to improve their level of independence and quality of life through cognitive reinforcement. To support formal analysis, we propose to build a context-aware reminding framework for elders living at home using Timed Planning specification. Then we demonstrate the effectiveness of formal methods via modeling and verifying an integrated smart space reminding system for monitoring and assisting people with mild dementia in the nursing home.
Appears in Collections:Ph.D Theses (Open)

Show full item record
Files in This Item:
File Description SizeFormatAccess SettingsVersion 
ZhangXian.pdf1.02 MBAdobe PDF



Page view(s)

checked on Dec 18, 2017


checked on Dec 18, 2017

Google ScholarTM


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.