SDRL
Systems Design Research Lab
 
 

Question or Comment
Contact: Valentina Sokolskaya
Last updated: January 31, 07

Winter - Spring 2000 Seminars

 

We have seminars together with Logic and Computation Group
each Monday at 4:30PM
University of Pennsylvania, Moore 554

 

Deriving operational congruences for reactive systems

James Leifer
Cambridge University

Monday, August 28, 2000, 4:30 PM
Moore 556

 Assigning mathematical interpretations (semantics) to computer programs allows us to prove that code is correct with respect to a specification, to make precise how a compiler works and what optimisations are valid, to compare language features, etc. Many interpretations exist for sequential computation and typically model a (deterministic) program as a function from memories to memories that  maps each state to the one that holds after the program executes.

The situation is more complex when considering parallel computation, and, in particular, languages presented in terms of reaction rules (characterising the primitive interactions) that cater for communication, distribution, mobility, and security. It is a major challenge to find a compositional semantic interpretation (one that respects the constructions of the language) and, in practice, is either impossible or accomplished in an ad hoc manner with a difficult hand-crafted proof of compositionality bolted on.

I describe new work that begins to address this challenge. I first show how to derive uniformly a labelled transition system (LTS) from a set of reaction rules, taking the labels, or  "observations'', to be those contexts which are just large enough to enable a reaction: a program undergoes a labelled transition exactly when it requires the entire label to react. The key contribution is the precise definition of  "just large enough'' in terms of the categorical notion of relative pushout. I prove using some lightweight reasoning that operational equivalences built from the LTS such as strong and weak bisimilarity and trace equivalence are congruences. Thus the semantic interpretation of programs in terms of these equivalences is guaranteed to be compositional. I conclude by touching on some future work.

Joint work with Robin Milner.

Back to seminars list

 

Logic-based design and synthesis of controllers for hybrid systems

Jen Davoren
Australian National University, Canberra

Monday, August 14, 2000    4:30 PM
Moore 556

 Hybrid systems are heterogeneous dynamical systems characterized by a non-trivial interaction of continuous and discrete dynamics, and typically arise in the embedded software control of physical processes. The widely accepted hybrid automaton model consists of a finite collection of continuous systems defined by differential equations, over a common state space, together with a mechanism which decides when and how the system can switch between these continuous sub-systems. We consider the following type of control problem. Given a finite collection of continuous systems, design and build a hybrid automaton model for that collection so that every hybrid trajectory of the resulting system is guaranteed to satisfy a given list of performance specifications. One novelty of our work is that in addition to the well-studied classes of safety and liveness properties of hybrid trajectories, we also address a quite general class of event sequence properties, by which one can enforce positive behavioural requirements on hybrid trajectories. We develop an abstract algorithm to solve this control problem for which we can guarantee finite termination. A central idea is that in tackling the problem, one needs to reason about sets of continuous states, and to build up complex sets of states using operators on sets induced by the given continuous flows and data from the specifications. We demonstrate how such reasoning and construction of sets can be cleanly and naturally formalized in the language of modal logic. The benefits of using the technical tool of modal logic are two-fold. First, it gives us a formal language in which to formulate our solution algorithm. Second, a proof of correctness can transparently be derived from a theory of modal formulas that are true of any hybrid automaton solution purely in virtue of the statement of the algorithm. The abstract algorithm will be illustrated via a simple example, with output generated by our prototype software implementation.

(Joint work with Dr. Thomas Moor, RSISE, ANU)

Short bio: Jen Davoren is a research fellow in the Computer Sciences Laboratory at the Research School of Information Sciences and Engineering at the Australian National University. She has a PhD in mathematics and an MSc in computer science from Cornell University, after undergraduate studies in mathematics and philosophy at the University of Melbourne, Australia. Prior to starting at the ANU last September, she had a postdoc position at Cornell with extended visits to the Dept. EECS at U.C. Berkeley.

Back to seminars list

Dependently Types Records for Representing Mathematical Structure

Randy Pollack
University of Durham

Thursday, Aug 10, at 3:00 PM
Moore 556

Randy will be visiting the CIS department on Thursday and Friday. Please contact bcpierce@cis.upenn.edu if you'd like to meet with him. His LCS seminar will continue informally during the PL Club lunch on Friday (12:30-2, in the Theory Lab). 

It is folklore that dependently typed tuples suffice to formalize abstract mathematical structures such as semi-group, monoid, group, ring, field, ... We want natural properties of informal mathematical language to be preserved; e.g. inheritance of properties and sharing of substructures. There is a big literature on the related topic of programming language modules.

This talk develops a notion of dependently typed records by adding field labels to Sigma types. Some obscure features from the literature are simplified and explained. E.g. field variables (local) vs field labels (global) are explained by ordinary lambda-binding. Subtyping is orthogonal to records, and is introduced using Luo's coercive subtyping. (Hence I do not explain the subtyping system in detail, but only show some examples.) 

I discuss the two standard approaches to sharing substructures: "Pebble style" and "manifest types" (ML style). By example, I argue that we really do need manifest types to formalize mathematics. I extend dependently typed records to include manifest types and the "with" notation for adding manifest information to an existing signature.

