WWW.DISSERTATION.XLIBX.INFO
FREE ELECTRONIC LIBRARY - Dissertations, online materials
 
<< HOME
CONTACTS



Pages:   || 2 | 3 | 4 | 5 |   ...   | 23 |

«TECHNIQUES FOR AUTOMATIC VERIFICATION OF REAL-TIME SYSTEMS a dissertation submitted to the department of computer science and the committee on ...»

-- [ Page 1 ] --

TECHNIQUES FOR AUTOMATIC VERIFICATION OF

REAL-TIME SYSTEMS

a dissertation

submitted to the department of computer science

and the committee on graduate studies

of stanford university

in partial fulfillment of the requirements

for the degree of

doctor of philosophy

By

Rajeev Alur

August 1991

c Copyright 1991 by Rajeev Alur

All Rights Reserved

ii

I certify that I have read this dissertation and that in my

opinion it is fully adequate, in scope and in quality, as a dissertation for the degree of Doctor of Philosophy.

David Dill (Principal Advisor) I certify that I have read this dissertation and that in my opinion it is fully adequate, in scope and in quality, as a dissertation for the degree of Doctor of Philosophy.

Zohar Manna (Coadvisor) I certify that I have read this dissertation and that in my opinion it is fully adequate, in scope and in quality, as a dissertation for the degree of Doctor of Philosophy.

Moshe Vardi

Approved for the University Committee on Graduate Studies:

Dean of Graduate Studies iii Abstract This thesis proposes formal methods for speci cation and automatic veri cation of nitestate real-time systems. The traditional formalisms for reasoning about programs abstract away from quantitative time and, consequently, are inadequate for reasoning about realtime systems. We extend the methods based on automata and temporal logics to allow them to model timing delays and to verify real-time requirements.

We introduce timed automata to model the behavior of real-time systems over time.

Our de nition provides a simple, and yet powerful, way to annotate state-transition graphs with timing constraints using nitely many real-valued clocks. A timed automaton accepts timed words | strings in which a real-valued time of occurrence is associated with each symbol. We study timed automata from the perspective of formal language theory: we consider closure properties, decision problems, and subclasses.

We present two conservative extensions of the existing temporal logics to allow them to specify timing properties. The metric interval temporal logic (MITL) uses linear-time semantics, and its syntax allows temporal operators to be subscripted with intervals restricting their scope in time. The timed computation tree logic (TCTL) uses branching-time semantics, and its syntax provides access to time through a novel kind of time quanti er.

In the proposed veri cation method, a nite-state system is modeled as a composition of timed automata, and the correctness is speci ed either as a deterministic timed automaton, or as a formula of MITL or TCTL. In each case we develop an algorithm for model checking. The distinguishing feature of our work is the use of the set of reals to model time we argue that the denseness of the time domain is crucial for modeling event-driven asynchronous systems. The thesis also clari es the relationship between di erent models and logics for real-time, and answers some basic questions regarding complexity, decidability, and expressiveness.

iv Acknowledgments First of all I thank my advisors, David Dill and Zohar Manna, for o ering me technical, nancial, and moral support during the last four years. My reading committee comprised of David, Zohar, and Moshe Vardi, and I consider myself fortunate that I had access to valuable guidance from all three of them. I am also thankful to them for their critical reading of the draft. Zohar introduced me to temporal logics, and directed me to the relatively unexplored area of real-time logics. He also made possible an extremely productive visit to the Weizmann Institute in Israel. Much of the research reported in this thesis is inspired by my discussions with David about his ideas on coupling automata with timing constraints.

Moshe is one of the leading proponents of the automata-theoretic approach to veri cation, and his expertise on the subject has been very useful to me.

It has been a great pleasure for me to work closely with Tom Henzinger. We learned to do research together we solved many problems together it would be futile to pinpoint his

innumerable contributions towards my work. Special thanks also go to my other colleagues:

Costas Courcoubetis and Tomas Feder. Costas's unbounded enthusiasm to attack new problems has been a source of inspiration to me. The decision procedure for MITL builds upon some insightful observations made by Tomas.

I have had the opportunity to discuss my research with many scientists at Stanford, at IBM Almaden Research Center, and at various conferences and seminars. I thank all of them for being helpful and encouraging. I am particularly grateful to Joe Halpern, Dinesh Katiyar, John Mitchell, Amir Pnueli, Howard Wong-Toi, and Mihalis Yannakakis.

My allegiance to computer science is mainly due to the excellent education I received at the Indian Institute of Technology at Kanpur, and I am thankful to the faculty on its Computer Science Department. Also this thesis would not exist without the love and support of my family, especially, my parents. I would also like to use this opportunity to thank all my friends on Stanford campus because of them my stay here has been very enjoyable and memorable.

–  –  –





Introduction

