---
_id: '4232'
author:
- first_name: Harold
full_name: Harold Vladar
id: 2A181218-F248-11E8-B48F-1D18A9856A87
last_name: Vladar
orcid: 0000-0002-5985-7653
citation:
ama: Vladar H. *Stochasticity and Variability in the Dynamics and Genetics of
Populations*. Faculty of mathematical and natural sciences, University of Groningen;
2009. doi:3811
apa: Vladar, H. (2009). *Stochasticity and Variability in the dynamics and genetics
of populations*. Faculty of mathematical and natural sciences, University of
Groningen. https://doi.org/3811
chicago: Vladar, Harold. *Stochasticity and Variability in the Dynamics and Genetics
of Populations*. Faculty of mathematical and natural sciences, University of
Groningen, 2009. https://doi.org/3811.
ieee: H. Vladar, *Stochasticity and Variability in the dynamics and genetics of
populations*. Faculty of mathematical and natural sciences, University of Groningen,
2009.
ista: Vladar H. 2009. Stochasticity and Variability in the dynamics and genetics
of populations, Faculty of mathematical and natural sciences, University of Groningen,p.
mla: Vladar, Harold. *Stochasticity and Variability in the Dynamics and Genetics
of Populations*. Faculty of mathematical and natural sciences, University of
Groningen, 2009, doi:3811.
short: H. Vladar, Stochasticity and Variability in the Dynamics and Genetics of
Populations, Faculty of mathematical and natural sciences, University of Groningen,
2009.
date_created: 2018-12-11T12:07:44Z
date_published: 2009-01-01T00:00:00Z
date_updated: 2019-04-26T07:22:41Z
day: '01'
doi: '3811'
extern: 1
month: '01'
publication_status: published
publisher: Faculty of mathematical and natural sciences, University of Groningen
publist_id: '1883'
quality_controlled: 0
status: public
title: Stochasticity and Variability in the dynamics and genetics of populations
type: dissertation
year: '2009'
...
---
_id: '4415'
abstract:
- lang: eng
text: 'Many computing applications, especially those in safety critical embedded
systems, require highly predictable timing properties. However, time is often
not present in the prevailing computing and networking abstractions. In fact,
most advances in computer architecture, software, and networking favor average-case
performance over timing predictability. This thesis studies several methods for
the design of concurrent and/or distributed embedded systems with precise timing
guarantees. The focus is on flexible and compositional methods for programming
and verification of the timing properties. The presented methods together with
related formalisms cover two levels of design: (1) Programming language/model
level. We propose the distributed variant of Giotto, a coordination programming
language with an explicit temporal semantics—the logical execution time (LET)
semantics. The LET of a task is an interval of time that specifies the time instants
at which task inputs and outputs become available (task release and termination
instants). The LET of a task is always non-zero. This allows us to communicate
values across the network without changing the timing information of the task,
and without introducing nondeterminism. We show how this methodology supports
distributed code generation for distributed real-time systems. The method gives
up some performance in favor of composability and predictability. We characterize
the tradeoff by comparing the LET semantics with the semantics used in Simulink.
(2) Abstract task graph level. We study interface-based design and verification
of applications represented with task graphs. We consider task sequence graphs
with general event models, and cyclic graphs with periodic event models with jitter
and phase. Here an interface of a component exposes time and resource constraints
of the component. Together with interfaces we formally define interface composition
operations and the refinement relation. For efficient and flexible composability
checking two properties are important: incremental design and independent refinement.
According to the incremental design property the composition of interfaces can
be performed in any order, even if interfaces for some components are not known.
The refinement relation is defined such that in a design we can always substitute
a refined interface for an abstract one. We show that the framework supports independent
refinement, i.e., the refinement relation is preserved under composition operations.'
acknowledgement: 978-0-549-83480-9
author:
- first_name: Slobodan
full_name: Matic, Slobodan
last_name: Matic
citation:
ama: Matic S. *Compositionality in Deterministic Real-Time Embedded Systems*.
University of California, Berkeley; 2008:1-148.
apa: Matic, S. (2008). *Compositionality in deterministic real-time embedded systems*
(pp. 1–148). University of California, Berkeley.
chicago: Matic, Slobodan. *Compositionality in Deterministic Real-Time Embedded
Systems*. University of California, Berkeley, 2008.
ieee: S. Matic, *Compositionality in deterministic real-time embedded systems*.
University of California, Berkeley, 2008, pp. 1–148.
ista: Matic S. 2008. Compositionality in deterministic real-time embedded systems,
University of California, Berkeley,p.
mla: Matic, Slobodan. *Compositionality in Deterministic Real-Time Embedded Systems*.
University of California, Berkeley, 2008, pp. 1–148.
short: S. Matic, Compositionality in Deterministic Real-Time Embedded Systems, University
of California, Berkeley, 2008.
date_created: 2018-12-11T12:08:44Z
date_published: 2008-01-01T00:00:00Z
date_updated: 2019-01-24T13:19:54Z
day: '01'
extern: 1
month: '01'
page: 1 - 148
publication_status: published
publisher: University of California, Berkeley
publist_id: '316'
quality_controlled: 0
status: public
title: Compositionality in deterministic real-time embedded systems
type: dissertation
year: '2008'
...
---
_id: '4409'
abstract:
- lang: eng
text: |-
Models of timed systems must incorporate not only the sequence of system events, but the timings of these events as well to capture the real-time aspects of physical systems. Timed automata are models of real-time systems in which states consist of discrete locations and values for real-time clocks. The presence of real-time clocks leads to an uncountable state space. This thesis studies verification problems on timed automata in a game theoretic framework.
For untimed systems, two systems are close if every sequence of events of one system is also observable in the second system. For timed systems, the difference in timings of the two corresponding sequences is also of importance. We propose the notion of bisimulation distance which quantifies timing differences; if the bisimulation distance between two systems is epsilon, then (a) every sequence of events of one system has a corresponding matching sequence in the other, and (b) the timings of matching events in between the two corresponding traces do not differ by more than epsilon. We show that we can compute the bisimulation distance between two timed automata to within any desired degree of accuracy. We also show that the timed verification logic TCTL is robust with respect to our notion of quantitative bisimilarity, in particular, if a system satisfies a formula, then every close system satisfies a close formula.
Timed games are used for distinguishing between the actions of several agents, typically a controller and an environment. The controller must achieve its objective against all possible choices of the environment. The modeling of the passage of time leads to the presence of zeno executions, and corresponding unrealizable strategies of the controller which may achieve objectives by blocking time. We disallow such unreasonable strategies by restricting all agents to use only receptive strategies --strategies which while not being required to ensure time divergence by any agent, are such that no agent is responsible for blocking time. Time divergence is guaranteed when all players use receptive strategies. We show that timed automaton games with receptive strategies can be solved by a reduction to finite state turn based game graphs. We define the logic timed alternating-time temporal logic for verification of timed automaton games and show that the logic can be model checked in EXPTIME. We also show that the minimum time required by an agent to reach a desired location, and the maximum time an agent can stay safe within a set of locations, against all possible actions of its adversaries are both computable.
We next study the memory requirements of winning strategies for timed automaton games. We prove that finite memory strategies suffice for safety objectives, and that winning strategies for reachability objectives may require infinite memory in general. We introduce randomized strategies in which an agent can propose a probabilistic distribution of moves and show that finite memory randomized strategies suffice for all omega-regular objectives. We also show that while randomization helps in simplifying winning strategies, and thus allows the construction of simpler controllers, it does not help a player in winning at more states, and thus does not allow the construction of more powerful controllers.
Finally we study robust winning strategies in timed games. In a physical system, a controller may propose an action together with a time delay, but the action cannot be assumed to be executed at the exact proposed time delay. We present robust strategies which incorporate such jitters and show that the set of states from which an agent can win robustly is computable.
author:
- first_name: Vinayak
full_name: Prabhu, Vinayak S
last_name: Prabhu
citation:
ama: Prabhu V. *Games for the Verification of Timed Systems*. University of
California, Berkeley; 2008:1-137.
apa: Prabhu, V. (2008). *Games for the verification of timed systems* (pp.
1–137). University of California, Berkeley.
chicago: Prabhu, Vinayak. *Games for the Verification of Timed Systems*. University
of California, Berkeley, 2008.
ieee: V. Prabhu, *Games for the verification of timed systems*. University
of California, Berkeley, 2008, pp. 1–137.
ista: Prabhu V. 2008. Games for the verification of timed systems, University of
California, Berkeley,p.
mla: Prabhu, Vinayak. *Games for the Verification of Timed Systems*. University
of California, Berkeley, 2008, pp. 1–137.
short: V. Prabhu, Games for the Verification of Timed Systems, University of California,
Berkeley, 2008.
date_created: 2018-12-11T12:08:42Z
date_published: 2008-09-01T00:00:00Z
date_updated: 2019-01-24T13:19:52Z
day: '01'
extern: 1
month: '09'
page: 1 - 137
publication_status: published
publisher: University of California, Berkeley
publist_id: '319'
quality_controlled: 0
status: public
title: Games for the verification of timed systems
type: dissertation
year: '2008'
...
---
_id: '4524'
abstract:
- lang: eng
text: |-
Complex requirements, time-to-market pressure and regulatory constraints have made the designing of embedded systems extremely challenging. This is evident by the increase in effort and expenditure for design of safety-driven real-time control-dominated applications like automotive and avionic controllers. Design processes are often challenged by lack of proper programming tools for specifying and verifying critical requirements (e.g. timing and reliability) of such applications. Platform based design, an approach for designing embedded systems, addresses the above concerns by separating requirement from architecture. The requirement specifies the intended behavior of an application while the architecture specifies the guarantees (e.g. execution speed, failure rate etc). An implementation, a mapping of the requirement on the architecture, is then analyzed for correctness. The orthogonalization of concerns makes the specification and analyses simpler. An effective use of such design methodology has been proposed in Logical Execution Time (LET) model of real-time tasks. The model separates the timing requirements (specified by release and termination instances of a task) from the architecture guarantees (specified by worst-case execution time of the task).
This dissertation proposes a coordination language, Hierarchical Timing Language (HTL), that captures the timing and reliability requirements of real-time applications. An implementation of the program on an architecture is then analyzed to check whether desired timing and reliability requirements are met or not. The core framework extends the LET model by accounting for reliability and refinement. The reliability model separates the reliability requirements of tasks from the reliability guarantees of the architecture. The requirement expresses the desired long-term reliability while the architecture provides a short-term reliability guarantee (e.g. failure rate for each iteration). The analysis checks if the short-term guarantee ensures the desired long-term reliability. The refinement model allows replacing a task by another task during program execution. Refinement preserves schedulability and reliability, i.e., if a refined task is schedulable and reliable for an implementation, then the refining task is also schedulable and reliable for the implementation. Refinement helps in concise specification without overloading analysis.
The work presents the formal model, the analyses (both with and without refinement), and a compiler for HTL programs. The compiler checks composition and refinement constraints, performs schedulability and reliability analyses, and generates code for implementation of an HTL program on a virtual machine. Three real-time controllers, one each from automatic control, automotive control and avionic control, are used to illustrate the steps in modeling and analyzing HTL programs.
acknowledgement: 978-0-549-83679-7
author:
- first_name: Arkadeb
full_name: Ghosal, Arkadeb
last_name: Ghosal
citation:
ama: Ghosal A. *A Hierarchical Coordination Language for Reliable Real-Time Tasks*.
University of California, Berkeley; 2008:1-210.
apa: Ghosal, A. (2008). *A hierarchical coordination language for reliable real-time
tasks* (pp. 1–210). University of California, Berkeley.
chicago: Ghosal, Arkadeb. *A Hierarchical Coordination Language for Reliable Real-Time
Tasks*. University of California, Berkeley, 2008.
ieee: A. Ghosal, *A hierarchical coordination language for reliable real-time
tasks*. University of California, Berkeley, 2008, pp. 1–210.
ista: Ghosal A. 2008. A hierarchical coordination language for reliable real-time
tasks, University of California, Berkeley,p.
mla: Ghosal, Arkadeb. *A Hierarchical Coordination Language for Reliable Real-Time
Tasks*. University of California, Berkeley, 2008, pp. 1–210.
short: A. Ghosal, A Hierarchical Coordination Language for Reliable Real-Time Tasks,
University of California, Berkeley, 2008.
date_created: 2018-12-11T12:09:18Z
date_published: 2008-01-31T00:00:00Z
date_updated: 2019-01-24T13:20:30Z
day: '31'
extern: 1
month: '01'
page: 1 - 210
publication_status: published
publisher: University of California, Berkeley
publist_id: '199'
quality_controlled: 0
status: public
title: A hierarchical coordination language for reliable real-time tasks
type: dissertation
year: '2008'
...
---
_id: '4559'
abstract:
- lang: eng
text: |-
We study games played on graphs with omega-regular conditions specified as parity, Rabin, Streett or Muller conditions. These games have applications in the verification, synthesis, modeling, testing, and compatibility checking of reactive systems. Important distinctions between graph games are as follows: (a) turn-based vs. concurrent games, depending on whether at a state of the game only a single player makes a move, or players make moves simultaneously; (b) deterministic vs. stochastic, depending on whether the transition function is a deterministic or a probabilistic function over successor states; and (c) zero-sum vs. non-zero-sum, depending on whether the objectives of the players are strictly conflicting or not.
We establish that the decision problem for turn-based stochastic zero-sum games with Rabin, Streett, and Muller objectives are NP-complete, coNP-complete, and PSPACE-complete, respectively, substantially improving the previously known 3EXPTIME bound. We also present strategy improvement style algorithms for turn-based stochastic Rabin and Streett games. In the case of concurrent stochastic zero-sum games with parity objectives we obtain a PSPACE bound, again improving the previously known 3EXPTIME bound. As a consequence, concurrent stochastic zero-sum games with Rabin, Streett, and Muller objectives can be solved in EXPSPACE, improving the previously known 4EXPTIME bound. We also present an elementary and combinatorial proof of the existence of memoryless \epsilon-optimal strategies in concurrent stochastic games with reachability objectives, for all real \epsilon>0, where an \epsilon-optimal strategy achieves the value of the game with in \epsilon against all strategies of the opponent. We also use the proof techniques to present a strategy improvement style algorithm for concurrent stochastic reachability games.
We then go beyond \omega-regular objectives and study the complexity of an important class of quantitative objectives, namely, limit-average objectives. In the case of limit-average games, the states of the graph is labeled with rewards and the goal is to maximize the long-run average of the rewards. We show that concurrent stochastic zero-sum games with limit-average objectives can be solved in EXPTIME.
Finally, we introduce a new notion of equilibrium, called secure equilibrium, in non-zero-sum games which captures the notion of conditional competitiveness. We prove the existence of unique maximal secure equilibrium payoff profiles in turn-based deterministic games, and present algorithms to compute such payoff profiles. We also show how the notion of secure equilibrium extends the assume-guarantee style of reasoning in the game theoretic framework.
acknowledgement: Technical Report No. UCB/EECS-2007-122
author:
- first_name: Krishnendu
full_name: Krishnendu Chatterjee
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
citation:
ama: Chatterjee K. *Stochastic ω-Regular Games*. University of California,
Berkeley; 2007:1-247.
apa: Chatterjee, K. (2007). *Stochastic ω-Regular Games* (pp. 1–247). University
of California, Berkeley.
chicago: Chatterjee, Krishnendu. *Stochastic ω-Regular Games*. University of
California, Berkeley, 2007.
ieee: K. Chatterjee, *Stochastic ω-Regular Games*. University of California,
Berkeley, 2007, pp. 1–247.
ista: Chatterjee K. 2007. Stochastic ω-Regular Games, University of California,
Berkeley,p.
mla: Chatterjee, Krishnendu. *Stochastic ω-Regular Games*. University of California,
Berkeley, 2007, pp. 1–247.
short: K. Chatterjee, Stochastic ω-Regular Games, University of California, Berkeley,
2007.
date_created: 2018-12-11T12:09:29Z
date_published: 2007-10-08T00:00:00Z
date_updated: 2019-08-02T12:38:33Z
day: '08'
extern: 1
main_file_link:
- open_access: '0'
url: http://chess.eecs.berkeley.edu/pubs/462.html
month: '10'
page: 1 - 247
publication_status: published
publisher: University of California, Berkeley
publist_id: '150'
quality_controlled: 0
status: public
title: Stochastic ω-Regular Games
type: dissertation
year: '2007'
...
---
_id: '4566'
abstract:
- lang: eng
text: |-
Complex system design today calls for compositional design and implementation. However each component is designed with certain assumptions about the environment it is meant to operate in, and delivering certain guarantees if those assumptions are satisfied; numerous inter-component interaction errors are introduced in the manual and error-prone integration process as there is little support in design environments for machine-readably representing these assumptions and guarantees and automatically checking consistency during integration.
Based on Interface Automata we propose a framework for compositional design and analysis of systems: a set of domain-specific automata-theoretic type systems for compositional system specification and analysis by behavioral specification of open systems. We focus on three different domains: component-based hardware systems communicating on bidirectional wires. concurrent distributed recursive message-passing software systems, and embedded software system components operating in resource-constrained environments. For these domains we present approaches to formally represent the assumptions and conditional guarantees between interacting open system components. Composition of such components produces new components with the appropriate assumptions and guarantees. We check satisfaction of temporal logic specifications by such components, and the substitutability of one component with another in an arbitrary context. Using this framework one can analyze large systems incrementally without needing extensive summary information to close the system at each stage. Furthermore, we focus only on the inter-component interaction behavior without dealing with the full implementation details of each component. Many of the merits of automata-theoretic model-checking are combined with the compositionality afforded by type-system based techniques. We also present an integer-based extension of the conventional boolean verification framework motivated by our interface formalism for embedded software components.
Our algorithms for checking the behavioral compatibility of component interfaces are available in our tool Chic, which can be used as a plug-in for the Java IDE JBuilder and the heterogenous modeling and design environment Ptolemy II.
Finally, we address the complementary problem of partitioning a large system into meaningful coherent components by analyzing the interaction patterns between its basic elements. We demonstrate the usefulness of our partitioning approach by evaluating its efficacy in improving unit-test branch coverage for a large software system implemented in C.
author:
- first_name: Arindam
full_name: Chakrabarti, Arindam
last_name: Chakrabarti
citation:
ama: Chakrabarti A. *A Framework for Compositional Design and Analysis of Systems*.
University of California, Berkeley; 2007:1-244.
apa: Chakrabarti, A. (2007). *A framework for compositional design and analysis
of systems* (pp. 1–244). University of California, Berkeley.
chicago: Chakrabarti, Arindam. *A Framework for Compositional Design and Analysis
of Systems*. University of California, Berkeley, 2007.
ieee: A. Chakrabarti, *A framework for compositional design and analysis of systems*.
University of California, Berkeley, 2007, pp. 1–244.
ista: Chakrabarti A. 2007. A framework for compositional design and analysis of
systems, University of California, Berkeley,p.
mla: Chakrabarti, Arindam. *A Framework for Compositional Design and Analysis
of Systems*. University of California, Berkeley, 2007, pp. 1–244.
short: A. Chakrabarti, A Framework for Compositional Design and Analysis of Systems,
University of California, Berkeley, 2007.
date_created: 2018-12-11T12:09:31Z
date_published: 2007-12-20T00:00:00Z
date_updated: 2019-01-24T13:20:45Z
day: '20'
extern: 1
month: '12'
page: 1 - 244
publication_status: published
publisher: University of California, Berkeley
publist_id: '145'
quality_controlled: 0
status: public
title: A framework for compositional design and analysis of systems
type: dissertation
year: '2007'
...
---
_id: '4236'
author:
- first_name: Harold
full_name: de Vladar,Harold Paul
last_name: De Vladar
citation:
ama: De Vladar H. *Métodos No Lineales y Sus Aplicaciones En Dinámicas Aleatorias
de Poblaciones Celulares*. Centro de estudios avazados, IVIC; 2004. doi:3810
apa: De Vladar, H. (2004). *Métodos no lineales y sus aplicaciones en dinámicas
aleatorias de poblaciones celulares*. Centro de estudios avazados, IVIC. https://doi.org/3810
chicago: De Vladar, Harold. *Métodos No Lineales y Sus Aplicaciones En Dinámicas
Aleatorias de Poblaciones Celulares*. Centro de estudios avazados, IVIC, 2004.
https://doi.org/3810.
ieee: H. De Vladar, *Métodos no lineales y sus aplicaciones en dinámicas aleatorias
de poblaciones celulares*. Centro de estudios avazados, IVIC, 2004.
ista: De Vladar H. 2004. Métodos no lineales y sus aplicaciones en dinámicas aleatorias
de poblaciones celulares, Centro de estudios avazados, IVIC,p.
mla: De Vladar, Harold. *Métodos No Lineales y Sus Aplicaciones En Dinámicas Aleatorias
de Poblaciones Celulares*. Centro de estudios avazados, IVIC, 2004, doi:3810.
short: H. De Vladar, Métodos No Lineales y Sus Aplicaciones En Dinámicas Aleatorias
de Poblaciones Celulares, Centro de estudios avazados, IVIC, 2004.
date_created: 2018-12-11T12:07:46Z
date_published: 2004-01-01T00:00:00Z
date_updated: 2019-01-24T13:18:53Z
day: '01'
doi: '3810'
extern: 1
month: '01'
publication_status: published
publisher: Centro de estudios avazados, IVIC
publist_id: '1877'
quality_controlled: 0
status: public
title: Métodos no lineales y sus aplicaciones en dinámicas aleatorias de poblaciones
celulares
type: dissertation
year: '2004'
...
---
_id: '4424'
abstract:
- lang: eng
text: |-
The enormous cost and ubiquity of software errors necessitates the need for techniques and tools that can precisely analyze large systems and prove that they meet given specifications, or if they don't, return counterexample behaviors showing how the system fails. Recent advances in model checking, decision procedures, program analysis and type systems, and a shift of focus to partial specifications common to several systems (e.g., memory safety and race freedom) have resulted in several practical verification methods. However, these methods are either precise or they are scalable, depending on whether they track the values of variables or only a fixed small set of dataflow facts (e.g., types), and are usually insufficient for precisely verifying large programs.
We describe a new technique called Lazy Abstraction (LA) which achieves both precision and scalability by localizing the use of precise information. LA automatically builds, explores and refines a single abstract model of the program in a way that different parts of the model exhibit different degrees of precision, namely just enough to verify the desired property. The algorithm automatically mines the information required by partitioning mechanical proofs of unsatisfiability of spurious counterexamples into Craig Interpolants. For multithreaded systems, we give a new technique based on analyzing the behavior of a single thread executing in a context which is an abstraction of the other (arbitrarily many) threads. We define novel context models and show how to automatically infer them and analyze the full system (thread + context) using LA.
LA is implemented in BLAST. We have run BLAST on Windows and Linux Device Drivers to verify API conformance properties, and have used it to find (or guarantee the absence of) data races in multithreaded Networked Embedded Systems (NESC) applications. BLAST is able to prove the absence of races in several cases where earlier methods, which depend on lock-based synchronization, fail.
author:
- first_name: Ranjit
full_name: Jhala, Ranjit
last_name: Jhala
citation:
ama: Jhala R. *Program Verification by Lazy Abstraction*. University of California,
Berkeley; 2004:1-165.
apa: Jhala, R. (2004). *Program verification by lazy abstraction* (pp. 1–165).
University of California, Berkeley.
chicago: Jhala, Ranjit. *Program Verification by Lazy Abstraction*. University
of California, Berkeley, 2004.
ieee: R. Jhala, *Program verification by lazy abstraction*. University of California,
Berkeley, 2004, pp. 1–165.
ista: Jhala R. 2004. Program verification by lazy abstraction, University of California,
Berkeley,p.
mla: Jhala, Ranjit. *Program Verification by Lazy Abstraction*. University
of California, Berkeley, 2004, pp. 1–165.
short: R. Jhala, Program Verification by Lazy Abstraction, University of California,
Berkeley, 2004.
date_created: 2018-12-11T12:08:47Z
date_published: 2004-12-01T00:00:00Z
date_updated: 2019-01-24T13:19:57Z
day: '01'
extern: 1
month: '12'
page: 1 - 165
publication_status: published
publisher: University of California, Berkeley
publist_id: '307'
quality_controlled: 0
status: public
title: Program verification by lazy abstraction
type: dissertation
year: '2004'
...
---
_id: '4425'
abstract:
- lang: eng
text: |-
Giotto provides a time-triggered programmer’s model for the implementation of embedded control systems with hard real-time constraints. Giotto’s precise semantics and predictabil- ity make it suitable for safety-critical applications.
Giotto is based around the idea that time-triggered task invocation together with time-triggered mode switching can form a useful programming model for real-time systems. To substantiate this claim, we describe the use of Giotto to refactor the software of a small, autonomous helicopter. The ease with which Giotto expresses the existing software provides evidence that Giotto is an appropriate programming language for control systems.
Since Giotto is a real-time programming language, ensuring that Giotto programs meet their deadlines is crucial. To study precedence-constrained Giotto scheduling, we first examine single-mode, single-processor scheduling. We extend to an infinite, periodic setting the classical problem of meeting deadlines for a set of tasks with release times, deadlines, precedence constraints, and preemption. We then develop an algorithm for scheduling Giotto programs on a single processor by representing Giotto programs as instances of the extended scheduling problem.
Next, we study multi-mode, single-processor Giotto scheduling. This problem is different from classical scheduling problems, since in our precedence-constrained approach, the deadlines of tasks may vary depending on the mode switching behavior of the program. We present conditional scheduling models which capture this varying-deadline behavior. We develop polynomial-time algorithms for some conditional scheduling models, and prove oth- ers to be computationally hard. We show how to represent multi-mode Giotto programs as instances of the model, resulting in an algorithm for scheduling multi-mode Giotto programs on a single processor.
Finally, we show that the problem of scheduling Giotto programs for multiple net- worked processors is strongly NP-hard.
author:
- first_name: Benjamin
full_name: Horowitz, Benjamin
last_name: Horowitz
citation:
ama: 'Horowitz B. *Giotto: A Time-Triggered Language for Embedded Programming*.
University of California, Berkeley; 2003:1-237.'
apa: 'Horowitz, B. (2003). *Giotto: A time-triggered language for embedded programming*
(pp. 1–237). University of California, Berkeley.'
chicago: 'Horowitz, Benjamin. *Giotto: A Time-Triggered Language for Embedded
Programming*. University of California, Berkeley, 2003.'
ieee: 'B. Horowitz, *Giotto: A time-triggered language for embedded programming*.
University of California, Berkeley, 2003, pp. 1–237.'
ista: 'Horowitz B. 2003. Giotto: A time-triggered language for embedded programming,
University of California, Berkeley,p.'
mla: 'Horowitz, Benjamin. *Giotto: A Time-Triggered Language for Embedded Programming*.
University of California, Berkeley, 2003, pp. 1–237.'
short: 'B. Horowitz, Giotto: A Time-Triggered Language for Embedded Programming,
University of California, Berkeley, 2003.'
date_created: 2018-12-11T12:08:47Z
date_published: 2003-10-01T00:00:00Z
date_updated: 2019-01-24T13:19:57Z
day: '01'
extern: 1
month: '10'
page: 1 - 237
publication_status: published
publisher: University of California, Berkeley
publist_id: '305'
quality_controlled: 0
status: public
title: 'Giotto: A time-triggered language for embedded programming'
type: dissertation
year: '2003'
...
---
_id: '2414'
author:
- first_name: Uli
full_name: Uli Wagner
id: 36690CA2-F248-11E8-B48F-1D18A9856A87
last_name: Wagner
orcid: 0000-0002-1494-0568
citation:
ama: Wagner U. *On K-Sets and Their Applications*. ETH Zurich; 2003. doi:10.3929/ethz-a-004708408
apa: Wagner, U. (2003). *On k-Sets and Their Applications*. ETH Zurich. https://doi.org/10.3929/ethz-a-004708408
chicago: Wagner, Uli. *On K-Sets and Their Applications*. ETH Zurich, 2003.
https://doi.org/10.3929/ethz-a-004708408.
ieee: U. Wagner, *On k-Sets and Their Applications*. ETH Zurich, 2003.
ista: Wagner U. 2003. On k-Sets and Their Applications, ETH Zurich,p.
mla: Wagner, Uli. *On K-Sets and Their Applications*. ETH Zurich, 2003, doi:10.3929/ethz-a-004708408.
short: U. Wagner, On K-Sets and Their Applications, ETH Zurich, 2003.
date_created: 2018-12-11T11:57:31Z
date_published: 2003-01-01T00:00:00Z
date_updated: 2019-04-26T07:22:12Z
day: '01'
doi: 10.3929/ethz-a-004708408
extern: 1
month: '01'
publication_status: published
publisher: ETH Zurich
publist_id: '4511'
quality_controlled: 0
status: public
title: On k-Sets and Their Applications
type: dissertation
year: '2003'
...
---
_id: '4416'
abstract:
- lang: eng
text: |-
Methods for the formal specification and verification of systems are indispensible for the development of complex yet correct systems. In formal verification, the designer describes the system in a modeling language with a well-defined semantics, and this system description is analyzed against a set of correctness requirements. Model checking is an algorithmic technique to check that a system description indeed satisfies correctness requirements given as logical specifications. While successful in hardware verification, the potential for model checking for software and embedded systems has not yet been realized. This is because traditional model checking focuses on systems modeled as finite state-transition graphs. While a natural model for hardware (especially synchronous hardware), state-transition graphs often do not capture software and embedded systems at an appropriate level of granularity. This dissertation considers two orthogonal extensions to finite state-transition graphs making model checking techniques applicable to both a wider class of systems and a wider class of properties.
The first direction is an extension to infinite-state structures finitely represented using constraints and operations on constraints. Infinite state arises when we wish to model variables with unbounded range (e.g., integers), or data structures, or real time. We provide a uniform framework of symbolic region algebras to study model checking of infinite-state systems. We also provide sufficient language-independent termination conditions for symbolic model checking algorithms on infinite state systems.
The second direction supplements verification with game theoretic reasoning. Games are natural models for interactions between components. We study game theoretic behavior with winning conditions given by temporal logic objectives both in the deterministic and in the probabilistic context. For deterministic games, we provide an extremal model characterization of fixpoint algorithms that link solutions of verification problems to solutions for games. For probabilistic games we study fixpoint characterization of winning probabilities for games with omega-regular winning objectives, and construct (epsilon-)optimal winning strategies.
author:
- first_name: Ritankar
full_name: Majumdar, Ritankar S
last_name: Majumdar
citation:
ama: Majumdar R. *Symbolic Algorithms for Verification and Control*. University
of California, Berkeley; 2003:1-201.
apa: Majumdar, R. (2003). *Symbolic algorithms for verification and control*
(pp. 1–201). University of California, Berkeley.
chicago: Majumdar, Ritankar. *Symbolic Algorithms for Verification and Control*.
University of California, Berkeley, 2003.
ieee: R. Majumdar, *Symbolic algorithms for verification and control*. University
of California, Berkeley, 2003, pp. 1–201.
ista: Majumdar R. 2003. Symbolic algorithms for verification and control, University
of California, Berkeley,p.
mla: Majumdar, Ritankar. *Symbolic Algorithms for Verification and Control*.
University of California, Berkeley, 2003, pp. 1–201.
short: R. Majumdar, Symbolic Algorithms for Verification and Control, University
of California, Berkeley, 2003.
date_created: 2018-12-11T12:08:44Z
date_published: 2003-12-01T00:00:00Z
date_updated: 2019-01-24T13:19:54Z
day: '01'
extern: 1
month: '12'
page: 1 - 201
publication_status: published
publisher: University of California, Berkeley
publist_id: '313'
quality_controlled: 0
status: public
title: Symbolic algorithms for verification and control
type: dissertation
year: '2003'
...
---
_id: '3678'
author:
- first_name: Christoph
full_name: Christoph Lampert
id: 40C20FD2-F248-11E8-B48F-1D18A9856A87
last_name: Lampert
orcid: 0000-0001-8622-7887
citation:
ama: Lampert C. *The Neumann Operator in Strictly Pseudoconvex Domains with Weighted
Bergman Metric *. Vol 356. Universität Bonn, Fachbibliothek Mathematik; 2003:1-165.
apa: Lampert, C. (2003). *The Neumann operator in strictly pseudoconvex domains
with weighted Bergman metric *. *Bonner Mathematische Schriften* (Vol.
356, pp. 1–165). Universität Bonn, Fachbibliothek Mathematik.
chicago: Lampert, Christoph. *The Neumann Operator in Strictly Pseudoconvex Domains
with Weighted Bergman Metric *. *Bonner Mathematische Schriften*. Vol.
356. Universität Bonn, Fachbibliothek Mathematik, 2003.
ieee: C. Lampert, *The Neumann operator in strictly pseudoconvex domains with
weighted Bergman metric *, vol. 356. Universität Bonn, Fachbibliothek Mathematik,
2003, pp. 1–165.
ista: Lampert C. 2003. The Neumann operator in strictly pseudoconvex domains with
weighted Bergman metric , Universität Bonn, Fachbibliothek Mathematik,p.
mla: Lampert, Christoph. “The Neumann Operator in Strictly Pseudoconvex Domains
with Weighted Bergman Metric .” *Bonner Mathematische Schriften*, vol. 356,
Universität Bonn, Fachbibliothek Mathematik, 2003, pp. 1–165.
short: C. Lampert, The Neumann Operator in Strictly Pseudoconvex Domains with Weighted
Bergman Metric , Universität Bonn, Fachbibliothek Mathematik, 2003.
date_created: 2018-12-11T12:04:34Z
date_published: 2003-03-31T00:00:00Z
date_updated: 2019-04-26T07:22:33Z
day: '31'
extern: 1
intvolume: ' 356'
main_file_link:
- open_access: '0'
url: http://pub.ist.ac.at/~chl/papers/lampert-phd2003.pdf
month: '03'
page: 1 - 165
publication: Bonner Mathematische Schriften
publication_status: published
publisher: Universität Bonn, Fachbibliothek Mathematik
publist_id: '2704'
quality_controlled: 0
status: public
title: 'The Neumann operator in strictly pseudoconvex domains with weighted Bergman
metric '
type: dissertation
volume: 356
year: '2003'
...
---
_id: '4414'
abstract:
- lang: eng
text: |-
This dissertation investigates game-theoretic approaches to the algorithmic analysis of concurrent, reactive systems. A concurrent system comprises a number of components working concurrently; a reactive system maintains an ongoing interaction with its environment. Traditional approaches to the formal analysis of concurrent reactive systems usually view the system as an unstructured state-transition graphs; instead, we view them as collections of interacting components, where each one is an open system which accepts inputs from the other components. The interactions among the components are naturally modeled as games.
Adopting this game-theoretic view, we study three related problems pertaining to the verification and synthesis of systems. Firstly, we propose two novel game-theoretic techniques for the model-checking of concurrent reactive systems, and improve the performance of model-checking. The first technique discovers an error as soon as it cannot be prevented, which can be long before it actually occurs. This technique is based on the key observation that "unpreventability" is a local property to a module: an error is unpreventable in a module state if no environment can prevent it. The second technique attempts to decompose a model-checking proof into smaller proof obligations by constructing abstract modules automatically, using reachability and "unpreventability" information about the concrete modules. Three increasingly powerful proof decomposition rules are proposed and we show that in practice, the resulting abstract modules are often significantly smaller than the concrete modules and can drastically reduce the space and time requirements for verification. Both techniques fall into the category of compositional reasoning.
Secondly, we investigate the composition and control of synchronous systems. An essential property of synchronous systems for compositional reasoning is non-blocking. In the composition of synchronous systems, however, due to circular causal dependency of input and output signals, non-blocking is not always guaranteed. Blocking compositions of systems can be ruled out semantically, by insisting on the existence of certain fixed points, or syntactically, by equipping systems with types, which make the dependencies between input and output signals transparent. We characterize various typing mechanisms in game-theoretic terms, and study their effects on the controller synthesis problem. We show that our typing systems are general enough to capture interesting real-life synchronous systems such as all delay-insensitive digital circuits. We then study their corresponding single-step control problems --a restricted form of controller synthesis problem whose solutions can be iterated in appropriate manners to solve all LTL controller synthesis problems. We also consider versions of the controller synthesis problem in which the type of the controller is given. We show that the solution of these fixed-type control problems requires the evaluation of partially ordered (Henkin) quantifiers on boolean formulas, and is therefore harder (nondeterministic exponential time) than more traditional control questions.
Thirdly, we study the synthesis of a class of open systems, namely, uninitialized state machines. The sequential synthesis problem, which is closely related to Church's solvability problem, asks, given a specification in the form of a binary relation between input and output streams, for the construction of a finite-state stream transducer that converts inputs to appropriate outputs. For efficiency reasons, practical sequential hardware is often designed to operate without prior initialization. Such hardware designs can be modeled by uninitialized state machines, which are required to satisfy their specification if started from any state. We solve the sequential synthesis problem for uninitialized systems, that is, we construct uninitialized finite-state stream transducers. We consider specifications given by LTL formulas, deterministic, nondeterministic, universal, and alternating Buechi automata. We solve this uninitialized synthesis problem by reducing it to the well-understood initialized synthesis problem. While our solution is straightforward, it leads, for some specification formalisms, to upper bounds that are exponentially worse than the complexity of the corresponding initialized problems. However, we prove lower bounds to show that our simple solutions are optimal for all considered specification formalisms. The lower bound proofs require nontrivial generic reductions.
author:
- first_name: Freddy
full_name: Mang, Freddy Y
last_name: Mang
citation:
ama: Mang F. *Games in Open Systems Verification and Synthesis*. University
of California, Berkeley; 2002:1-116.
apa: Mang, F. (2002). *Games in open systems verification and synthesis* (pp.
1–116). University of California, Berkeley.
chicago: Mang, Freddy. *Games in Open Systems Verification and Synthesis*.
University of California, Berkeley, 2002.
ieee: F. Mang, *Games in open systems verification and synthesis*. University
of California, Berkeley, 2002, pp. 1–116.
ista: Mang F. 2002. Games in open systems verification and synthesis, University
of California, Berkeley,p.
mla: Mang, Freddy. *Games in Open Systems Verification and Synthesis*. University
of California, Berkeley, 2002, pp. 1–116.
short: F. Mang, Games in Open Systems Verification and Synthesis, University of
California, Berkeley, 2002.
date_created: 2018-12-11T12:08:44Z
date_published: 2002-05-01T00:00:00Z
date_updated: 2019-01-24T13:19:54Z
day: '01'
extern: 1
month: '05'
page: 1 - 116
publication_status: published
publisher: University of California, Berkeley
publist_id: '315'
quality_controlled: 0
status: public
title: Games in open systems verification and synthesis
type: dissertation
year: '2002'
...
---
_id: '4411'
abstract:
- lang: eng
text: |-
Model checking algorithms for the verification of reactive systems proceed by a systematic and exhaustive exploration of the system state space. They do not scale to large designs because of the state explosion problem --the number of states grows exponentially with the number of components in the design. Consequently, the model checking problem is PSPACE-hard in the size of the design description. This dissertation proposes three novel techniques to combat the state explosion problem.
One of the most important advances in model checking in recent years has been the discovery of symbolic methods, which use a calculus of expressions, such as binary decision diagrams, to represent the state sets encountered during state space exploration. Symbolic model checking has proved to be effective for verifying hardware designs. Traditionally, symbolic checking of temporal logic specifications is performed by backward fixpoint reasoning with the operator Pre. Backward reasoning can be wasteful since unreachable states are explored. We suggest the use of forward fixpoint reasoning based on the operator Post. We show how all linear temporal logic specifications can be model checked symbolically by forward reasoning. In contrast to backward reasoning, forward reasoning performs computations only on the reachable states.
Heuristics that improve algorithms for application domains, such as symbolic methods for hardware designs, are useful but not enough to make model checking feasible on industrial designs. Currently, exhaustive state exploration is possible only on designs with about 50-100 boolean state variables. Assume-guarantee verification attempts to combat the state explosion problem by using the principle of "divide and conquer," where the components of the implementation are analyzed one at a time. Typically, an implementation component refines its specification only when its inputs are suitably constrained by other components in the implementation. The assume-guarantee principle states that instead of constraining the inputs by implementation components, it is sound to constrain them by the corresponding specification components, which can be significantly smaller. We extend the assume-guarantee proof rule to deal with the case where the specification operates at a coarser time scale than the implementation. Using our model checker Mocha, which implements this methodology, we verify VGI, a parallel DSP processor chip with 64 compute processors each containing approximately 800 state variables and 30K gates.
Our third contribution is a systematic model checking methodology for verifying the abstract shared-memory interface of sequential consistency on multiprocessor systems with three parameters --number of processors, number of memory locations, and number of data values. Sequential consistency requires that some interleaving of the local temporal orders of read/write events at different processors be a trace of serial memory. Therefore, it suffices to construct a non-interfering serializer that watches and reorders read/write events so that a trace of serial memory is obtained. While in general such a serializer must be unbounded even for fixed values of the parameters --checking sequential consistency is undecidable!-- we show that the paradigmatic class of snoopy cache coherence protocols has finite-state serializers. In order to reduce the arbitrary-parameter problem to the fixed-parameter problem, we develop a novel framework for induction over the number of processors and use the notion of a serializer to reduce the problem of verifying sequential consistency to that of checking language inclusion between finite state machines.
author:
- first_name: Shaz
full_name: Qadeer,Shaz
last_name: Qadeer
citation:
ama: Qadeer S. *Algorithms and Methodology for Scalable Model Checking*. University
of California, Berkeley; 1999:1-150.
apa: Qadeer, S. (1999). *Algorithms and Methodology for Scalable Model Checking*
(pp. 1–150). University of California, Berkeley.
chicago: Qadeer, Shaz. *Algorithms and Methodology for Scalable Model Checking*.
University of California, Berkeley, 1999.
ieee: S. Qadeer, *Algorithms and Methodology for Scalable Model Checking*.
University of California, Berkeley, 1999, pp. 1–150.
ista: Qadeer S. 1999. Algorithms and Methodology for Scalable Model Checking, University
of California, Berkeley,p.
mla: Qadeer, Shaz. *Algorithms and Methodology for Scalable Model Checking*.
University of California, Berkeley, 1999, pp. 1–150.
short: S. Qadeer, Algorithms and Methodology for Scalable Model Checking, University
of California, Berkeley, 1999.
date_created: 2018-12-11T12:08:43Z
date_published: 1999-10-01T00:00:00Z
date_updated: 2019-01-24T13:19:53Z
day: '01'
extern: 1
main_file_link:
- open_access: '0'
url: http://mtc.epfl.ch/~tah/Students/qadeer.pdf
month: '10'
page: 1 - 150
publication_status: published
publisher: University of California, Berkeley
publist_id: '321'
quality_controlled: 0
status: public
supervisor:
- first_name: Robert
full_name: Bryton, Robert K.
last_name: Bryton
- first_name: John
full_name: Steel, John
last_name: Steel
title: Algorithms and Methodology for Scalable Model Checking
type: dissertation
year: '1999'
...
---
_id: '4419'
author:
- first_name: Peter
full_name: Kopke, Peter W
last_name: Kopke
citation:
ama: Kopke P. *The Theory of Rectangular Hybrid Automata*. Cornell University;
1996.
apa: Kopke, P. (1996). *The Theory of Rectangular Hybrid Automata*. Cornell
University.
chicago: Kopke, Peter. *The Theory of Rectangular Hybrid Automata*. Cornell
University, 1996.
ieee: P. Kopke, *The Theory of Rectangular Hybrid Automata*. Cornell University,
1996.
ista: Kopke P. 1996. The Theory of Rectangular Hybrid Automata, Cornell University,p.
mla: Kopke, Peter. *The Theory of Rectangular Hybrid Automata*. Cornell University,
1996.
short: P. Kopke, The Theory of Rectangular Hybrid Automata, Cornell University,
1996.
date_created: 2018-12-11T12:08:45Z
date_published: 1996-01-01T00:00:00Z
date_updated: 2019-01-24T13:19:55Z
day: '01'
extern: 1
month: '01'
publication_status: published
publisher: Cornell University
publist_id: '312'
quality_controlled: 0
status: public
title: The Theory of Rectangular Hybrid Automata
type: dissertation
year: '1996'
...
---
_id: '4428'
abstract:
- lang: eng
text: |-
Hybrid systems are real-time systems that react to both discrete and continuous activities (such as analog signals, time, temperature, and speed). Typical examples of hybrid systems are embedded systems, timing-based communication protocols, and digital circuits at the transistor level. Due to the rapid development of microprocessor technology, hybrid systems directly control much of what we depend on in our daily lives. Consequently, the formal specification and verification of hybrid systems has become an active area of research. This dissertation presents the first general framework for the formal specification and verification of hybrid systems, as well as the first hybrid-system analysis tool--HyTech. The framework consists of a graphical finite-state-machine-like language for modeling hybrid systems, a temporal logic for modeling the requirements of hybrid systems, and a computer procedure that verifies modeled hybrid systems against modeled requirements. The tool HyTech is the implementation of the framework using C++ and Mathematica.
More specifically, our hybrid-system modeling language, Hybrid Automata, is an extension of timed automata with discrete and continuous variables whose dynamics are governed by differential equations. Our requirement modeling language, ICTL, is a branching-time temporal logic, and is an extension of TCTL with stop-watch variables. Our verification procedure is a symbolic model-checking procedure that verifies linear hybrid automata against ICTL formulas. To make HyTech more efficient and effective, we use model-checking strategies and abstract operators that can expedite the verification process. To enable HyTech to verify nonlinear hybrid automata, we introduce two translations from nonlinear hybrid automata to linear hybrid automata. We have applied HyTech to analyze more than 30 hybrid-system benchmarks. In this dissertation, we present the application of HyTech to three nontrivial hybrid systems taken from the literature.
author:
- first_name: Pei
full_name: Ho, Pei-Hsin
last_name: Ho
citation:
ama: Ho P. *Automatic Analysis of Hybrid Systems*. Cornell University; 1995:1-188.
doi:CSD-TR95-1536
apa: Ho, P. (1995). *Automatic Analysis of Hybrid Systems* (pp. 1–188). Cornell
University. https://doi.org/CSD-TR95-1536
chicago: Ho, Pei. *Automatic Analysis of Hybrid Systems*. Cornell University,
1995. https://doi.org/CSD-TR95-1536.
ieee: P. Ho, *Automatic Analysis of Hybrid Systems*. Cornell University, 1995,
pp. 1–188.
ista: Ho P. 1995. Automatic Analysis of Hybrid Systems, Cornell University,p.
mla: Ho, Pei. *Automatic Analysis of Hybrid Systems*. Cornell University, 1995,
pp. 1–188, doi:CSD-TR95-1536.
short: P. Ho, Automatic Analysis of Hybrid Systems, Cornell University, 1995.
date_created: 2018-12-11T12:08:48Z
date_published: 1995-01-01T00:00:00Z
date_updated: 2019-01-24T13:19:58Z
day: '01'
doi: CSD-TR95-1536
extern: 1
month: '01'
page: 1 - 188
publication_status: published
publisher: Cornell University
publist_id: '304'
quality_controlled: 0
status: public
title: Automatic Analysis of Hybrid Systems
type: dissertation
year: '1995'
...
---
_id: '4516'
author:
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: Henzinger TA. *The Temporal Specification and Verification of Real-Time Systems
*. Stanford University; 1991.
apa: Henzinger, T. A. (1991). *The Temporal Specification and Verification of
Real-time Systems *. Stanford University.
chicago: Henzinger, Thomas A. *The Temporal Specification and Verification of
Real-Time Systems *. Stanford University, 1991.
ieee: T. A. Henzinger, *The Temporal Specification and Verification of Real-time
Systems *. Stanford University, 1991.
ista: Henzinger TA. 1991. The Temporal Specification and Verification of Real-time
Systems , Stanford University,p.
mla: Henzinger, Thomas A. *The Temporal Specification and Verification of Real-Time
Systems *. Stanford University, 1991.
short: T.A. Henzinger, The Temporal Specification and Verification of Real-Time
Systems , Stanford University, 1991.
date_created: 2018-12-11T12:09:15Z
date_published: 1991-08-01T00:00:00Z
date_updated: 2019-08-02T12:38:32Z
day: '01'
extern: 1
main_file_link:
- open_access: '0'
url: http://mtc.epfl.ch/~tah/Publications/the_temporal_specification_and_verification_of_real-time_systems.pdf
month: '08'
publication_status: published
publisher: Stanford University
publist_id: '210'
quality_controlled: 0
status: public
title: 'The Temporal Specification and Verification of Real-time Systems '
type: dissertation
year: '1991'
...
---
_id: '4337'
author:
- first_name: Nicholas H
full_name: Nicholas Barton
id: 4880FE40-F248-11E8-B48F-1D18A9856A87
last_name: Barton
orcid: 0000-0002-8548-5240
citation:
ama: Barton NH. *A Hybrid Zone in the Alpine Grasshopper Podisma Pedestris*.
University of East Anglia; 1979.
apa: Barton, N. H. (1979). *A hybrid zone in the alpine grasshopper Podisma pedestris*.
University of East Anglia.
chicago: Barton, Nicholas H. *A Hybrid Zone in the Alpine Grasshopper Podisma
Pedestris*. University of East Anglia, 1979.
ieee: N. H. Barton, *A hybrid zone in the alpine grasshopper Podisma pedestris*.
University of East Anglia, 1979.
ista: Barton NH. 1979. A hybrid zone in the alpine grasshopper Podisma pedestris,
University of East Anglia,p.
mla: Barton, Nicholas H. *A Hybrid Zone in the Alpine Grasshopper Podisma Pedestris*.
University of East Anglia, 1979.
short: N.H. Barton, A Hybrid Zone in the Alpine Grasshopper Podisma Pedestris, University
of East Anglia, 1979.
date_created: 2018-12-11T12:08:20Z
date_published: 1979-01-01T00:00:00Z
date_updated: 2019-04-26T07:22:43Z
day: '01'
extern: 1
month: '01'
publication_status: published
publisher: University of East Anglia
publist_id: '1694'
quality_controlled: 0
status: public
title: A hybrid zone in the alpine grasshopper Podisma pedestris
type: dissertation
year: '1979'
...