Most recently, I have been able to directly program records with first-class labels, dependent, manifest signatures and "with" in type theory, using Dybjer's "inductive-recursive" definition. All of the rules (projection, subtyping, "value rules", definition of "with") are derivable from the inductive-recursive definition, which has only three constructors and three corresponding computation rules. 

A preliminary paper is available 

Back to seminars list

 

Automatic Verification of Parameterized Cache Coherence Protocols

Giorgio Delzanno
DISI - University of Genova

Thursday, July 24, 2000, 3:00 PM
Moore 554

 We propose a new method for the verification of parameterized cache coherence protocols.
Cache coherence protocols are used to maintain data consistency in multiprocessor systems equipped with local fast caches. 
In our approach we use arithmetic constraints to model possibly infinite sets of global states of a multiprocessor system with many identical caches.
In preliminary experiments using symbolic model checkers for infinite-state systems based on real arithmetics (HyTech and DMC we have automatically verified safety properties for parameterized versions of widely implemented write-invalidate and write-update cache coherence policies like the Mesi, Berkeley, Illinois, Firefly and Dragon protocols.
With this application, we show that symbolic model checking tools originally designed for hybrid and concurrent systems can be applied successfully to a new class of infinite-state systems of practical interest.

Back to seminars list

 

What logic is good for CS ?

or
"The Drinking Philosophers"
in the mirror of Horn linear logic

Max Kanovitch
University of Pennsylvania

Monday, May 1, 2000, 4:30 PM
Moore 554

 The aim of this research is to develop adequate and comprehensive logical systems capable of handling important properties of real-time systems.

The basic step in understanding a given timed system S is to show that its `reachability' predicate: 
        "There exists a trajectory that leads to a given state s'',
is partial recursive.

After that, for any reasonably expressive logical system L, one can immediately conclude that the above 'reachability problem' is equivalent to the problem whether the corresponding sequent is provable in L or not.

The real challenge is to establish that a proposed logical system L is 'fully adequate': that there is a direct correspondence between trajectories in S and proofs in L.

We will consider real-time systems with quantitative time constraints, within which all things may be changed during the course of actions and events: the number of actors, the "communication topology'', even the numerical bounds in the time constraints.

A number of obstructions to a fully adequate logical analysis are figured out:
* A global continuous time implies an over-complicated set of trajectories.
* Potentially unbounded number of actors and dynamically configured topology of actors push us out beyond the finite automata paradigm.
* Global quantitative time constraints push us out beyond the Markov processes property (that is, the Present determines the Future); whereas the proofs are always "Markovian''.
* Besides, a common user is used to describe actions and events in his own terms by means of a Horn-like format: if ... then ... .

The aim of the talk is to show that the Horn fragment of linear logic provides us with a fully adequate logical formalism for the real-time systems under consideration.

The "non-Markovian'' problem is circumvented by introducing hidden variables recorded by "time-guards''.

For the underlying trajectories with time-guards we introduce an exact bisimulation equivalence (together with a high-school proof of its correctness, based on the combination: a coarse hour-glass + a precise one-hand watch).

Back to seminars list

 

Geometry of Proofs and Models of Computation

Esfandiar Haghverdi
University of Ottawa

Thursday, April 27, at 3:00 in DRL 4E9 

 Girard introduced his Geometry of Interaction Programme (GoI) in a series of influential papers. The goal of this programme was to provide a mathematical analysis of the cut elimination process in linear logic proofs. This new interpretation replaces graph-rewriting by information flow in proof-nets. A specific model considered by Girard was based on the C*-algebra of bounded linear operators on the space l^2. From a computational point of view this yields an analysis of l-calculus b-reduction and has been applied in such areas as the analysis of optimal reduction strategies. GoI has also brought forward a new perspective for the semantics of computation which places it in a kind of "middle ground'' between imperative/procedural, denotational/operational approaches in the semantics of programming languages. This new view helps to model the computational dynamics which is absent in denotational semantics and manages to offer a mathematical analysis which is lacking in operational semantics.

In this talk we give a general categorical framework for the Girard programme inspired by recent work of Samson Abramsky. We show how to construct linear combinatory algebras and models of untyped combinatory logic in this framework. In particular, we will focus on combinatory algebras constructed using a special class of traced symmetric monoidal categories called traced unique decomposition categories. These categories provide an algebraic setting for an important class of examples and axiomatize the "particle-style" GoI along with providing a computational calculus.

Back to seminars list

 

Supervisory Control of Distributed Systems using Petri Nets and PartialOrder Methods

Kevin X. He
Notre Dame

Monday, April 24, 2000, 4:30 PM
Moore 554

 A distributed system is a system that consists of a group of distributed and communicating processes. Examples of such systems arise in robotic manufacturing systems, computer networks, telecommunication systems and systems with networked embedded microprocessors. This talk introduces a systematic way to achieve automatic generation of maximally permissive supervisors or supervisory software plug-ins that ensure desired system behavior. The approach is based on a discrete event model called Petri net and a partial order method called network unfolding. A Petri net is a bipartite graph consisting of places, transitions and directed arcs connecting places and transitions. An unfolding is a net homomorphism that maps the original net to an acyclic occurrence net. Petri nets provide compact and convenient models for distributed systems, while unfoldings identify concurrent, cyclic, and causally related fundamental executions within the system. The maximally permissive supervisor is efficiently constructed by restricting undesirable interactions among fundamental executions. A distributed cache system example is also provided to illustrate this approach. 

Back to seminars list

 

Hierarchical Design and Analysis of Reactive Systems

Radu Grosu
University of Pennsylvania

Monday, February 28, 2000, 4:30 PM
Moore 554

Computer based reactive systems are becoming an integral part of nearly every engineered product: they control consumer products, commercial aircraft, nuclear power plants, medical devices, weapon systems, aerospace systems, automobiles, public transportation systems, and so on. At the same time quality and confidence issues are increasing in importance. Software errors have resulted in loss of life, destruction of property, failure of businesses, and environmental harm. To master and speedup the development cycle of these increasingly complex systems, software engineers proposed the object oriented methods, currently standardized in form of UML and UML for Real Time. To increase the confidence in reactive systems, researchers developed formal analysis methods and tools. Among them model checkers are one of the most popular. Unfortunately, formal analysis tools did not scale up yet in a satisfactory way. Moreover, there is a considerable gap between the software engineering and the formal methods.

Our main research goal is to close this gap and to use the well established software engineering concepts to scale up the analysis tools. In this talk, we present the theory of modular design and reasoning for the behavior hierarchy of reactive systems. This describes the control structure of a system by 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. This provides the basis for a refinement notion between modes that is compositional with respect to the mode constructors. We show how these concepts may be used for modular reasoning and for building a model checker that exploits the mode hierarchy.

Back to seminars list

 

Reconciling message sequence charts and state machines

Kousha Etessami
Bell Labs, Lucent Technologies

Monday, February 21, 2000, 4:30 PM
Moore 554

I will describe message sequence charts (MSCs) and give examples of how they are being used in early modeling of software systems. I will then describe a framework for reconciling MSCs with the more familiar state machine model of concurrent software. In this framework we give an algorithm for inferring unspecified MSCs from a set of MSCs which supply a partial description of the behaviors of the system, and an algorithm for synthesizing concurrent state machines giving the "most conservative" realization of the behaviors specified by a given set of MSCs.

Based on a joint paper with Rajeev Alur and Mihalis Yannakakis, to appear in 22nd Intl Conf on Software Engineering (ICSE 2000) 

Back to seminars list

 

Process Algebraic Approach to the Parametric Analysis of Real-time Scheduling Problems

Hee Hwan Kwak
University of Pennsylvania

Monday, January 31, 2000, 4:30 PM
Moore 554

This talk describes a general framework for parametric analysis of real-time systems based on process algebra and illustrates the usefulness of a process-algebraic framework by applying this method to real-time scheduling problems.

The Algebra of Communicating Shared Resources (ACSR) has been extended to ACSR with Value-passing (ACSR-VP) in order to model the systems that pass values between processes and change the priorities of events and timed actions dynamically. In order to capture the semantics of ACSR-VP process terms, we propose a Symbolic Graph with Assignment (SGA). We further presents an algorithms for computing symbolic weak bisimulation for ACSR-VP processes.

With our new framework the scheduling problem in real-time systems is reduced to the problem of solving predicate equations, a boolean expression, or the set of sequential boolean equations. A solution to them yields the values of the parameters that make the system schedulable. To solve predicate equations with unknown parameters, we
demonstrate the use of constraint logic programming techniques. A boolean expression with unknown parameter can be solved by integer programming tools, and we present new algorithms to solve a set of boolean equations with unknown parameters. 

Back to seminars list

 

An Implicitly-Typed Deadlock-Free Process Calculus

Naoki Kobayashi
University of Tokyo

Monday, January 17, 2000, 4:30 PM
Moore 554

We have extended Kobayashi and Sumii's type system [1, 2] for the deadlock-free Pi-calculus and developed a type reconstruction algorithm. Kobayashi and Sumii's type system is a generalization of Kobayashi, Pierce, and Turner's linear pi-calculus, and it helps high-level reasoning about programs by guaranteeing that communication on certain channels will eventually succeed. It can ensure, for example, that a process implementing a function really behaves like a function. However, because it lacked a type reconstruction algorithm and required rather complex type annotations, it was impractical to apply it to real concurrent languages. We have therefore developed a type reconstruction algorithm for an extension of the type system. The key novelties that made it possible are generalization of the usages (which was first introduced in [2]) and a subusage relation.

In this talk, I will first summarize the ideas of Kobayashi and Sumii's original deadlock-free process calculus, and then explain how we extended it and obtained its type reconstruction algorithm.

Joint work with Shin Saito and Eijiro Sumii

[1] Kobayashi, "A Partially Deadlock-Free Typed Process Calculus," ACM TOPLAS, 20(2), pp.436--482, 1998

[2] Sumii and Kobayashi, "A Generalized Deadlock-Free Process Calculus," Proceedings of HLCL'98, ENTCS, 16(3), 1998.

Back to seminars list

Back to seminars home page