1.1 Motivation With the increasing use of computers in safety-critical applications there is a pressing need for designing more reliable systems. As a result, developing formal methods for the design and analysis of concurrent systems has been an active area of computer science research. The conventional approach to testing the correctness of a system involves simulation on some test cases. This method is quite inadequate for developing bug-free complex concurrent systems. One approach to assure correctness is to employ automatic veri cation methods.

A veri cation formalism comprises of

1. A formal semantics which assigns mathematical meanings to system components and correctness criteria.

2. A language for describing the essential aspects of the system components, and constructs for combining them.

3. A speci cation language for expressing the correctness requirements.

4. A veri cation algorithm to check if the correctness criteria are ful lled in every possible execution of the system.

In this thesis we provide formalisms for automatic veri cation of nite-state real-time systems.

The class of systems to which our methods are applicable includes asynchronous circuits, communication protocols, and controllers (such as a ight controller, or a controller for a

CHAPTER 1. INTRODUCTION 2

manufacturing plant). The essential characteristics of such systems are:

Finite-state: The system can be in one of the nitely many discrete states. If we focus only on the control aspect of the system, ignoring the computational aspect, then this is an useful abstraction in many cases. State-transitions are triggered by events which are instantaneous.

Reactive: The system constantly interacts with the environment reacting to stimuli.

So we are interested in the ongoing behavior over time. This is quite unlike the traditional \transformational" view of the programs where the functional relationship between the input state and the output state de nes the meaning of a program. The system comprises of a collection of components operating concurrently and communicating with each other.

Real-time: The correctness of the system depends on the actual magnitudes of the timing delays of the components. This is obviously the case when the system needs to meet hard real-time deadlines: the system needs to respond to a stimulus within a certain xed time bound. Also there are cases when the logical correctness of the system depends on the lengths of various delays.

Real-time systems are used in safety-critical applications such as controllers for nuclear plants. Failures in such systems can be very expensive and even life-threatening. Because of the intricacies of the timing relationships, real-time systems are quite hard to model, specify, and design. Consequently, there is a great demand for formal methods applicable to real-time systems.

1.2 Background: formalisms for qualitative reasoning Several di erent formalisms have been proposed to reason about reactive systems. These include Petri nets, process algebras, temporal logics, automata-theoretic techniques, and partial-order models.

These methodologies

Abstract

from time, retaining the information about the causality and/or the temporal order of occurrence of observable events. Even though there is no general agreement about what is the right semantics of concurrency, some of these techniques have provided the foundations for building veri ers for hardware and communication protocols, and some have suggested structured disciplines for writing concurrent programs. We

CHAPTER 1. INTRODUCTION 3

will brie y review these approaches the methods for automatic veri cation of nite-state systems are of main interest to us.

1.2.1 Temporal logics The use of temporal logic as a formalism for specifying the behavior of a reactive system over time was rst proposed by Pnueli in 1977 Pnu77]. The subject has been extensively studied since then BMP81, MP81, EC82, OL82, Lam83, MW84, BKP86, CES86, Pnu86, MP89, Lam91]. Temporal logic is a modal logic with modalities such as 3 meaning \eventually", and 2 meaning \always" (see Eme90] for an overview). Temporal logics provide a succinct and natural way of expressing the desired temporal requirements. Two types of temporal logics have been proposed: linear-time and branching-time.

In the linear-time framework, a system is viewed as a set of computations, where each computation is a sequence of system-states recording all the transitions over the course of time. A linear temporal logic formula is interpreted over such state sequences Pnu77, OL82]. The branching-time logics, on the other hand, are interpreted over tree models BMP81, EC82, EL85]. The system is viewed as a nitely-branching tree the paths in the tree correspond to the possible executions of the system.

In the traditional approach to veri cation of concurrent programs, the correctness of the program is expressed by a formula in rst-order temporal logic. The veri cation problem reduces to proving a theorem in a deductive system. For example, Manna and Pnueli MP89] have developed the model of fair transition systems to describe the implementation, and give a proof system to verify temporal logic speci cations. Though the technique is quite general, constructing a proof needs to be done manually and requires a great deal of understanding of the program. The only extent of automation one can hope for is to have the proof checked by a machine and possibly to have some limited heuristics in nding the proof.

Model checking provides a di erent approach to checking properties of nite-state systems CES86, LP85, EL85, BCD+ 90, GW91]. In this approach, the global state-transition graph is viewed as a nite Kripke structure (with fairness requirements, if necessary). The speci cation of the system is given as a formula of a propositional temporal logic. The model-checking algorithm then decides whether the system meets the speci cation in all possible scenarios. For the linear-time case, the complexity of model-checking is linear in the size of the state-transition graph and exponential in the size of the speci cation, and in

CHAPTER 1. INTRODUCTION 4

the branching-time case, it is linear both in the size of the state-transition graph and the length of the temporal logic speci cation. Various aspects of the model-checking problem for the logic CTL EC82] have been studied. This approach has been successfully applied to verify circuits and protocols, and to nd bugs in previously-published, non-trivial protocols and circuits CES86, BCDM86].

The model-checking approach to program veri cation is probably the most exciting advance in the theory of program correctness in recent years. It has been extended to probabilistic systems Var85, PZ86, CY88], to real-time systems EMSS89, AH89, ACD90, Lew90, HLP90], and to probabilistic real-time systems HJ89, ACD91a, ACD91b].

The main di culty in using model-checking approach is the state-explosion problem: the size of the global state-transition graph grows exponentially with the number of components in the system. This problem has received great attention recently, and di erent ways to cope with the problem have been proposed BCD+ 90, God90, GW91].

1.2.2 Automata-theoretic approach A related approach to veri cation of nite-state systems uses !-automata WVS83, Var87].

The computation of a reactive program is viewed as an in nite word over the alphabet of events (or states). This gives rise to an intimate connection between reasoning about reactive systems and the formal language theory. A system is modeled as an automaton generating in nite sequences which correspond to the possible computations of the system.

The automata over in nite words were rst studied by Buchi in relation to the theory S1S, the second order monadic theory of natural numbers with successor Buc62]. Buchi automata and their variants have been studied in great detail since then Cho74, Mul63, McN66], leading to a beautiful theory of !-regular languages (see Tho90] for an overview).

In the automata-theoretic framework, a system is modeled as a composition of several automata. The implementation automaton I is the product of these automata, and acts as a generator. The speci cation is given as another automaton S which acts as an acceptor. Alternatively, from a linear temporal logic speci cation, one can construct an automaton which accepts all the computations that satisfy the given formula. The implementation is correct i every behavior generated by I is accepted by S. Thus the veri cation problem reduces to the language inclusion problem. Consequently the known e ective constructions for intersection, complementation, and test for emptiness can be used

CHAPTER 1. INTRODUCTION 5

as a basis for automatic veri cation. Checking for language inclusion involves complementing the speci cation automaton which can be expensive, particularly for nondeterministic automata SVW87, Saf88]. Alternative ways which use simulation relations have been proposed DHW91].



Pages:   || 2 | 3 | 4 | 5 |   ...   | 23 |


Similar works:

«MISSION-WITH IN INNER-SOUTH MANCHESTER AN AUTO-ETHNOGRAPHIC EXPLORATION OF PRESENCEAMONG AND PROJECT-PRAXIS WITH LOCAL COMMUNITY AS A MODEL OF URBAN MISSION, WITH PARTICULAR REFERENCE TO THE COMMUNITY GROUP CARISMA. ! by PAUL BRIAN KEEBLE A thesis submitted to The University of Birmingham for the degree of MASTER OF PHILOSOPHY Urban Theology Unit, Sheffield Department of Theology and Religion College of Arts and Law The University of Birmingham June 2013 University of Birmingham Research...»

«John Howard Yoder on Christian Nonviolence and the Haustafeln by In-Yong Lee Graduate Program in Religion Duke University Date: _Approved: _ Stanley Hauerwas, Supervisor _ Amy Laura Hall _ Allen Verhey _ Susan Eastman _ Douglas Campbell Dissertation submitted in partial fulfillment of the requirements for the degree of Doctor of Philosophy in the Graduate Program in Religion in the Graduate School of Duke University ABSTRACT John Howard Yoder on Christian Nonviolence and the Haustafeln by...»

«Statistical Mechanics and the Asymmetry of Counterfactual Dependence∗ Adam Elga MIT Dept. of Linguistics and Philosophy adam@mit.edu Forthcoming, Philosophy of Science (supp. vol., PSA 2000) Abstract In “Counterfactual Dependence and Time’s Arrow,” David Lewis defends an analysis of counterfactuals intended to yield the asymmetry of counterfactual dependence: that later affairs depend counterfactually on earlier ones, and not the other way around. I argue that careful attention to the...»

«Der Sechste Zhva dmar pa Chos kyi dbang phyug (1584–1630) und sein Reisebericht aus den Jahren 1629/1630: Studie, Edition und Übersetzung Inaugural-Dissertation zur Erlangung des Doktorgrades der Philosophie an der Ludwig-Maximilians-Universität München vorgelegt von: Navina Lamminger Datum der mündlichen Prüfung: 28. Januar 2013 Gutachter: Prof. Dr. Franz-Karl Ehrhard Prof. Dr. Jens-Uwe Hartmann Inhaltsverzeichnis Danksagung vii 1. Allgemeine Einführung und Aufbau der Arbeit 1 1.1...»

«Department of Educational Administration Doctoral Degree K-12 Educational Administration Student / Faculty Handbook For accepted / enrolled students Last Updated: 08/20/2015 TABLE OF CONTENTS I. Program Overview • PhD Program Mission and Philosophy • PhD Program Expectations II. Program Components Credit Accrual Preliminary • Exam Comprehensive • Exam Research Practicum • Dissertation Proposal • Dissertation Defense • III. Degree Requirements Residency Requirement • Time...»

«EVALUATION OF PEARL MILLET FORAGE By Fadi M. Hassanat Department of Animal Science McGill University Montreal, Quebec November, 2007 A Thesis Submitted for the Faculty of Graduate and Postdoctoral Studies in partial fulfilment of the requirements of the degree of Doctor in Philosophy Ⓒ Fadi Hassanat, 2007 ABSTRACT This research evaluated millet as forage source for ruminants. Four studies were conducted using two cultivars of forage millet [i.e. brown midrib (BM) and regular (RM)]. The first...»

«Investigating the causes of the decline of the urban House Sparrow Passer domesticus population in Britain Kate E. Vincent (BSc.) A thesis submitted for the degree of Doctor of Philosophy Awarded by De Montfort University Funded by English Nature, RSPB and De Montfort University October 2005 ABSTRACT In Britain and parts of northwest Europe, House Sparrow Passer domesticus populations have declined markedly in urban-suburban landscapes since the mid-1980s. Little is known about the demographic...»

«EVALUATING THE IMPACTS OF ENTERPRISE RESOURCE PLANNING ON ORGANIZATIONAL PERFORMANCE FOR SMALL TO MEDIUM ENTERPRISES IN MANUFACTURING A Dissertation Presented to The Academic Faculty by Arya Sedehi In Fulfillment of the Requirements for the Degree Doctor of Philosophy in the School of Building Construction Georgia Institute of Technology May 2015 COPYRIGHT © 2015 BY ARYA SEDEHI EVALUATING THE IMPACTS OF ENTERPRISE RESOURCE PLANNING ON ORGANIZATIONAL PERFORMANCE FOR SMALL TO MEDIUM ENTERPRISES...»

«A MODEL BASED APPROACH TO THE ANALYSIS OF INTERSECTION CONFLICTS AND COLLISION AVOIDANCE SYSTEMS by Kazutoshi Nobukawa A dissertation submitted in partial fulfillment of the requirements for the degree of Doctor of Philosophy (Mechanical Engineering) in The University of Michigan 2011 Doctoral Committee: Professor Timothy J. Gordon, Chair Professor Jessy W. Grizzle Professor Huei Peng Professor Noel C. Perkins © Kazutoshi Nobukawa 2011 DEDICATION To my parents. ii ACKNOWLEDGMENTS This...»

«PHOTO-DYNAMIC XPS FOR INVESTIGATING PHOTOINDUCED VOLTAGE CHANGES IN SEMICONDUCTING MATERIALS A DISSERTATION SUBMITTED TO THE DEPARTMENT OF CHEMISTRY AND THE GRADUATE SCHOOL OF ENGINEERING AND SCIENCE OF BILKENT UNIVERSITY IN PARTIAL FULFILLMENT OF THE REQUIREMENTS FOR THE DEGREE OF DOCTOR OF PHILOSOPHY By HİKMET SEZEN December, 2011 I I certify that I have read this thesis and that in my opinion is it is fully adequate, in scope and in quality, as a dissertation for the degree of the doctor of...»

«Stony Brook University The official electronic file of this thesis or dissertation is maintained by the University Libraries on behalf of The Graduate School at Stony Brook University. © Allll Riightts Reserved by Autthor. © A R gh s Reserved by Au hor Ecogeographic Variation in Neandertal Dietary Habits: Evidence from Microwear Texture Analysis A Dissertation Presented by Sireen El Zaatari to The Graduate School in Patrial fulfillment of the Requirements for the Degree of Doctor of...»

«IN VIVO DOSE RECONSTRUCTION USING A 2D DOSIMETER VIA TRANSIT DOSIMETRY By HEETEAK CHUNG A DISSERTATION PRESENTED TO THE GRADUATE SCHOOL OF THE UNIVERSITY OF FLORIDA IN PARTIAL FULFILLMENT OF THE REQUIREMENTS FOR THE DEGREE OF DOCTOR OF PHILOSOPHY UNIVERSITY OF FLORIDA 2009 1 © 2009 by Heeteak Chung 2 To my parents. it has been a long road. 3 ACKNOWLEDGMENTS The completion of Ph.D. program is a huge milestone in my life. I could not have done it without the help from many people that have...»





 
<<  HOME   |    CONTACTS
2016 www.dissertation.xlibx.info - Dissertations, online materials

Materials of this site are available for review, all rights belong to their respective owners.
If you do not agree with the fact that your material is placed on this site, please, email us, we will within 1-2 business days delete him.