School of Computing Science : Events

Asynchronous Systems Labs (ASLs)

The aim of this seminar series is to provide a forum for research staff and students to present and discuss work on a wide range of topics related to the theory and applications of concurrent and distributed systems. The meetings are organised jointly by the School of Computing Science (Maciej Koutny) and the School of Electrical, Electronic and Computer Engineering (Alex Yakovlev).

At the moment there are no ASLs scheduled

Past ASLs

August 12, 2011 3-5pm, CPD room (M413) , Merz Court
Spatial processing of the SPICE circuit simulator using reconfigurable architectures
Nachiket Kapre: Spatial processing of the SPICE circuit simulator using reconfigurable architectures (i.e. FPGAs) can deliver an order of magnitude speedup over conventional processors (i.e. Intel multi-core CPUs) for a range of benchmark circuits. SPICE has historically been hard to parallelize due to the irregular nature of the computation. In this talk, I show how to expose the different, irregular parallel patterns inherent in SPICE using a high-level, domain-specific framework capable of composing multiple patterns simultaneously on the same FPGA fabric. I will also briefly overview some recent, preliminary enhancements that can further improve the SPICE FPGA design.
August 9, 2011 11am, CPD room (M413) , Merz Court
Understanding the State of the Art in Energy-Aware System Design and first results of applying this to the XMOS processor
Kerstin Eder: Understanding the State of the Art in Energy-Aware System Design and first results of applying this to the XMOS processor Nine months into a Royal Academy of Engineering Industrial Secondment focused on Understanding the State of the Art in Energy-Aware System Design this presentation gives an overview of techniques developed to model, analyse and optimize energy consumption at different levels of abstraction within the system stack. It becomes clear that collaboration will be the key to success in addressing the challenges of Energy-Aware System Design because a good understanding of the entire system stack is required, starting from application software and algorithms, via programming languages, compilers, instruction sets and micro architectures, down to the design and manufacture of the hardware. This talk also gives an insight into the challenges encountered while modelling and analysing software energy consumption in a hardware multi-threaded architecture on the example of the XMOS XCore architecture. I conclude by presenting the vision behind the Energy Aware COmputing initiative series that I have recently introduced at Bristol: http://www.cs.bris.ac.uk/Research/Micro/eaco.jsp
May 6, 2011 3pm, CPD room (M413) , Merz Court
Energy-Modulated Computing
Alex Yakovlev: For years people have been designing electronic and computing systems focusing on improving performance but “keeping power and energy consumption in mind”. This is a way to design energy-aware or power-efficient systems, where energy is considered as a resource whose utilization must be optimized in the realm of performance constraints. Increasingly, energy and power turn from optimization criteria into constraints, sometimes as critical as, for example, reliability and timing. Furthermore, quanta of energy or specific levels of power can shape the system’s action. In other words, the system’s behaviour, i.e. the way how computation and communication is carried out, can be determined or modulated by the flow of energy into the system. This view becomes dominant when energy is harvested from the environment. In this talk, we attempt to pave the way to a systematic approach to designing computing systems that are energy-modulated. To this end, several design examples are considered where power comes from energy harvesting sources with limited power density and unstable levels of power. Our design examples include voltage sensors based on self-timed logic and speed-independent SRAM operating in the dynamic range of Vdd 0.2-1V. Overall, this talk advocates the vision of designing systems in which a certain quality of service is delivered in return for a certain amount of energy.
May 5, 2011 3pm, CPD room (M413) , Merz Court
Biometrics: limitations and future research
Feng Hao: Biometrics has been an active research subject for many years. In this talk, I'll first explain my involvement in this area in the two published papers by IEEE Transactions journals. The first paper addresses the problem that how to effectively integrate biometrics into cryptographic applications despite the fuzziness of data (Hao,Anderson,Daugmna'06). The second paper address the search problem that how to efficiently store and retrieve biometric data (Hao,Daugman,Zielinski'08). I'll share some of my thoughts about the future of biometric research. It seems to me that this research area has reached a bottleneck. Inventing new types of biometrics is highly unlikely; improving existing biometric systems to a substantial extent seems very difficult as well. However, in this world, not only humans have biometrics. In fact, an physical object has "biometrics" that naturally occur, are unique and can't be cloned. If we keep an open-mind, we might find there are plenty of new research avenues and challenges.
April 21, 2011 3pm, CPD room (M413) , Merz Court
Antennas for Medical Applications
Kenneth Tong: Besides wireless communications, antennas are used in various medical areas, for instance Microwave Tomography, Hyperthermia Cancer Treatment, Parkinson Disease Treatment and Intra-Cortical Proximity Communications. In the seminar, we will discuss how novel antenna design can help these techniques to battle the complex and non-homogenous environment of human body for maximum performance. Some of the preliminary results will be presented as well.
April 15, 2011 3pm, The Buttery, 4th Floor, Merz Court
Predictability Verification with Petri Net Unfoldings
Agnes Madalinski: Fault diagnosis determinates if an "invisible" fault has occurred in a partially observable system. A fault is predictable if it is possible to deduce about future occurrences of the fault based on the observable record before it occurs. If it is possible to predict the occurrence of a fault when a warning can be issued and preventive measures can be taken. We show how predictability can be verified with Petri net unfoldings.
April 15, 2011 11am, The Buttery, 4th Floor, Merz Court
Insertion Modeling in Distributed Systems Design
Alexander Letichevsky: The talk describes insertion modeling methodology, its theory, implementation and applications. Insertion modeling is a methodology of model driven distributed system design. It is based on the model of interaction of agents and environments. Both agents and environments are characterized by their behaviors represented as the elements of continuous behavior algebra, a kind of the ACP with approximation relation, but in addition each environment is supplied by an insertion function, which takes the behavior of an agent and the behavior of an environment as arguments and returns a new behavior of this environment. Each agent can be considered as a transformer of environment behaviors and a new kind of equivalence of agents weaker than bisimulation is deﬁned in terms of the algebra of behavior transformations. Arbitrary continuous functions can be used as insertion functions and rewriting logic is used to deﬁne computable ones. The theory has applications for studying distributed computations, multi agent systems and semantics of speciﬁcation languages. In applications to distributed system design we use Basic Protocol Specification Language (BPSL) for the representation of requirement specifications of distributed systems. The central notion of this language is the notion of basic protocol, a sequencing diagram with pre- and postconditions represented as logic formulas interpreted by environment description. Semantics of BPSL allows concrete and abstract models on different levels of abstraction. Models defined by Basic Protocol Specifications (BPS) can be used for verification of requirement specifications as well as for generation of test cases for testing products, developed on the basis of BPS. Insertion modeling is supported by the system VRS (Verification of Requirement Specifications), developed for Motorola by Kiev VRS group. The system provides static requirement checking on the base of automatic theorem proving, symbolic and deductive model checking, and generation of traces for testing with different coverage criteria. All tools have been developed on a base of formal semantics of BPSL constructed according to insertion modeling methodology. The VRS has been successfully applied to a number of industrial projects from different domains including Telecommunications, Telematics and real time applications. Prof Alexander Letichevsky is a member of the National Academy of Sciences of Ukraine, and is a famous computer scientist of the former Soviet Union. He graduated from Kiev State University in 1957 and till now works for Glushkov Institute of Cybernetics (before 1961 it was Computational Centre, then Institute of Cybernetics and from 1982 Glushkov Institute of Cybernetics) of the National Academy of Sciences of Ukraine. Scientific interests of Prof Letichevsky were changing during his scientific life and include automata theory, theory of programming, formal methods in software and hardware design, computer algebra, automatic reasoning, parallel computation, and software verification. Prof Letichevsky took part in many industrial projects including computers MIR with hardware implementation of high level programming languages, computer algebra system Analytic (1960), Macroconveyer computers (multiprocessor MIMD computing systems with distributed memory, 1980) and many other projects.
March 9, 2011 4pm, CPD room, Merz Court
Parallelism in asynchronous on-chip routers
Wei Song: State-of-the-art multi-processor system-on-chips use on-chip networks as their communication fabric. Although most of current on-chip networks are implemented synchronously, asynchronous quasi-delay-insensitive (QDI) on-chip networks have several advantages over their synchronous counterparts. Timing division multiplexing (TDM) flow control methods have been utilized in asynchronous on-chip networks extensively. The data synchronization required by TDM leads to significant speed penalty. Compared with using TDM methods, exploring spatial parallelism and applying the spatial division multiplexing (SDM) flow control method achieve better network throughput with less area overhead. Channel slicing is a pipeline structure that alleviates the speed penalty by removing the synchronization among bit-level data pipelines. SDM is a flow control method that improves network throughput without introducing synchronization among buffers of different frames, which is required by TDM methods on the contrary. The major design problem of SDM is the area consuming crossbars. A novel 2-stage Clos switch structure is proposed to replace the crossbar in SDM routers, which reduces the area overhead significantly. This Clos switch is dynamically reconfigured by a new asynchronous dispatching algorithm. An asynchronous SDM router is implemented using these new techniques. An asynchronous router using VC is also reproduced for comparison. Performance analyses show that the SDM router outperforms the VC router in throughput, area to throughput efficiency and power to throughput efficiency.
January 25, 2011 11am-1pm (11am-1pm on 26 January, 12noon-2pm on January), Room 1.02, Claremont Tower
Reaction Systems - (3 day course: 25th, 26th and 27th January)
G.Rozenberg: This course builds on a colloquium on 24th January (http://www.cs.ncl.ac.uk/events). The 3-day course will be self-contained and will address both the biological and computational aspects of the reaction systems. ABSTRACT: Natural Computing is an interdisciplinary field of research that investigates human-designed computing inspired by nature as well as computation taking place in nature, i.e., it investigates models, computational techniques, and computational technologies inspired by nature as well as it investigates phenomena/processes taking place in nature in terms of information processing. One of the research areas from the second strand of research is the computational nature of biochemical reactions. It is hoped that this line of research may contribute to a computational understanding of the functioning of the living cell, which is based on interactions between (a huge number of) individual reactions. These reactions are regulated, and the main regulation mechanisms are facilitation/acceleration and inhibition/retardation. The interactions between individual reactions take place through their influence on each other, and this influence happens through these two mechanisms. In our lecture we present a formal framework for the investigation of processes carried by biochemical reactions. We motivate this framework by explicitly stating a number of assumptions that hold for a great number of biochemical reactions, and we point out that these assumptions are very different from the ones underlying traditional models of computation. We discuss some basic properties of processes carried by biochemical reactions, and demonstrate how to capture and analyse, in our formal framework, some biochemistry related notions. Besides providing a formal framework for reasoning about processes instigated by biochemical reactions, the models discussed in the lecture are novel and attractive from the (theoretical) computer science point of view.
December 21, 2010 3pm, Merz Court M.4.13 (CPD)
Application Specific Routing Algorithms for Networks on Chip
Maurizio Palesi: In this talk we present a methodology to develop efficient and deadlock free routing algorithms for Network-on-Chip (NoC) platforms which are specialized for an application or a set of concurrent applications. The proposed methodology, called Application Specific Routing Algorithm (APSRA), exploits the application specific information regarding pairs of cores which communicate and other pairs which never communicate in the NoC platform to maximize communication adaptivity and performance. The methodology also exploits the known information regarding concurrency/non-concurrency of communication transactions among cores for the same purpose. The methodology does not require virtual channels to guarantee deadlock freedom. We demonstrate, through analysis of adaptivity as well as simulation based evaluation of latency and throughput, that algorithms produced by the proposed methodology give significantly higher performance as compared to other deadlock free algorithms for both homogeneous as well as heterogeneous 2D mesh topology NoC systems. Since APSRA methodology is topology agnostic, the most appropriate general implementation of the routing function within the router is using a table. A table-based implementation of the router is costlier as compared to an algorithm-based implementation. We also propose a technique to compress routing table in a mesh topology NoC to very small sizes with very little negative effect on routing adaptivity.
November 19, 2010 1pm, Merz Court L302
Circuit development with Workcraft
Stanislavs Golubcovs: Workcraft is an integrated development system designed to create various mathematical models. It is integrated with such external tools as Petrify, Punf, and Mpsat and can simplify and partially automate the asynchronous circuit design. With new features is now also useful for the modelling, simulation and formal verification of digital circuits. A model of a circuit is composed out of function components that represent circuit logic gates (or even more complex elements). Each function component can be represented with set/reset Boolean equations. These equations are not limited by the number of inputs, therefore, gates of arbitrary complexity can be created for the experimentation prior to decomposition. It is possible to mark functional blocks to be treated as part of the environment. The technique is useful for specifying components with internal conflicts such as mutex elements. These conflicts are being put outside the scope of the model and are not considered during the verification phase. Finally, the simulation of the circuit it based on the Circuit Petri Net beneath it and essentially inherits all of the features available for the STG simulation.
September 24, 2010 2pm, The Buttery, Merz Court
Automated Design Optimization for Low Power Reconfigurable Systems
Qiang Liu: To meet design goals, designers of computational hardware must perform multiple optimizations, making it difficult to provide optimized designs quickly. Starting from sequential programs, we present an approach combining data reuse, multi-level MapReduce, and pipelining to automatically find the most power-efficient designs that meet speed and area constraints in the design space on Field-Programmable Gate Arrays (FPGAs). The combined design space exploration is formulated as a Geometric Programming model, leading to globally optimized designs. This combined approach enables trade-offs in power, speed and area: we show 63% reduction in power can be achieved with 27% increase in execution time. Compared to the sequential designs, our approach yields designs with up to 158 times reduction in execution time. Moreover, for a given execution time, our combined approach generates designs using up to 28.6% less power than those produced by the same optimizations applied separately and can also find solutions missed by separating the optimizations.
September 8, 2010 11am, The Buttery, Merz Court
Controlling biomimetic robots with electronic nervous systems
Joseph Ayers: We build biomimetic robots based on simple neurobiological models, the lobster, honeybees and sea lamprey. The robots feature a physical plant that captures the biomechanical advantages of the body form, a neuronal circuit-based controller, neuromorphic sensors, myomorphic actuators and a behavioral set based on action patterns, reverse engineered from movies of the animal models. Our controllers are based on neuronal circuits established from neurophysiology. To achieve real-time operation, we base our electronic neurons on nonlinear dynamical models of neuronal behavior rather than physiological models. We employ both UCSD electronic neurons and synapses (analog computers that solve the Hindmarsh-Rose equations) and discrete time map based neurons and synapses that are integrated on a DSP. Together these components provide an integrated architecture for the control of innate behavioral action patterns and reactive autonomy.
August 24, 2010 9.30-11.00, The Buttery
Infrastructure Support for Real-Time Network Architecture
Hugo Simpson: The Real-Time Network Architecture (RTNA) is characterised by structural forms in which independently operating concurrent functions interact through explicitly identified connectors. RTNA has proved to be highly successful in the development of multi-tasking multi-processing embedded real-time systems. This talk will focus particularly on hardware micro-kernel techniques which can be used to support the interaction and scheduling concepts implicit in RTNA. A notation is introduced to express the functionality of the micro-kernel and it is shown how this translates into clock-free gate-level electronic designs. Although RTNA originates in the real-time distributed systems field, it is directly applicable to any development problem in which efficient computing resource utilisation and low electrical power consumption are primary concerns.
August 18, 2010 12.30-2.00, CPD (M413) room, Merz Court
Hebbian Eigenfilter for Neurophysiological Spike Train Analysis
Bo YU: The emergence of micro-electrode array enables the study of real-time neurophysiological activities across multiple regions of the brain. However, the real-time extracellular voltage potentials recorded on any electrode represent the simultaneous electrical activity of an unknown number of neurons which present a critical challenge to the accuracy of interpretation and identification of the neural circuitry in the subsequent analysis. In this talk, we present a principal component analysis approach utilizing Hebbian eigenfilter to identify the corresponding electrical activities to each neuron, or namely spike sorting. We designed Hebbian eigenfilter hardware by Xilinx System Generator and evaluated software and hardware using synthetic spike train.
July 13, 2010 2pm, Room M413 (Merz Court)
A New Type of Behaviour-Preserving Transition Insertions in Unfolding Prefixes
Victor Khomenko: A new kind of behaviour-preserving insertions of new transitions in Petri nets is proposed, and a method for computing such insertions using a complete unfolding prefix of the Petri net is developed. Moreover, as several transformations often have to be applied one after the other, the developed theory allows one to avoid (expensive) re-unfolding after each transformation, and instead use local modifications on the existing complete prefix to obtain a complete prefix of the modified net.
July 2, 2010 2pm, The Buttery, Merz Court
Diagnosability Verification with Parallel LTL-X Model Checking Based on Petri Net Unfoldings
Agnes Madalinski: We show that the diagnosability problem on a Petri net can be re-formulated in terms of LTL-X model checking. The advantage of this is that existing efficient methods and tools can be employed, in particular parallel model checking based on Petri net unfoldings. The experimental results show that this approach is efficient, and a good level of parallelisation can be achieved.
June 8, 2010 1pm, Room M4.13 Merz Court
Constructing and exploring a design space
Graham Birtwistle: The talk presents a systematic way of studying design spaces applied to timed and untimed, bundled, 2-- and 4phase asynchronous latch controllers. The work is joint work with Ken Stevens ECE Utah who supplies all the engineering insights and expertise. We derive a model for asynchronous latch controllers tailored to the study of their behaviours when pipelined in series, parallel, rings, .... Starting with the most state rich behaviour satisfying a protocol, we systematically cut away states to generate families of reduced-state behaviours. The cuts enable all behaviours to be ordered and related. They predict behaviours when pipelined singly, in parallel, in rings ... and such properties as liveness and occupancy. The cuts also reveal the full design space. Ken has (almost) automated the generation of circuits from our models and generated novel designs with good behaviours. Graham Birtwistle entered his 7th decade of university life this year (work that one out). He has a PhD from Sheffield on the behaviour of thin arch dams, and has worked in Norway on Simula compilers and Canada on hardware verification in HOL and CCS. Ever tha man to catch the tidal wave of research his chief claim to fame lies in being (somewhat contested) the first man to give up OO programming (1984 appropriately).
May 24, 2010 2pm, The Buttery, Merz Court
Towards Hybrid Neural-Silicon Sensorimotor Systems
Terrence Mak: Sensorimotor system governs the dynamics of learning and adaptation that enables high performance cognitive and behavioural activities in biological organisms. In parallel with the development in neuroscience, microelectronic technology quickly evolves into a regime that is almost compatible to biological neural systems, in terms of computational power. Hybrid neural-silicon system becomes possible and such system will have profound implications in engineering design, from prosthetics to sensorimotor control that advance human abilities. In this talk, I will outline the major microelectronic design obstacles to build such hybrid sensorimotor systems. New research initiatives and novel design methodologies, including high-performance neural signal processing, power management, and real-time dynamic optimization, along with the direction of hybrid neural-silicon sensorimotor systems will be presented.
May 12, 2010 1pm, The Butter, Merz Court
Visualisation in Circuit Design
Ian W. Jones, Sun Labs, Oracle: Visualisation techniques can enhance the understanding of circuit behaviour and their operating environment. Visualisation enables exploration of massive quantities of data from a high-level overview right down to low-level detail. I will present some short animated movies that address clock domain crossing circuits, and whole-chip clock distribution. These visualisation aids are used to tune and debug designs, and have uncovered problems not found by the standard development tools.
March 5, 2010 1pm, CLT.701
Modelling Gradients Using Petri Nets
Laura M.F. Bertens: Motivated by the graded posteriorization during the AP axis development in Xenopus laevis, we propose a Petri Net model for establishing a gradient of proteins in a chain of cells. We analyze its properties and robustness.
February 26, 2010 3pm, Room M413 (Merz Court)
Statistical Tool Framework for Circuit Variability Simulation
Ghaith Tarawneh: Statistical simulation is quickly replacing purely deterministic and corner-based approaches in characterizing the performance of circuits. Despite the rising need, current simulation tools and methodologies fall behind on providing adequate statistical functionality to evaluate designs under severe variability effects. We introduce a new framework built on top of SPICE and a GNU Matlab clone (Octave) that enable researchers to run extensive statistical simulations in a flexible yet fully-automated environment. The development of the tool will be discussed in terms of SPICE simulation technology and software engineering, followed by a demonstration of some interesting simulation results obtained using the tool.
February 5, 2010 3pm, The Buttery, Merz Court
ASL: the next ten years and beyond
Alex and Maciej: This will be a special ASL meeting to celebrate the 10th anniversary of the very firt ASL talk : January 20, 2000 12pm, Room 922; Formal Modelling of Asynchronous Hardware; Alex Yakovlev We will discuss some of our past research as well as plans for the future.
December 11, 2009 1pm, Buttery, Merz Court
Specification and synthesis of processors using CPOG-based methodology
Maxim Rykunov: Design automation of embedded systems involves the process of co-designing hardware and software for a given application or, to be more clear, a set of functional and performance. In the aspect of reducing specialized hardware and software co-design for a particular CPU, the most recent grand challenge is developing Computer-Aided Design (CAD) tool support for automatic synthesis of processors. So in this way the problem could be formulated as taking some legacy software code for some and synthesizing a new CPU (its micro-architecture, circuits and even instruction sets) optimal for the given requirements. There are some original theoretical ideas and models such as Conditional Partial Order Graphs (CPOG). CPOG-based methodology has already shown its high potential to solve such problems on simplified example processor. Now research is continuing on more representative, therefore more complex CPU and also well-known one (Core of MCS 80C51). Till now there were several things on this problem done: 1. Code analysing and overlaying all instructions into a CPOG description; 2. Boolean encoding of synthesized CPOG and mapping them to Boolean equation; 3. Translate into HDLs; 4. Synthesis of schematic implementation.
December 3, 2009 11 am, Merz Court room M4.13 (CPD)
Output-Determinacy and Asynchronous Circuit Synthesis
Victor Khomenko: Signal Transition Graphs (STG) are a formalism for the description of asynchronous circuit behaviour. In this talk we propose (and justify) a formal semantics of non-deterministic STGs with dummies and OR-causality. For this, we introduce the concept of output-determinacy, which is a relaxation of determinism, and argue that it is reasonable and useful in the speed-independent context. We apply the developed theory to improve an STG decomposition algorithm used to tackle the state explosion problem during circuit synthesis, and present some experimental data for this improved algorithm and some benchmark examples.
November 20, 2009 10am, Merz Court room M4.13 (CPD)
On automated Fault diagnosis in Service oriented Architectures
Behzad Bordbar: Creating systems to identifying occurrences of failure is one of the key challenges of Service oriented Architectures (SoA). This is often achieved by creating Diagnosers that monitor the interaction between services to identify if a type of failure has happened or may have happened. This talk aims to report on our recent results on the application of Discrete Event Systems (DES) techniques to failure detection in SoA. Firstly, a brief introduction to Diagnosability theory in DES will be presented. Then an outline of a formal representation of business processes that allows specifying interactions between services will be described. This formal representation, which is motivated by Petri nets, draws on Business Process modelling style used in major tools such as IBM Websphere and Oracle JDeveloper. Relying on the formalism an algorithms for creating Diagnosers will be explained. Finally, after a brief explanation of the sketch of the proof of correctness of the algorithm, a set of empirical results created by an implementation as an Oracle JDeveloper plugin will be described.
November 9, 2009 1pm, Room 701, Claremont Tower
Mobile Membranes
Gabriel Ciobanu: Membrane computing belongs to the more general area of natural computing. Membrane systems represent parallel and non-deterministic computing models which abstract from the functioning and structure of the cell. We have investigated variants of mobile membrane systems as models for molecular computing. On one hand, we follow the standard approach of research in membrane computing: defining a notion of computation for mobile membrane systems, and investigating the computational power of such computing devices. Specifically, we address issues concerning the power of operations for a new class of mobile membrane working with endocytosis (moving a membrane inside a neighbouring membrane) and endocytosis (moving a membrane outside the membrane where it is placed). On the other hand, we relate mobile membrane systems to mobile ambients, timed mobile ambients, pi-calculus and brane calculi by providing some encodings and adding some concepts inspired from process algebra in the framework of mobile membrane computing.
October 30, 2009 1pm, Merz Court room M4.13 (CPD)
Organize the engines in a laissez-faire and natural way
Xiangyu Li: Our group belongs to the Division of Integrated Circuit and System Design of Institute of Microelectronics, Tsinghua University. Research in our lab is about developing new circuits and architectures for future signal processing system chip and security IC. Our main interested fields include the asynchronous circuit and data-flow processor, implementation security of crypto VLSI and particle detection system. Two random order executing AES processor which is based on data-flow architecture and asynchronous circuit technique have been developed. Their key feature is side channel attack resistance with low power. This work resolves the control problem in random order executing ASIC. Scheduling in a multi-heterogeneous-task data-driven SoCs based on data-flow and asynchronous communication is a next interested topic. One of the example applications is the wireless sensor network node. Data flow mode is suitable for the multi-task parallel scheduling, the random task request arrival timing and the event-driven feature. Controller and interconnection with power management consideration are the critical issues.
October 13, 2009 1pm, Room 701, CLT
A Unifying Analytical Framework for Discrete, Linear Time
Ben Moszkowski: Discrete, linear state sequences provide a compellingly natural and flexible way to model many dynamic computational processes involving hardware or software. Over 50 years ago, the distinguished logicians Church and Tarski initiated the study of a fundamental and powerful class of decidable calculi for rigorously describing and analysing various basic aspects of discrete, linear-time behaviour. The number of such formalisms has significantly grown to include many temporal logics, some of which are employed in industry, and even found in IEEE standards. They are intimately connected with regular languages, analogues for infinite words called omega-regular languages and the associated finite-state automata. We describe a promising hierarchical approach for systematically analysing and relating such logics. Our framework is based on Interval Temporal Logic (ITL), a well-established, stable formalism first studied over 25 years ago. It offers a greatly simplified way to show axiomatic completeness for such logics and for some of them even suggests new improved axioms and inference rules. This is in itself a definite advance over previous work of the last roughly 40 years on axiomatic completeness which in contrast embedded complicated deductions involving nontrivial techniques such as the complementation of nondeterministic finite-state automata which recognise infinite words. Our presentation also offers intriguing evidence that Propositional ITL (PITL) might play a central role in the overall proof theory of this class of notations, and perhaps will eventually come to be regarded as the canonical propositional logic of linear, discrete time. Furthermore, PITL also provides a starting point for decidable calculi which formalise memory, framing and multiple time granularities as well as for a calculus of sequential and parallel composition based on Hoare triples having assertions expressed in temporal logic. In view of all of this, ITL in the future might be recognised as more than just a unifying, canonical notation for exploring discrete, linear time systems. It could also be seen as a key analytical formalism for investigating associated programming semantics and calculi as well as both regular and omega-regular languages.
October 2, 2009 1pm, Merz Court room M4.13 (CPD)
Workcraft - a tool for Interpreted Graph Models
Ivan Poliakov: A large number of models that are employed in the field of concurrent systems design, such as Petri Nets, Signal Transition Graphs, gate-level circuits, Static Data Flow Structures and Conditional Partial Order Graphs have an underlying static graph structure. Their semantics, however, is defined using additional entities, e.g. tokens or node/arc states, which in turn form the overall state of the system. We jointly refer to such formalisms as Interpreted Graph Models. The similarities in notation allow for links between different models to be created, such as interfaces between different formalisms or conversion from one model type into another, which greatly extend the range of applicable analysis techniques. The Workcraft tool is designed to provide a flexible common framework for development of Interpreted Graph Models, including visual editing, (co-)simulation and analysis. The latter can be carried out either directly or by mapping a model into a behaviourally equivalent model of a different type (usually a Petri Net). Hence the user can design a system using the most appropriate formalism (or even different formalisms for the subsystems), while still utilising the power of Petri Net analysis techniques. The tool is platform-independent, highly customisable by means of plug-ins, and is freely available for academic use.
June 4, 2009 2pm, Room CLT.701
Structured Occurrence Nets
Brian Randell - joint work with Maciej Koutny: This talk introduces the concept of a 'structured occurrence net', which is based on that of an 'occurrence net', a well-established formalism for an abstract record that represents causality and concurrency information concerning a single execution of a system. Structured occurrence nets consist of multiple occurrence nets, associated together by means of various types of relationship, and are intended for recording either the actual behaviour of complex systems as they communicate and evolve, or evidence that is being gathered and analysed concerning their alleged past behaviour. The talk discuss how structured occurrence nets could form a basis for improved techniques of system failure prevention and analysis. Note: This is a joint SRG/ASL talk.
May 15, 2009 2:30pm, Merz Court room M4.13 (CPD)
Prospects for Energy Harvesting Devices
Bashir M. Al-Hashimi: Continuing innovation in low power hardware and software is extending the battery life in mobile devices. At present there is clear opportunity to develop complementary and alternative energy sources for self-powered electronics for emerging applications areas including autonomous environmental, industrial monitoring and personalised healthcare. In this talk I will outline the key multidisplinary knowledge and expertise needed to carry out research in energy harvesting electronics and will provide comprehensive overview of the state-of-the-art research and development in energy harvesting electronics including micro generators, ultra low power design, modelling and optimisation tools with examples drawn from the Pervasive System Centre at the Uni. of Southampton.
April 29, 2009 2.30-3.30pm, M4.13 Merz Court
Connection-Centric Network for Spiking Neural Networks
Robin Emery: A reconfigurable network architecture applied to spiking neural networks is presented. For hardware platforms for neural networks that implement some degree of realism of interest to neuroscientists, connectivity between neurons can be a major limitation. Recent data indicates that neurons in the brain form clusters of connections. Through the combination of this data and a routing scheme that uses a hybrid of short-range direct connectivity and an AER (Address Event Representation) network, the presented architecture aims to provide a useful amount of inter-neuron connectivity. A connection-centric design can provide opportunities for NoCs such as optimising power, bandwidth or introducing redundancy. A method of mapping a network to the architecture is discussed, along with results of optimal hardware specifications for a given set of network parameters.
April 6, 2009 2pm, Merz Court Room L302
Modular approach to multi-resource arbiter design
Stanislavs Golubcovs: When circuits need to be constructed out of several self timed parts that access shared resources, asynchronous arbitration is often required. We consider the creation of the general purpose arbiter delegating resources to clients for the cases when the resources can be either active or passive participants of the arbitration. Firstly, the solution is provided for the case of two active resources being offered to two clients. Then a general case of N clients and M resources is shown. Finally, on the basis of the arbiter designed, it is shown how it can be used to create a scalable multi-resource arbiter for passive resources
March 20, 2009 1pm, Room M413, Merz Court
Towards Efficient Verification of Systems with Dynamic Process Creation
Hanna Klaudel: Modelling and analysis of dynamic multi-threaded state systems often encounters obstacles when one wants to use automated verification methods, such as model checking. Our aim in this paper is to develop a technical device for coping with one such obstacle, namely that caused by dynamic process creation. We first introduce a general class of coloured Petri nets---not tied to any particular syntax or approach---allowing one to capture systems with dynamic (and concurrent) process creation as well as capable of manipulating data. Following this, we introduce the central notion of our method which is a marking equivalence that can be efficiently computed and then used, for instance, to aggregate markings in a reachability graph. In some situations, such an aggregation may produce a finite representation of an infinite state system which still allows one to establish the relevant behavioural properties. We show feasibility of the method on an example and provide initial experimental results.
February 4, 2009 1pm, L101 (Merz Court)
Flat Arbiters
Andrey Mokhov: In this paper we propose a new way of constructing Nway arbiters. The main idea is to perform arbitrations between all pairs of requests, and then make decision on what grant to issue based on their outcomes. Crucially, all the ME elements in such an arbiter work in parallel. This ‘flat’ arbitration is prone to new threats such as formation of cycles (leading to deadlocks), but at the same time opens new opportunities for designing arbitration structures with different decision policies due to the availability of the global order relation between requests. To facilitate resolution of such cycles and further developments in the context of flat arbitration, the paper presents new theoretical results, including a proof of correctness of a generic structure for the N-way arbiter decision logic.
December 12, 2008 12 noon, Research Beehive - Room 2.20
How to solve hard problems using SAT based techniques
Victor Khomenko: In this tutorial I will give a brief introduction into Boolean Satisfiability (SAT): the problem itself, techniques of its solving, ways of reducing other problems to SAT, and some applications.
October 31, 2008 1pm, Merz Court M413
Cyclic combinational circuits
Andrey Mokhov: A collection of logic gates forms a combinational circuit if the outputs can be described as Boolean functions of the current input values. Optimizing combinational circuitry, for instance, by reducing the number of gates (the area) or by reducing the length of the signal paths (the delay), is an overriding concern in the design of integrated circuits. The accepted wisdom is that combinational circuits must have acyclic (i.e., loop-free or feed-forward) topologies. In fact, the idea that "combinational" and "acyclic" are synonymous terms is so thoroughly ingrained that many textbooks provide the latter as a definition of the former. And yet simple examples suggest that this is incorrect. In this presentation, we advocate the design of cyclic combinational circuits (i.e., circuits with loops or feedback paths). We demonstrate that circuits can be optimized effectively for area and for delay by introducing cycles.
September 11, 2008 1pm, Room 3.02, Marz Court
Ready Simulation -- It's Logical!
Walter Vogler: In practice, software engineers typically mix imperative language constructs with declarative contracts (assume/guarantee-reasoning). This way, one can simultaneously prescribe an operational architecture as well as logically specify the components and requirements for the overall system; also, the step-wise transformation of logical specifications to operational system descriptions is supported. The aim of our project is to develop a specification language for concurrent systems where operators from process algebra and temporal logics can be mixed freely. The respective refinement (i.e. implementation) relation should * support compositional reasoning * find a place in the well-known spectrum for concurrency semantics when restricted to processes * correspond to implication when restricted to logical formulae, and * express that a process satisfies a formula. We have generalised labelled transition systems (LTS) in a suitable way to Logic LTS and defined several operators on these. Starting from a very simple basic relation, we have shown that what we call ready tree semantics is exactly adequate for treating conjunction. The respective preorder has to be refined to ready simulation preorder when we also consider parallel composition; this preorder indeed satisfies the requirements listed above.
August 4, 2008 11am, Room M5.02, Merz Court
Virtual Thermal Management: An Alternative to Dynamic Voltage and Frequency Scaling
Sandip Kundu: The sustained push for performance, transistor count and instruction level parallelism has reached a point where IC thermal issues are at the forefront of design constraints. Many of the current systems deploy dynamic voltage and frequency scaling (DVFS) to address thermal emergencies. DVFS has certain limitations in terms of response lag, scalability, and being reactive. On the other hand, several hardware based control theoretic schemes have been proposed to deliver optimal performance, but such schemes come at high cost and lack flexibility and scalability. In this talk, we present an alternative thermal monitoring and management system that utilizes software and hardware components, based on virtual machine concept. The proposed scheme delivers flexible thermal management at low cost, adapts well to a multitasking environment, while delivering maximum performance under thermal stress. The results show that in 65nm technology, the targeted, localized, and preemptive response improves the system performance by an average of 45% over conventional Dynamic Voltage and Frequency Scaling (DVFS).
July 25, 2008 2pm, M502, Merz Court
Checking pi-Calculus Structural Congruence is Graph Isomorphism Complete
Victor Khomenko: We show that the problems of checking pi-Calculus structural congruence (piSC) and graph isomorphism (GI) are Karp reducible to each other. The reduction from GI to piSC is given explicitly, and the reduction in the opposite direction proceeds by transforming piSC into an instance of the term equality problem (i.e. the problem of deciding equivalence of two terms in the presence of associative and/or commutative operations and commutative variable-binding quantifiers), which is known to be Karp reducible to GI. Our result is robust in the sense that it holds for several variants of structural congruence and some rather restrictive fragments of pi-Calculus. Furthermore, we address the question of solving piSC in practice, and describe a number of optimisations exploiting specific features of pi-Calculus terms, which allow one to significantly reduce the size of the resulting graphs that have to be checked for isomorphism. Link to the technical report: http://www.cs.ncl.ac.uk/publications/trs/abstract/1100
April 28, 2008 11am, Merz Court, Room M502
Diagnosability verification with Petri net unfoldings
Agnes Madalinski: Diagnosability is an important property that determines the ability of a system to detect failures occurrences given only observable sequences (the system has observable events and unobservable events including failures). If a system is diagnosable the diagnosis will find an accurate explanation for any possible set of observations from the system, otherwise the diagnosis will give an ambiguous and useless explanation. The seminal work of Sampath et al. has introduced a formal language framework for diagnosis and analysis of diagnosability properties of discrete event systems. The complexity of the algorithm for verification of diagnosability is exponential in the number of states of the system and doubly exponential in the number of failure types. Jiang et al. proposed an improvement, which resulted in the twin plant method. The basic idea is to build a verifier from a diagnoser, which is constructed from a finite state model of the system. The verifier compares every pair of paths in the system that have the same observable behaviour. It is obtained by the synchronous product of the diagnoser with itself on observable events. Naturally, the state-based twin plant method suffers from the state space explosion problem. In order to elevate this problem Petri net unfoldings are applied to it. The finite and complete prefixes of Petri net unfoldins provides an efficient and compact representation of all behaviours of the Petri net in partial order semantics. Executions are considered as partial ordered set of events rather than sequences. Two algorithms are proposed to test diagnosability; one performs an exhaustive search and reports in the case the system is not diagnosable all ambiguous explanations, and the other is designed to stop at the first ambiguous explanation if it exists and simply report the result, i.e. if the system is diagnosable or not. Moreover, some improvements for both algorithms are presented.
March 28, 2008 11am, Research Beehive, room 2.20
Automated verification of asynchronous circuits using circuit Petri nets
Ivan Poliakov: To detect problematic circuit behavior such as potential hazards and deadlocks in a reasonable amount of time a technique is required which would avoid exhaustive exploration of the state space of the system. Unlike the currently employed verification methods that are generally based on binary decision diagrams (BDDs), this talk presents an alternative approach of using a special type of Petri nets to represent circuits. Once a Petri net is constructed (an algorithm for automatic conversion of a circuit netlist into a behaviourally equivalent Petri net is proposed) and composed with the provided environment specification, the presence and reachability of troublesome states can be verified by using methods based on unfoldings. The Petri net verification results are then mapped back onto a gate-level representation. Experimental results for a tool based on this method and comparison with previously available tools are also presented.
March 27, 2008 11am, Merz Court, Room M502
Conditional Partial Order Graphs and Dynamically Reconfigurable Control Synthesis
Andrey Mokhov: The talk introduces a new formal model for specifying control paths in the context of asynchronous system design. The model, called Conditional Partial Order Graph (CPOG), is capable of capturing concurrency and choice in a system's behaviour in a compact and efficient way. A problem of CPOG synthesis is formulated and solved; various CPOG optimisation techniques are presented. The introduced model can be used for the specification of system behaviour and for synthesis of area-efficient dynamically reconfigurable controllers. The synthesis of a controller is based on a novel generic architecture, called Transition Sequence Encoder (TSE). The synthesized controllers are speed independent and thus very robust to parametric variations. The ideas presented in the talk can be applied for CPU control synthesis as well as for synthesis of different kinds of event-coordination circuits often used in data coding and communication in digital systems.
January 25, 2008 1pm, Room M502 (Merz Court - former Maths part)
Logic Decomposition of Asynchronous Circuits Using STG Unfoldings
Victor Khomenko: In this paper, a technique for logic decomposition of asynchronous circuits which works on STG unfolding prefixes rather than state graphs is proposed. It retains all the advantages of the state space based approach, such as the possibility of multiway acknowledgement, latch utilisation and highly optimised circuits. Moreover, it significantly alleviates the state space explosion, and thus has superior memory consumption and runtime, and is able to synthesise much larger specifications.
December 14, 2007 10am, Room 2.21 Research Beehive
The theory of gene assembly: contributions to theoretical computer science
Grzegorz Rozenberg: Natural Computing is a dynamic and fast growing research area concerned with computing taking place in nature and with human-designed computing inspired by nature. A popular and important topic in the former line of research is computation in living cells, and a good example of this research is the investigation of gene assembly in ciliates. Ciliates, a very ancient group of unicellular organisms, have evolved extraordinary ways of organizing, manipulating and replicating the DNA in their micronuclear genomes. The way that ciliates transform genes from their micronuclear (storage) form into their macronuclear (expression) form is the most involved DNA processing in nature that is known to us. This gene assembly process is also very interesting from the computational point of view. Current research concerning gene assembly is an example of flourishing interdisciplinary research involving computer scientists and molecular biologists. The results obtained thus far are interesting and beneficial for both molecular biology and computer science. One of the central research issues is the quest for discovery of "molecular hardware" needed for the implementation (in vivo) of molecular operations accomplishing gene assembly. This quest will be the topic of our lectures. In the first lecture we will discuss the biology of gene assembly and demonstrate a solution to the molecular hardware problem - it is based on the template-guided recombination. This recombination is very different from the standard homologous recombination of DNA strands, but it has the properties that are necessary to ensure the DNA acrobatics required for the implementation of the gene assembly process. In the second lecture we present a mathematical theory based on the template-guided recombination. Surprisingly enough this theory turns out to be quite fundamental for theoretical computer science. The lectures are organized in such a way that they can be followed independently of each other. However the two lectures together provide an example of a "complete package" of interdisciplinary research: (1) An important problem from biology is explained and a solution for it is presented, (2) A formal theory instigated by the solution turns out to be relevant for theoretical computer science, (3) The implications of the formal theory provide relevant guidelines for the research on the original biological problem. The lectures are of a tutorial character and self-contained. In particular, no knowledge of basic molecular biology is required.
December 13, 2007 10am, Room 2.20 Research Beehive
The biology of gene assembly: the quest for discovery of biological hardware (bioware) in vivo
Grzegorz Rozenberg: Natural Computing is a dynamic and fast growing research area concerned with computing taking place in nature and with human-designed computing inspired by nature. A popular and important topic in the former line of research is computation in living cells, and a good example of this research is the investigation of gene assembly in ciliates. Ciliates, a very ancient group of unicellular organisms, have evolved extraordinary ways of organizing, manipulating and replicating the DNA in their micronuclear genomes. The way that ciliates transform genes from their micronuclear (storage) form into their macronuclear (expression) form is the most involved DNA processing in nature that is known to us. This gene assembly process is also very interesting from the computational point of view. Current research concerning gene assembly is an example of flourishing interdisciplinary research involving computer scientists and molecular biologists. The results obtained thus far are interesting and beneficial for both molecular biology and computer science. One of the central research issues is the quest for discovery of "molecular hardware" needed for the implementation (in vivo) of molecular operations accomplishing gene assembly. This quest will be the topic of our lectures. In the first lecture we will discuss the biology of gene assembly and demonstrate a solution to the molecular hardware problem - it is based on the template-guided recombination. This recombination is very different from the standard homologous recombination of DNA strands, but it has the properties that are necessary to ensure the DNA acrobatics required for the implementation of the gene assembly process. In the second lecture we present a mathematical theory based on the template-guided recombination. Surprisingly enough this theory turns out to be quite fundamental for theoretical computer science. The lectures are organized in such a way that they can be followed independently of each other. However the two lectures together provide an example of a "complete package" of interdisciplinary research: (1) An important problem from biology is explained and a solution for it is presented, (2) A formal theory instigated by the solution turns out to be relevant for theoretical computer science, (3) The implications of the formal theory provide relevant guidelines for the research on the original biological problem. The lectures are of a tutorial character and self-contained. In particular, no knowledge of basic molecular biology is required.
December 4, 2007 10am, Research Beehive, Room 2.22
Communication Centric Computer Design
Simon Moore: We are at a pivotal point in the design of computational devices. Technology scaling favours transistors over wires which has led us into an era where communication takes more time and consumes more power than the computation itself. We believe that this technology driver inextricably pushes us toward a communication-centric approach to computer system design from both hardware and software perspectives. Our work is focused on exploring this new communication-centric view of computer system design from engineering wires through computer architecture, compiler design, language design and application mapping.
November 14, 2007 4pm, Room M502 (Merz Court - former Maths part)
A Petri Net semantics for pi-calculus Verification
Roland Meyer: Automata-theoretic representations have proven useful in the automatic and exact analysis of computing systems. We propose a new semantical mapping of Pi-Calculus processes into place/transition Petri nets. Our translation exploits the connections created by restricted names; it yields finite nets for processes with unbounded name and unbounded process creation. For finite Petri nets, well-investigated verification techniques are available. The property of structural stationarity characterises the processes mapped to finite nets. We provide exact conditions for structural stationarity using the novel characteristic functions of depth and breadth. Referring to the standard interpretation of processes as hypergraphs, we prove that boundedness in depth and in breadth corresponds to boundedness in the length of the simple paths and boundedness of the hyperedge degrees, respectively. This gives an intuitive understanding of structurally stationary processes. For modelling client-server architectures like the car platooning case study, we design the syntactic class of finite handler processes. Applying our theory, we prove that finite handler processes are structurally stationary. Our Petri net translation facilitates the automatic verification of the car platooning system. We infer occurrence number, temporal, and topological properties using efficient algorithms that exploit the graph structure of the Petri net. Traditional Petri net constructions for process calculi focus on the concurrency of sequential processes. When comparing these translations with our new semantics, we observe that both finitely represent different classes of processes. We work out a combination of the translations that unifies and extends the two classes. At present, this gives the most expressive class of Pi-Calculus processes that have a finite Petri net representation. To argue that our semantics is useful for verification, we discuss the aspects we believe constitute a useful semantics: retrievability, finiteness and expressiveness, analysability, and compositionality.
November 5, 2007 11am, Room M502 (Merz Court - former Maths part)
Data driven modeling of multistage interconnection networks by compositional high level Petri nets
Elisabeth Pelz: Systems on chip and multicore processors have emerged in the last few years. The required networks on chips can be realized by multistage interconnection networks (MIN). Prior to technical realizations, establishing and investigating formal models helps to choose best adequate MIN architectures. This talk presents a Petri net semantics for modeling such MINs in case of multicast traffic. The new semantics is inspired by high-level versions of the Petri box algebra providing a method to formally represent concurrent communication systems in a fully compositional way. In our approach, a dedicated net class is formed, which leads to three kinds of basic nets describing: a switching element, a packet generator, and a packet flush. With these basic nets, models of MINs of arbitrary crossbar size can be established compositionally following their inductive definition. Particular token generation within these high-level nets, as for instance, random load, yields an alternative approach to the use of stochastic Petri nets when compared with previous studies. The simulation of the models under step semantics provides a basis for performance evaluation and comparison of various MIN architectures and their usability for networks on chips. Particularly, multicast traffic patterns, which are important for multicore processors, can be handled by the new model.
October 26, 2007 4pm, BEDTC.L.G.35
Asynchronous Links for Networks on Chip - Part 2
Alex Yakovlev: Nanometer technology facilitates integration of massive functionalities on a single chip, allowing designers to build multi-processor systems-on-chip. According to industrial estimates, at a very deep submicron level "total interconnect length can reach several meters, with interconnect delay as much as 90% of total path delay, and parasitics from interconnect becoming a dominant factor, which often causes timing issue in chip design" (from J.Lin's Tutorial at ISSS 2003). There is a gradual realization that inter-block communication interfaces and links are becoming the first victims in the current standard system design methodology, which is based on global clocking. Clock skew becomes a problem for long interconnects, which limits the operating frequency in the channel. Thus maintaining high bandwidth under fully synchronous mode appears to be possible only by increasing the number of wires, wire width and inter-wire spacing (to reduce crosstalk), which is unrealistic because the metal layer area is at a premium on billion transistor chips. Globally clocked interconnect also suffers from the increased power and EMC problems. All this leads to thinking that future links are going to be increasingly self-timed. ITRS'05 predicts 4x increase in global asynchronous signalling by 2012 (8x by 2020). This talk will focus on some key aspects involved in designing asynchronous links for on-chip communication, starting from the physical level, such as level, transition and pulse-based signalling, delay-insensitive data encoding, handshake protocols, control logic for synchronization buffers. It will then move to the link level circuits, such as FIFO buffers, address decoders and simple routers, paying particular attention to design of arbiters (tree, token-ring, priority etc.). Besides looking at purely asynchronous interfaces, the talk will also discuss async-to-sync links which are meant to be used at links between globally asynchronous channels and locally synchronous processing cores, in order to facilitate SoC desynchronization and construction of GALS systems. Here, problems with designing robust synchronizers will be addressed. The talk will also briefly look at successful examples of self-timed interconnects such as CHAIN, commercialised by Silistix.
October 19, 2007 4pm, Room M502 (Merz Court - former Maths part)
Asynchronous Links for Networks on Chip - Part 1
Alex Yakovlev: Nanometer technology facilitates integration of massive functionalities on a single chip, allowing designers to build multi-processor systems-on-chip. According to industrial estimates, at a very deep submicron level "total interconnect length can reach several meters, with interconnect delay as much as 90% of total path delay, and parasitics from interconnect becoming a dominant factor, which often causes timing issue in chip design" (from J.Lin's Tutorial at ISSS 2003). There is a gradual realization that inter-block communication interfaces and links are becoming the first victims in the current standard system design methodology, which is based on global clocking. Clock skew becomes a problem for long interconnects, which limits the operating frequency in the channel. Thus maintaining high bandwidth under fully synchronous mode appears to be possible only by increasing the number of wires, wire width and inter-wire spacing (to reduce crosstalk), which is unrealistic because the metal layer area is at a premium on billion transistor chips. Globally clocked interconnect also suffers from the increased power and EMC problems. All this leads to thinking that future links are going to be increasingly self-timed. ITRS'05 predicts 4x increase in global asynchronous signalling by 2012 (8x by 2020). This talk will focus on some key aspects involved in designing asynchronous links for on-chip communication, starting from the physical level, such as level, transition and pulse-based signalling, delay-insensitive data encoding, handshake protocols, control logic for synchronization buffers. It will then move to the link level circuits, such as FIFO buffers, address decoders and simple routers, paying particular attention to design of arbiters (tree, token-ring, priority etc.). Besides looking at purely asynchronous interfaces, the talk will also discuss async-to-sync links which are meant to be used at links between globally asynchronous channels and locally synchronous processing cores, in order to facilitate SoC desynchronization and construction of GALS systems. Here, problems with designing robust synchronizers will be addressed. The talk will also briefly look at successful examples of self-timed interconnects such as CHAIN, commercialised by Silistix.
September 14, 2007 2.30pm, Room: Research Beehive, Room 2.22
Grand Challenges in Microelectronic Design
Steve Furber: The UK microelectronics design research community has been working towards a 'Common Vision' of where the exciting research opportunities lie over the next ten to twenty years. This has culminated in the identification of four Grand Challenges that provide a focus for future research. In this seminar I will describe the process that has led to these Grand Challenges, what they are, and how the community can engage in them and in the process of refining and developing them in the future.
August 29, 2007 2pm, Room 701, CLT
Modelling agent systems with combination of behavioral and state-based approaches
Alexei Iliasov: The talk will present results of the ongoing work on modelling and verification of agent systems. The work aims at combining process algebraic and state-based models in a single development using the refinement technique. Behavioral modelling is a natural choice for high-level modelling of parallel and distributed systems. Behavioral specifications focus on modelling temporal or causal ordering of events, omitting details of state evolution. A behavioral description, however, lacks the level of precision attainable with the state-based approach. Behavioral specifications are invariably abstract. On the other hand, modelling of behaviour in the state-based approach is difficult. Agent systems is a typical example of the systems for which behavioral model is preferable for a high-level system abstraction but a state-based description is required to formulate practical models. The presented method attempts to combine behavioral and state-based modelling in a single development using the refinement technique. An abstract system model is specified using a process algebra which is gradually transformed into a state-based description with the equivalent observable behaviour. The talk will present an outline of a tool for computer-aided development of agent systems. Such tool would combine simplicity of visual modelling tools such as UML, the expressive power of specifications languages such as B and Z and systematic step-wise development of the refinement.
May 25, 2007 1pm, E4, Basement, Merz Court, School of EEC
Combining Decomposition and Unfolding for STG Synthesis
Victor Khomenko: For synthesising efficient asynchronous circuits one has to deal with the state space explosion problem. In this talk, I will present a combined approach to alleviate it, based on using Petri net unfoldings and decomposition. The experimental results show significant improvement in terms of runtime compared with other existing methods.
May 11, 2007 1pm, E4, Basement, Merz Court, School of EECE
Conditional Partial Order Graphs and Dynamically Reconfigurable Control Synthesis
Andrey Mokhov: A new formal model for specifying control paths in the context of asynchronous system design is introduced. The model, called Conditional Partial Order Graph (CPOG), is capable of capturing concurrency and choice in a system's behaviour in a compact and efficient way. The presented model can be used for the specification of system behaviour and for synthesis of area-efficient dynamically reconfigurable controllers. The synthesis of a controller is based on a novel generic architecture, called Transition Sequence Encoder (TSE). The synthesized controllers are delay insensitive and thus very robust to parametric variations. The presented ideas can be applied for CPU control synthesis as well as for synthesis of different kinds of event-coordination circuits often used in data coding and communication in digital systems.
April 27, 2007 1pm, E4, Basement, Merz Court, School of EEC
Distributed complete prefix construction
Agnes Madalinski: The modular construction of finite and complete prefixes applied to distributed systems, which are modelled by Petri nets in form of synchronous products of automata, is presented. A distributed system is described as a collection of components interacting through interfaces. They exhibit factorisation properties, viz. the unfolding of a distributed system factorises as the product of unfoldings of its components. This gives a compact representation and makes it possible to analise the system by parts. The construction of modular prefixes is based on deriving 'summaries' of components w.r.t. their interfaces whilst passing them on the interaction structure of system via interfaces. Prefixes of components are then derived locally by taking into account the summaries received on their interfaces.
February 16, 2007 1pm, E4, Basement, Merz Court, School of EEC
A High Resolution Flash Time-to-Digital Converter Taking Into Account Process Variability
Nikolaos Minas: Timing issues are a major concern in the design of high performance synchronous, asynchronous circuits and GALS. Investigations into the causes of many timing problems cannot be satisfactorily undertaken using external equipment due to its remoteness from the source of the potential problem; this necessitates the development of on-chip time measurement circuitry. Current techniques have the capability of resolving timing differences down to 5ps , however further improvement is impeded by process variations. This paper describes a flash Time to Digital Converter (TDC) suitable for on-chip implementation. The theory to overcome the effects of process variations, potentially permitting the time resolution down to one picosecond is described. Proof of concept is demonstrated by implementing the techniques in an FPGA, improving on the current resolution of FPGA implementation of a TDC.
February 2, 2007 1pm, E4, Basement, Merz Court, School of EEC
Efficient Automatic Resolution of Encoding Conflicts Using STG Unfoldings
Victor Khomenko: Synthesis of asynchronous circuits from Signal Transition Graphs (STGs) involves resolution of state encoding conflicts by means of refining the STG specification. In this paper, a fully automatic technique for resolving such conflicts by means of insertion of new signals is proposed. It is based on conflict cores, i.e. sets of transitions causing encoding conflicts, which are represented at the level of finite and complete prefixes of STG unfoldings, and a SAT solver is used to find where in the STG the transitions of new signals should be inserted. The experimental results show significant improvements over the state space based approach in terms of runtime and memory consumption, as well as some improvements in the quality of the resulting circuit.
January 26, 2007 1pm, E4, Basement, Merz Court, School of EEC
Modelling Intelligent Memory on a Dynamically Re-configurable System
Jun Xu: In the past 30 years, an exponential rate of improvement has been witnessed in semiconductor technology. The CPU performance increases at rate of 60% per year while the memory performance only increases 10% per year. This imbalance has caused a 50% of growing performance between the CPU and memory. The effort to improve computer performance and equip standard memories with processing power has emerged as an alternative solution. This is normally referred to logic-in-memory/Processor-In-Memory (PIM). In this talk, I will explain how to explore a self-learning and self-acting, truly intelligent PIM system, using dynamic reconfiguration, for the improvement of processor-memory performance.
December 1, 2006 1pm, E4, Basement, Merz Court, School of EEC
Transition Systems of Elementary Net Systems with Localities
Marta Pietkiewicz-Koutny: We investigate transition systems of a class of Petri nets suitable for the modelling and behavioural analysis of globally asynchronous locally synchronous systems. The considered model of Elementary Net Systems with Localities (ENL-systems) is basically that of Elementary Net Systems (EN-systems) equipped with an explicit notion of locality. Each locality identifies a distinct set of events which may only be executed synchronously, ie in a maximally concurrent manner. For this reason, the overall behaviour of an ENL-system cannot be represented by an interleaved transition system, with arcs being labelled by single events, but rather by a suitable notion of a step transition system, with arcs being labelled by sets of events executed concurrently. We completely characterise transition systems which can be generated by Elementary Net Systems with Localities under their mintended concurrency semantics. In developing a suitable characterisation, we follow the standard approach in which key relationships between a Petri net and its transition system are established via the regions of the latter defined as specific sets of states of the transition system. We argue that this definition is insufficient for the class of transition systems of ENL-systems, and then augment the standard notion of a region with some additional information, leading to the notion of a region with explicit input and output events (or io-region). We define, and show consistency of, two behaviour preserving translations between ENL-systems and their transition systems. As a result, we provide a solution to the synthesis problem of Elementary Net Systems with Localities, which consists in constructing an ENL-system for a given transition system in such a way that the transition system of the former is isomorphic to the latter.
November 24, 2006 1pm, E4, Basement, Merz Court, School of EEC
Comparative Analysis of GALS Clocking Schemes
Sohini Dasgupta: Due to the increase in complexity of distributing a global clock over a single die globally asynchronous and locally synchronous systems are becoming an efficient alternative technique to design distributed SoCs. Number of independently clocked synchronous domains can be integrated by clock pausing, clock stretching or data driven clock techniques. Such techniques are applied on point-to-point inter-domain communication schemes. We present here a comparison of these schemes and how it can be applied to an existing partitioned synchronous architecture to obtain a reliable, low latency and efficient clock control architectures. The comparison highlights the advantages and disadvantages of one scheme over the other in terms of logical correctness, circuit implementation, performance and relative power consumption. This talk also presents circuit solutions for stretchable and data driven clocking schemes. These circuit solutions can be easily plugged into existing partitioned synchronous islands. To enable early evaluation of functional correctness, this paper proposes the use of Petri net modeling technique to model the asynchronous control blocks that constitute the interface between the synchronous islands.
November 17, 2006 1pm, E4, Basement, Merz Court, School of EEC
Process Semantics of Membrane Systems
Maciej Koutny: Membrane systems are a computational model inspired by the way living cells are divided by membranes into compartments where chemical reactions may take place. They share a number of features with Globally Asynchronous Locally Synchronous systems (GALS). The talk will consider synchrony and asynchrony between executed reactions in the computations of such systems using Petri nets and their processes as a formal behavioural model. The non-sequential semantics of the resulting nets is formalised through processes based on occurrence nets. Such processes provide a convenient tool for analysing synchrony and asynchrony in the executions of membrane systems and shed light on the causal relationships between the reactions taking place.
November 3, 2006 1pm, E4, Basement, Merz Court, School of EEC
Verification with Bounded Model Checking
Keijo Heljanko: Model checking is a set of methods for analysing whether a model of a system (e.g., a Petri net) fulfils its specification given as a temporal logic formula. Bounded model checking (BMC) was introduced by Biere et. al to further improve the scalability of model checking by applying methods based on propositional satisfiability (SAT). In bounded model checking only counterexample executions of the system that are shorter than some fixed length are considered. The success of BMC, especially in the context of hardware verification, is based on the enormous advances in SAT solving techniques achieved during the last few years. In this talk we focus is on topics which arise when creating an efficient bounded model checkers for an asynchronous system model (e.g., a 1-safe Petri net). This requires the use of efficient SAT encodings for the model checking problem at hand.
October 18, 2006 1pm, E4, Basement, Merz Court, School of EEC
Symbolic Unfoldings of Coloured Petri Nets
Thomas Chatain: Despite the use of true concurrency models, most of the techniques dedicated to the study of distributed systems suffer from the state space explosion problem due to the interleavings of concurrent actions. Unfoldings provide a solution to this problem. They are based on a causal semantics defined as an alternative to the sequential semantics. But although high-level extensions of Petri nets are commonly used to model real systems, the unfolding technique has not been much studied in the framework of high-level true concurrency models. Colored Petri nets are a classical extension of Petri nets and allow to model data aspects. Colored Petri nets can be "expanded" into low-level Petri nets, which allows to define the unfolding of a colored Petri net as the unfolding of its expansion. We propose a different approach, which is based on the symbolic representation of families of executions that share the same structure.
October 4, 2006 2pm, Room 2.29 Research Beehive
Guarding the Pass Between the Real World and the Digital World
David Kinniment: Any system that has to interact with other, independent, sources of data needs to know when incoming data has arrived in order to make sense of it. This may seem obvious, but it is not easy to do. It means that requests from an external time frame must be synchronized with the time frame of the receiving system, but unfortunately time is a continuous quantity, where the presence or absence of a request is digital. It's either there, or it isn't. This is a fundamental problem in which a continuous variable (time) has to be mapped to a discrete variable (request). Synchronizers and arbiters are the circuits that attempt, imperfectly, to do the job, and the more systems there are that have to interact, the better we need to understand their imperfections and the resulting unreliability. This seminar will deal with measuring the performance of real circuits, the trade-off between latency and reliability, and how decision making can be made more robust.
July 7, 2006 2pm, Room 2.20 Research Beehive
A Chip Multiprocessor for Large-Scale Neural Simulation
Steve Furber: The real-time modelling of large systems of spiking neurons is computationally very demanding in terms of processing power, synaptic weight memory requirements and communication throughput. We propose to build a high-performance computer for this purpose with a multicast communications infrastructure inspired by neurobiology. The core component will be a chip multiprocessor incorporating some tens of small embedded processors, interconnected by an NoC that carries spike events between processors on the same or different chips. The design emphasizes modelling flexibility, power-efficiency, and fault-tolerance, and is intended to yield a general-purpose platform for the real-time simulation of large-scale spiking neural systems.
June 14, 2006 3.30pm, Research Beehive, Room 2.20
Lossy Synthesis - a New Paradigm for Hardware Synthesis of DSP Systems
Peter Cheung: With the availability of low cost, high gate-count FPGAs, it is now possible to map complex DSP algorithms onto hardware with ease and at a low cost. Traditional synthesis methods require an exact description of the system hardware, usually at RTL level. Synthesis tools are then employed to generate optimised designs which performance exactly as the description. Lossy synthesis is an approach whereby the circuit synthesized is allowed to have errors, hence providing an additional trade-off between area, performance, power and accuracy. To demonstrate the lossy synthesis approach, recent results from two research projects carried out in our research group will be described. The first project is to optimally synthesis any sets of 2D non separable filters using heterogenous FPGAs (i.e. FPGAs that contains lookuptables, multipliers and RAMs). Based on the SVD algorithm, our synthesis method produces hardware mapping that is significantly smaller than existing methods. The second project is about computation using a new number representation known as Dual FiXed-point (DFX), which has the advantage of hardware simplicity of fixed point arithmetic and the improved dynamic range of a floating-point representation. New results on error modeling, circuit complexity and application examples will be presented.
June 9, 2006 1pm, E4, Basement, Merz Court, School of EEC
Use of Petri-net in modelling and simulation of biological networks
Tiak Wan Ng: I shall elaborate first on how to model and simulate Biological networks, begin with some historical review of initial attempts based on electrical circuit design, and later from Chemical Kinetics approach. Both Deterministic and stochastic approach can eventually be represented and explored in more detail using the Petri-net analysis. Simple biological networks will be used to illustrate how this can be done. Discussion will be focused on the potential use of Petri-net in modelling and simulation of Biological networks.
June 2, 2006 1pm, E4, Basement, Merz Court, School of EEC
Modelling and Analysing Genetic Networks: From Boolean Networks to Petri Nets
Jason Steggles: In order to understand complex genetic regulatory networks researchers require automated formal modelling techniques that provide appropriate analysis tools. In this talk we propose a new qualitative model for genetic regulatory networks based on Petri nets and detail a process for automatically constructing these models using logic minimization. We take as our starting point the Boolean network approach in which regulatory entities are viewed abstractly as binary switches. The idea is to extract terms representing a Boolean network using logic minimization and to then directly translate these terms into appropriate Petri net control structures. The resulting compact Petri net model addresses a number of shortcomings associated with Boolean networks and is particularly suited to analysis using the wide range of Petri net tools. We demonstrate our approach by presenting a case study in which the genetic regulatory network underlying the nutritional stress response in Escherichia coli is modelled and analysed. The above talk is based on a Technical Report available at: http://www.cs.ncl.ac.uk/research/pubs/trs/abstract.php?number=962
May 31, 2006 1pm, E4, Basement, Merz Court, School of EEC
On-chip timing releationship regeneration
Crescenzo DAlessandro: A major issue in the design of circuit design is the requirement to preserve timing relationships between paths. This is important when parallel paths are involved for the transmission of data over a long communication channel; in this case effects such as cross-talk can reduce the delay relationship between two wires, so that the system could fail even though the design is correct in the sense that the timing closure requirement is satisfied. In particular, in the context of phase-encoding, which is the main driver for the work, the timing relationship is all-important to ensure reliable data recovery. This work discusses some methods that can be used to restore the timing relationship so it is preserved between the sender and the receiver, showing examples of design and the design procedure involved.
May 19, 2006 1pm, E4 Merz Court
Completion Detection Optimisation based on Relative Timing
Andrey Mokhov: This paper presents an algorithm for efficient distribution of completion detection blocks in a dual-rail self-timed circuit to ensure correct computation of the completion signal. Layer-wise optimisation technique is used with the width of layers selected so as to satisfy timing constraints and use the least possible number of completion detection blocks. The presented algorithm is implemented in a tool for asynchronous design flow.
May 12, 2006 1pm, E4, Basement, Merz Court, School of EEC
Area and performance optimization of partially acknowledged asynchronous circuits
Yu Zhou: We introduce a design method of asynchronous circuits based on the concept of partial acknowledgement. The method keeps the interconnections of a synchronous Boolean network but maps its gate elements to certain function modules using dual-rail code. We assure that each input and internal variable is partial acknowledged so that the isochronic assumption is satisfied. Furthermore, we explore the possible distributions of partial acknowledgement towards optimal area and performance of the final implementation.
April 28, 2006 1pm, E4, Basement, Merz Court, School of EECE
Behaviour-Preserving Transition Insertions in Unfolding Prefixes
Victor Khomenko: Some design methods based on Petri nets modify the original specification by behaviour-preserving insertion of new transitions. If the unfolding prefix is used to analyse the net, it has to be re-unfolded after each modification, which is detrimental for the overall performance. The approach presented in this paper applies the transformations directly to the unfolding prefix, thus avoiding re-unfolding. This also helps in visualisation, since the application of a transformation directly to the prefix changes it in a way that was 'intuitively expected' by the user, while re-unfolding can dramatically change the shape of the prefix. Moreover, rigourous validity checks for several kinds of transition insertions are developed. These checks are performed on the original unfolding prefix, so one never has to backtrack due to the choice of a transformation which does not preserve the behaviour.
March 3, 2006 1pm, E4, Basement, Merz Court, School of EECE
Recent Developments in Pret a Voter
Peter Y A Ryan: In this talk I will describe some of the latest developments of the Pret a Voter scheme. This scheme, derived from an earlier scheme due to Chaum, has the surprising property of voter-verifiability: voters can confirm that their vote is accurately included in the tally, whilst at the same time preserving secrecy of their vote. This is achieved with minimal dependence on components of the system by providing maximal transparency within the constraints of ballot secrecy. I will discuss some of the assumptions underlying dependability of the current scheme, and the associated vulnerabilities. I will then describe some enhancements: the use of ElGamal crypto primitives to enable re-encryption mixes and distributed creation of ballot forms. I will also describe some joint work with Michael Clarkson and Andy Myers (Cornell) on coercion-resistant adaptations of the original, supervised scheme to the remote voting context.
February 24, 2006 1pm, E4, Basement, Merz Court, School of EECE
Timing Analysis for Latency-Aware Design
Crescenzo DAlessandro: The issue of timing analysis has been of crucial importance to microelectronics designers since the early stages of digital IC design. Timing closure, clock distribution and synchronisation are well-recognised problems. The ways to tackle timing analysis depend on several factors, in particular the required accuracy of the results. Techniques such as Logical Effort (LE) have been used to minimise the delay of a path by sizing the transistors of the gates along the path in question; however LE, in its simplest form, does not provide an accurate estimation of the absolute path delay, making it unusable to compare and synchronise different paths to a high level of reliability. The talk will first introduce some examples of design where the timing characterisation is important. It will then proceed to discuss the use of LE in these cases and the potential developments of this method, as compared to Static Timing Analysis techniques.
February 17, 2006 1pm, E4, Basement, Merz Court, School of EECE
Enhancing Signature-based Collaborative Spam Detection
Jeff Yan: Spam (junk email) is everywhere, annoying almost each email user and eroding their productivity. To date, statistical spam filters are probably the most heavily studied, and most widely adopted spam detection technology. However, among other disadvantages, they fail to detect spam that cannot be predicated by machine learning algorithms on which they are based. Neither they identify spam that is sent in an image format. In addition, these filters need to be regularly trained, particularly when false positive occurs. Signature-based collaborative spam detection (SCSD) seems to provide a promising solution addressing all the problems given above. What is especially attractive is that it can provide a reasonalbe solution to detect unforeseeable new spam, which intuitively appears to be mission impossible. However, SCSD approaches usually rely on huge databases of email signatures (or checksums), demanding lots of resource in signature lookup as well as signature database storage, transmission and merging. In this talk, I report our enhancements to two representative SCSD systems, Razor and DCC. In our enhancements, signature lookups can be performed in O(1), i.e. constant time, independent of the number of signatures in the database. Space-efficient representation can reduce signature dababase size by a factor of 25.6 or more for Razor-style systems before any data compression algorithm is applied. A simple but efficient algorithm for merging different signature databases is also supported. In the spirit of encouraging collaborative research, ongoing work and quite a few interesting open problems will also be discussed in this talk.
February 3, 2006 10am, E4, Basement, Merz Court, School of EECE
Variability-Tolerant Architectures
Satya Kiran Munaga: The talk addresses the impact of the increased parametric variability in deep submicron technologies upon the design process for SiP/Soc, and surveys variability-tolerant design approaches including self-timed design. Speaker address: IMEC, Leuven, Belgium
December 9, 2005 1pm, E4, Basement, Merz Court, School of EECE
An Introduction to Computational Complexity
Victor Khomenko: This talk is intended as a very basic introduction into the subject of computational complexity. Issues such as P vs. NP problem, or, say, that sorting can be done in O(n log n) worst case time, will be discussed.
December 2, 2005 1pm, Room 2.22 Beehive
Petri net unfoldings
Maciej Koutny: This talk will introduce and discuss the basic concepts ideas behind unfoldings of Petri nets, their finite prefixes, and verification techniques which are based on finite prefixes of net unfoldings.
November 30, 2005 9am-11am, L302, Merz Court
An Overview of Wireless LAN Standards
Anthony C Davies: Plan of the talk: Motives for WLAN development: mobility, cable-replacement. Standards: IEEE 802 standards, ETSI standards. The ISM frequency bands. Transmission methods (PHY layer). Frequency-hopping, Direct Sequence Spread Spectrum, Orthogonal Frequency Division Multiplex. Bluetooth, Wi-Fi, Hiperlan, Zigbee. Future trends: UWB, WiMax. Bluetooth Network formation and structures. WLAN security. Implementation issues. Contact details: Prof. Anthony C Davies Visiting Professor, Kingston University Emeritus Professor, Kings College London e-mail: tonydavies@ieee.org
November 18, 2005 1pm, E4, Basement, Merz Court, School of EECE
Derivation of Set and Reset Covers for gC Elements and Standard C Implementation Using STG Unfoldings
Victor Khomenko: The behaviour of asynchronous circuits is often described by Signal Transition Graphs (STGs), which are Petri nets whose transitions are interpreted as rising and falling edges of signals. One of the crucial problems in the synthesis of such circuits is deriving the set and reset covers for the state-holding elements implementing each output signal of the circuit. The derived covers must satisfy certain correctness constraints, in particular the Monotonic Cover condition must hold for the standard C implementation. The covers are usually derived using state graphs. In this paper, we avoid constructing the state graph of an STG, which can lead to state space explosion, and instead use only the information about causality and structural conflicts between the events involved in a finite and complete prefix of its unfolding. We propose an efficient algorithm for deriving the set and reset covers of gC elements and standard C implementation based on the Incremental Boolean Satisfiability (SAT) approach. Experimental results show that this technique leads not only to huge memory savings when compared with the methods based on state graphs, but also to significant speedups in many cases, without affecting the quality of the solution.
November 8, 2005 11am, E4, Basement, Merz Court, School of EECE
New Methods for STG Decomposition
Mark Schaefer: STGs are a well-known formalism for the modelling of asynchronous circuits. However, their synthesis can be rather inefficient. STG decomposition tries to reduce this complexity by splitting an STG into several components which are synthesised seperately. In this talk one approach to decomposition is introduced and justified. Furthermore some improvements of this decomposition method are discussed.
November 4, 2005 1pm, E4, Basement, Merz Court, School of EECE
Trellis Processes : a Tool for Distributed System Monitoring
Eric Fabre: The trajectory set of a discrete event system is usually represented as a trellis, where one dimension is time, and the other dimension represents possible states at each time. This structure underlies most algorithms for state estimation, optimal control, or dynamic programming procedures in general. However when moving to large networked systems, this trellis structure rapidly leads to intractable methods. By networked system, we mean a modular system obtained by connecting elementary components into a "network" or graph of components, where the edges represent possible interactions. Such systems suffer from two combinatorial explosions: in the number of possible states, and in the number of possible trajectories, due to the concurrency of events (the fact that several events can occur in parallel). In this talk, we present a strategy to deal with such distributed systems, based on three main ideas. First of all, we propose a representation of trajectories in the so-called "true concurrency semantics." This semantics replaces sequences of events by partial orders of events, thus preserving only causality relations instead of an explosive number of meaningless interleavings. Secondly, we propose a notion of trellis to represent all runs of a system in this semantics. We thus obtain "Trellis Processes," which are an avatar of "Merged Processes." Finally, for a networked system, we prove that the trellis of the global system can be expressed as the product (in a particular sense) of the trellises its components. This property is algebraically equivalent to the factorization property of the probability distribution in a Markov random field (or Bayesian network). This opens the way to distributed processings, operating at the scale of a single component, that take advantage of well known belief propagation/turbo algorithms. We illustrate these ideas on a simple distributed "diagnosis" problem. Short Bio: Eric Fabre is a Research Scientist at INRIA Rennes (IRISA), France. His research interests include distributed algorithms for distributed system monitoring, but also (probabilistic) graphical models of interactions and their applications in telecommunications. The work presented in this seminar is supported by a contract with Alcatel, dedicated to distributed failure diagnosis in telecommunication networks.
October 31, 2005 11am, Beehive: Room 2.21
Complex Electronics
Bashir M. Al-Hashimi: Hand-held computing and mobile communication devices continue to require embedded systems of increasing functionality, higher computational performance and reduced power consumption. Achieving such contradictory requirements need innovation in system level design methodologies. In the first part of my talk, I will review the primary concepts of some of the key energy management techniques with particular focus on dynamic voltage scaling (DVS) and then detail a new hardware/software co-design methodology for the synthesis of energy-efficient embedded systems. I will show through a case study of a smart phone how one can take advantage of the diversity of functions that embedded computing systems need to perform and their execution probabilities to reduce system energy consumption. A key feature of the electronics employed in hand-held devices is that it is complex in order to deliver the required functionality. In the second part of my talk, I will consider the impact of such complexity on the cost of manufacturing test and outline some techniques that are being developed at Southampton University aiming at reducing the cost of testing complex digital systems through the employment of compression methods. Furthermore, I will outline some design-for-test techniques that are compatible with low power design methods.
October 28, 2005 1pm, E4, Basement, Merz Court, School of EECE
Analysis and Verification of Object Oriented Systems
Swapan Bhattacharya: Software testing has gained immense importance in the present competitive world of developing software more quickly, more efficiently and more accurately. Testing activity is carried out throughout the lifecycle of software development and not only towards the end of development. Time and effort required to correct errors, detected later is much more compared to those, which are detected earlier. This has direct impact on costs and has led to a splurge of research activities in this domain. Our work has been mainly carried out in two domains - Verification of functional specifications of a system using a model based approach and verification and testing of software code for developing efficient and suitable test cases. Model-based testing has recently gained attention with the popularization of modeling itself. We have adopted Unified Modeling Language (UML) as the model for specifying the structural and behavioral aspects of an object oriented system. The UML is a visual model comprising of several diagrams which portray different yet overlapping views of the same system. Since translation of functional requirements into design models (UML) are mostly done manually, chances of inconsistencies are inevitable. We have developed an approach [1] to trace requirements into the UML diagrams constituting the design model so that any missing requirements would be traceable and ensure that the design is modeled as per the user specifications. Secondly another methodology [2] developed by us ensures that the related diagrams of the design model are coherent and consistent. Several rules have been proposed and an XML based approach is used for such verification. Thirdly we have developed an approach [3] for automated translation of one set of UML diagrams from a given set of diagrams. Automated derivation would definitely decrease chances of error and enable the development process to be more efficient and fast. Our second domain of work [4], [5], [6] focuses on verification and testing of code to ensure that it functions as expected. Code based testing more commonly known as white-box testing has several prevalent techniques. One very popular and widely used technique uses control flow graphs (CFG) to identify the various control paths in the software code and then develop adequate test cases to ensure execution of those paths. This technique however has some difficulties in being applied to object oriented systems. We have developed another graphical model called Extended Control Flow Graph (ECFG) to identify the control flow paths in an object oriented software and a new set of metrics called Extended Cyclomatic Complexity (E-CC) which gives an estimate of the minimum number of independent paths in the software that needs to be tested. A mechanism to derive test paths from the graph is also proposed. References [1] Ananya Kanjilal and Swapan Bhattacharya, "Verification of Requirements for ensuring Design Completeness in Object Oriented Systems", Accepted in ADCOM-2005, 13th International Conference on Advanced Computing and Communication, Coimbatore, December 14-17, 2005. [2] Ananya Kanjilal and Swapan Bhattacharya, "Design Verification of Object Oriented systems : XML-based Approach", accepted in SEKE 2005, 17th International Conference on Software Engineering and Knowledge Engineering, Taipei, Taiwan, July 14-16, 2005. [3] Sabnam Sengupta, Ananya Kanjilal, Swapan Bhattacharya, "Automated Translation of behavioral models using OCL and XML", Accepted in IEEE TENCON 2005, Melbourne, Australia, 21-24 Nov, 2005. [4] Ananya Kanjilal, Goutam Kanjilal, Swapan Bhattacharya, "Extended Control Flow Graph : An Engineering Approach" , Proceedings of CIT 03, Sixth International Conference on Information Technology, Bhubaneswar, India, December 22-25, 2003, page 151-156. [5] Swapan Bhattacharya, Ananya Kanjilal, "Static Analysis of Object Oriented systems using Extended Control Flow graph", Proceedings of IEEE TENCON 2004, Chiang Mai, Thailand, Nov 21-24, 2004, Vol-B, page B310-314. [6] Ananya Kanjilal, Swapan Bhattacharya, "Test Path Identification for Object Oriented systems using Extended Control Flow Graph", Proceedings of ADCOM-2004, 12th International Conference on Advanced Computing and Communication, Ahmedabad, India, December 15-18, 2004. Swapan Bhattacharya Dept. of Computer Science & Engg. Jadavpur University, Kolkata, India E-mail : bswapan2000@yahoo.co.in
October 21, 2005 1pm, E4, Basement, Merz Court, School of EECE
Automating the Process of Software Automation : Perspectives, Issues and Concerns
Swapan Bhattacharya: In spite of the phenomenal advancements in the arena of information and communication technology in recent times, success rates of software products are still quite poor. Many software projects fail to meet budgeted time and cost estimates, and some of them have to be abandoned even before completion. This alarming scenario concerning the process of software production can be attributed to the following factors : (i) inadequate domain knowledge of software developers, (ii) incomplete / imprecise perception of clients / end-users about functional requirements of software products vis-a-vis available technology, (iii) lack of stability of appropriate technology for deployment of reusable components, and (iv) excessive dependence of the process of production on the efficiency and capability of human beings involved in the process. All these issues of critical concern can be addressed through automation of the software production process. Technological tools are already available for automating later stages of production life cycle. Significant improvement in quality and efficiency of the production process can however be achieved only if automation can be deployed at the earlier stages and also for integration of subsequent stages of life cycle. Lack of precise and unambiguous statements on desired system requirements make development of formal models for earlier stages extremely difficult, which is turn makes the process of automation infeasible. A workable solution may be thought of through evolution of feasible and implementable formal models for domain-specific applications. The problems concerning automating the process of software production open up various challenging research issues in different dimensions. This particular session is aimed at deliberations leading to identification of these issues and appropriate methodologies with potential to address them, and also to evolve a platform for integration of various interrelated research perspectives. Speaker address: Department of Computer Science and Engineering Jadavpur University, Kolkata, India
October 14, 2005 1pm, E4, Basement, Merz Court, School of EECE
Modelling asynchronous circuits using Petri Nets
Alex Yakovlev: The talk will address the relationship between asynchronous circuits and concurrent systems and introduce the basic ideas of modelling asynchronous circuits with Petri nets. These modelling techniques could serve as a theoretical foundation to verification and synthesis of asynchronous circuits and systems.
July 19, 2005 9:30am - 12:30pm, Room 2.29, Research Beehive
The Role Method (tutorial)
Hugo Simpson: The role model method has been developed to support the correctness analysis of asynchronous communication mechanism (ACM) algorithms. The essence of the method is the use of functionally relevant abstractions to explore the full envelope of operation. This contrasts with the more traditional approach which commonly models physical implementation. The result is very much smaller models which nevertheless cover all interaction possibilities. A family of ACM connectors is presented before selecting a particular example for detailed role model analysis. Various modelling techniques are exposed by outline descriptions of the computer program logic required to implement them. It is shown that the role model method provides a powerful research tool which can be constructed without undue difficulty, and which provides insights to ACM operation not easily achieved by other means.
July 7, 2005 10 am, Room: E4, Merz Court
Galois Decomposition of Boolean Functions: An Efficient Synthesis Approach with Testability
Asutosh Singh: This talk presents a fast efficient graph-based decomposition technique for Boolean functions in finite fields, which utilizes the data structure of the Multiple-Output Decision Diagrams. The proposed technique is based on finite fields and can decompose any N valued arbitrary function F into N distinct sets conjunctively and N-1 distinct sets disjunctively. The proposed technique is capable of generating highly testable circuits. The experimental results show that the proposed method is more economical in terms of literal count compared to existing approaches.
May 3, 2005 1pm, Room E4 in the School of EECE
Merged Processes - a New Condensed Representation of Petri Net Behaviour
Maciej Koutny: Model checking based on Petri net unfoldings is an approach widely applied to cope with the state space explosion problem. In this talk we propose a new condensed representation of a Petri net's behaviour called merged processes, which copes well not only with concurrency, but also with other sources of state space explosion, \viz sequences of choices and non-safeness. Moreover, this representation is sufficiently similar to the traditional unfoldings, so that a large body of results developed for the latter can be re-used. Experimental results indicate that the proposed representation of a Petri net's behaviour alleviates the state space explosion problem to a significant degree and is suitable for model checking.
April 11, 2005 1pm, Merz Court
Energy Efficient Surfing
Mark Greenstreet: Surfing is a latchless pipelining technique where the propagation delays of gates and other logic functions are modulated to produce event attractors. We describe a test chip that demonstrates a surfing pipeline ring and then introduce new circuits that dramatically reduce the energy overhead for surfing. Our test chip implements a twelve-stage, surfing ring that supports two=0Aindependent waves of computation without latches or other storage elements. We have operated the chip for over 48 hours and more than 2.6*10^{15} surfing events without an error. However, the energy consumption of the ring is unacceptable for scaling to larger applications. Thus, we introduce a new family of surfing circuits that use less energy than their domino counterparts and provide a significant improvement by the E t^2 metric. We demonstrate this new family with the design of a carry lookahead adder. Keywords: Asynchronous design, carry lookahead adders, E t^2, high speed circuits, surfing, wave pipelining.
March 22, 2005 1pm, CLT.519
The Computer Ate My Vote
Peter Ryan: For centuries, in the UK at least, we have taken democracy for granted and placed trust in the paper ballot approach to casting and counting votes. In reality, the process of casting and counting votes is one of considerable fragility. This has been recognized since the dawn of democracy: the Ancient Greeks perceived the threat and devised mechanical devices to try to sidestep the need to place trust in officials. For over a century, the US has been using technological approaches to recording and counting votes: level machines, punch cards, optical readers, touch screen machines, largely in response to widespread corruption with paper ballots. In the last few years, the UK has been experimenting with alternative voting technologies. In this talk I will discuss approaches to achieving assurance of accuracy and ballot secrecy in electoral systems. In particular I will present a cryptographic scheme, based on an earlier scheme due to David Chaum that has the remarkable property of providing voters with the opportunity to verify that their vote is accurately counted whilst still ensuring the secrecy of their ballot. At the same time, minimal trust need be placed in the technology or officials.
March 15, 2005 1pm, CLT.519
Resolution of Encoding Conflicts by Signal Insertion and Concurrency Reduction Based on STG Unfoldings
Agnes Madalinski: A combined framework for the resolution of encoding conflicts in STG unfoldings is presented, which extends previous work by incorporating concurrency reduction in addition to signal insertion. Furthermore, a novel validity condition is proposed to justify these transformations.
March 8, 2005 1pm, CLT.519
Investigation on the applications of the ACMs
Fei Hao: Each part of the digital control system may execute at different speeds. The frequency diversity will lead to dead lock, which disturbs the control of the system. To make every part working properly, asynchronous communication method should be used. ACM (asynchronous communication mechanism) is a kind of component fit for this job. MATLAB models were built for buffered ACMs according to their algorithms. As a case study example, a brushless DC motor controller was used to investigate the effects after ACM was plugged in. The simulation waveforms showed the correct results as expected.
March 1, 2005 1pm, CLT.519
Asynchronous system design flow based on Petri nets
Danil Sokolov: The BESST (BEhavioural Synthesis of Self-Timed Systems) tool kit is used for asynchronous system synthesis based on Petri Nets. It incorporates software tools for high-level partitioning, scheduling, direct mapping and logic synthesis. These are used to generate efficient speed-independent circuits from behavioural Verilog specification.
February 22, 2005 1pm, CLT.519
Opacity and Anonymity (subtitle: you can't prove anything)
Jeremy Bryans: Opacity has proved to be a promising technique for describing formal security properties. In this talk we present the notion of opacity in the context of labelled transition systems. Anonymity comes in various flavours. We show how variations of opacity can be used to describe strong, weak and conditional anonymity.
December 1, 2004 1pm, CLT.519
Modelling Opacity using Petri Nets
Maciej Koutny: The talk will describe joint work with Jeremy Bryans and Peter Ryan which will appear in the ENTCS volume containing paper accepted for WISP 2004. It considers opacity as a property of the local states of the secure (or high-level) part of the system, based on the observation of the local states of a low-level part of the system as well as actions. The approach proposes a Petri net modelling technique which allows one to specify different information flow properties, using suitably defined observations of system behaviour. The talk will also discuss expressiveness of the resulting framework and the decidability of the associated verification problems.
November 24, 2004 1pm, CLT.519
Metastability In Asynchronous Communication Mechanisms (ACMs)
Neil Henderson: The control variables of ACMs have often been assumed (in academic literature) to behave like (Lamport) safe registers. This talk describes how CSP has been used, with the FDR model checker, to verify the behaviour the a number of ACMs, and the possible effects of metastability on their behaviour. It has been shown that it is important to model the effects of metastability, and the techniques used to contain those effects, correctly. Failure to do so may lead to optimistic results (a protocol may be incorrectly verified to exhibit a property), or pessimistic results (a protocol may be incorrectly verified not to exhinit a property), when models of the ACMs are model checked. None of the protocols that have been modelled are completely immune to the effects of metastability, but it is shown that more efficient algorithms can be found than current impossibility results say are possible.
November 17, 2004 1pm, CLT.519
An Algebra of Petri Nets with Arc-based Time Restrictions
Apostolos Niaouris: In this talk we present two algebras, one based on term re-writing and the other on Petri nets, aimed at the specification and analysis of concurrent systems with timing information. The former is based on process expressions (at-expressions) and employs a set of SOS rules providing their operational semantics. The latter is based on a class of Petri nets with time restrictions associated with their arcs, called at-boxes, and the corresponding transition firing rule. We relate the two algebras through a compositionally defined mapping which for a given at-expression returns an at-box with behaviourally equivalent transition system. The resulting model, called the Arc Time Petri Box Calculus (atPBC), extends the existing approach of the Petri Box Calculus (PBC).
November 10, 2004 1pm, CLT.519
Design of an Asynchronous Loadable Counter Using Petri Net Based Methods
Yu Zhou: Design of a loadable module-N counter provides a nontrivial task for people interested in asynchronous VLSI circuit programming. Different methodologies have been proposed starting with top-level specifications such as CSP (Communicating Sequential Processes) language or graphic formalism like Petri net. Decomposition and synthesis at different levels is developed afterwards till the final handshaking circuit is implemented. However, the sequential nature between the outputs and inputs of the loadable counter made a seamless output stream infeasible, which can be promisingly used for security circuit where a random sequence generator is called for. To solve this problem, FIFO is used as an interface with computing module to store input data for each bit. Each computing module in the loadable counter communicates with both its FIFO interface and neighbouring computing parts. By such an improvement, input data is dynamically loaded and the output stream exhibits a seamless pulse sequences with constant response time. The design flow based on Petri net and STG (signal transition graph) method is presented in detail in this presentation.
November 3, 2004 1pm, CLT.519
Speed-Independent Synthesis of Strongly-Indicating Combinational Logic Circuits
Will Toms: Speed-Independent synthesis of combinational logic datapath circuits using tools such as Petrify is often inefficient or infeasible because such circuits typically contain many concurrent inputs and independent outputs. A practical method for generating arbitrary N-of-M encoded combinational logic circuits will be presented using a sub-class of speed-independent circuits known as Strongly-Indicating circuits. The synthesis technique described differs from general-purpose speed-independent synthesis methods by selecting common divisors from the whole network, rather than individual signals. Because of the monotonic nature of strongly-indicating combinational logic circuits, groups of divisors can be inserted, using a simple substitution technique, without the need to verify the speed-independence of the resulting circuit through construction of a state-graph or other method. Applications include situations where combinational logics blocks are required between on-chip communication fabrics that employ delay-insensitive encodings: expensive code conversion circuits can thereby be avoided. The synthesis technique has been incorporated into the Balsa behavioural asynchronous synthesis system and has been used to synthesise complete processors using speed-independent circuits with a variety of data encodings.
October 27, 2004 1pm, CLT.519
Queues and networks at arrival and departure instants
Isi Mitrani: To evaluate the behaviour of systems where one or more service nodes are visited by one or more streams of demands, it is often necessary to distinguish the customer's view of the system from that of a 'random observer'. The relationship between the two, and its consequences for performance evaluation, will be discussed.
October 20, 2004 1pm, CLT.519
Computing Shortest Violation Traces in Model Checking Based on Petri Net Unfoldings and SAT
Victor Khomenko: Model checking based on the causal partial order semantics of Petri nets is an approach widely applied to cope with the state space explosion problem. One of the ways to exploit such a semantics is to consider (finite prefixes of) net unfoldings - themselves a class of acyclic Petri nets - which contain enough information, albeit implicit, to reason about the reachable markings of the original Petri nets. One of the possibilities for the verification process is to build a finite and complete prefix and use it for constructing a Boolean formula such that any satisfying assignment to its variables yields a trace violating the property being checked. (And if there are no satisfying assignments then the property is not violated.) In this talk a method for computing the shortest violation traces (which can greatly facilitate debugging the system) is proposed. Experimental results demonstrate that it can achieve significant reductions in the size of the Boolean formula as well as in the time required to compute a shortest violation trace, when compared with a naive approach.
September 8, 2004 3pm, CLT.120
Distributing Synchronous Specifications in GALS Architectures
Dumitru Potop-Butucaru: This presentation is about some formal aspects regarding the correct-by-construction implementation of synchronous specifications over GALS (globally asynchronous, locally synchronous) architectures. I shall introduce: 1. A macro-step formalization and a micro-step formalization of the correct implementation problem 2. The notions of weak endochrony and weak isochrony, which form together a criterion insuring the correct deployment. These notions are related to classical trace theory notions, and (most important) represent the first approach to solving our problem that supports concurrency (and thus lighter communication protocols).
July 20, 2004 2pm, CLT.519
Using Unification For Opacity Properties
Laurent Mazare: The most studied property, secrecy, is not always sufficient to prove the security of a protocol. Other properties such as anonymity, privacy or opacity could be useful. Here, we give a simple definition of opacity by looking at the possible traces of the protocol. Our approach draws on a new property over messages called similarity. Then, using rewriting methods close to those used in unification, we demonstrate the decidability of our opacity property. This is only achieved in the case of atomic keys using a method called Key Quantification.
May 20, 2004 11am, Room 120 Claremont Tower
Low Power RAM with Testability Speaker
Dhiraj Pradhan: All the existing low power designs of RAMs essentially focus on circuit level solutions. What we propose here is a novel architecture level solution. Our methodology provides a systematic trade off between power and area. Also, it allows tradeoff between test time and power consumed in test mode. Significantly, too, the proposed design has the potential to achieve performance improvements while reducing power. The basic approach here divides the RAM into modules, interconnecting these modules in a binary tree where the tree can be reconfigured dynamically during normal operation and during test mode. Furthermore, during test mode, most of the RAM can be switched off - providing major power reduction, while test application time is reduced. The aspect ratio of the modules is allowed to vary as a design parameter. The chosen aspect ratio for module impacts power/access time/area tradeoffs. Such novel features make the proposed methodology of potential practical significance. Also a design tool is developed which inputs various parameters, such as desired power/performance, and giving outputs basic design parameters such as the needed number of modules, area overhead and resulting test speed-up.
March 12, 2004 1pm, E3.03 in Merz Court
PG students presentation
Apostolos Niaouris and Arash Shahriari-Rad: Talk 1: Arash Shahriari-Rad: "Design flow for visualizing Timing Diagrams from STGs using M.G or S.M reduction" Talk 2: Apostolos Niaouris: "An Algebra of Petri Nets with Arc-based Time Restrictions"
March 5, 2004 1pm, CLT.519
Rapid Introduction to Computational Complexities
Victor Khomenko: This is a continuation of the talk given on 27th February 2004,
February 27, 2004 1pm, CLT.519
Rapid Introduction to Computational Complexities
Victor Khomenko: Most computing science people heard something about computational complexities, e.g. P vs. NP problem, or, say, that sorting can be done in O(n log n) worst case time. This talk is intended as a very basic introduction into the subject.
February 20, 2004 1pm, CLT.518
Pomset Language Equivalence Results
Eike Best: This is a continuation of the talk given on 13th February 2004
February 13, 2004 1pm, CLT.519
Pomset Language Equivalence Results
Eike Best: Pomsets (partially ordered multisets) are like words over an alphabet, but are endowed with a partial, rather than linear, ordering relation. Pomset languages are defined as sets of pomsets over a fixed alphabet, just as languages are defined to be sets of words. Labelled Petri nets are often used to generate pomset languages, since they generalise finite automata that may be used to generate (regular) languages. Constructions that preserve pomset languages are interesting, in that they can be viewed as preserving not just behaviour, but also concurrency. However, the theory of pomset language preservation is rather novel, compared with results on ordinary language preservation. In this talk, a handful of new results are explained: (a), every labelled safe marked graph (special Petri net) can be transformed into a pomset-equivalent safe marked graph without internal transitions; (b), every labelled k-bounded Petri net can be transformed into a pomset-equivalent safe Petri net, and (c), every labelled k-bounded marked graph can be transformed into a language-equivalent safe marked graph, but, in general, not into a pomset-equivalent safe marked graph. The talk describes work done by the author in cooperation with Harro Wimmel and Philippe Darondeau.
February 6, 2004 1pm, CLT.518
Causality Semantics of Petri Nets with Weighted Inhibitor Arcs
Maciej Koutny: I will describe a causality semantics for weighted Place/Transition nets with weighted inhibitor arcs (PTI-nets), by extending the standard approach based on the process semantics given through net unfolding and occurrence nets. Moreover, I will outline a framework allowing to separately consider behaviours, processes and causality, in order to facilitate the discussion of their mutual consistency for different Petri net classes.
January 13, 2004 2pm, CLT.519
Applying Process Algebra and Model-checking to Security Protocols
Peter Ryan: This will be a continuation of the talk given on 5th December 2003
December 10, 2003 2pm, CLT.518
Unified Approaches to Verification and Design of Digital Circuits
Abusaleh M. Jabir: Verification of digital circuits continues to be one of the most difficult problems in CAD, which is perhaps best highlighted by the Pentium bug. There does not seem to be a single, simple solution to this problem, owing to its complexity. In most cases, a combination of techniques are used, e.g., based on structural and functional properties of a circuit. In this talk, we shall focus on graph-based techniques for synthesis and verification of circuits at various levels of abstractions. Firstly, we shall review the well-known graph-based representation, the Binary Decision Diagram (BDD). Then, we shall present the theory behind circuit synthesis and verification in a finite field, also called a Galois field, of any order, i.e., in GF(N), where N=p^k, and p is a prime number and k an integer. A new representation, called MODD, based on finite fields will be introduced, which is capable of producing better results compared to traditional BDDs, and BMDs. The concept behind an MODD can help with verification, synthesis, and simulation of circuits, including quantum circuits. We shall present some areas where the MODD can be used for efficient representation. Finite field theory can be used for synthesis and verification of highly-testable circuits. We shall also focus on how our presented techniques can be used for such a purpose.
December 5, 2003 1pm, T519
Applying Process Algebra and Model-checking to Security Protocols
Peter Ryan: I give an overview of approaches to the analysis of security protocols. I then describe the use of the process algebra CSP to encode security protocols, their security goals and the capabilities of the adversary. I will also outline the use of the CSP model-checker FDR to perform refinement checks of protocols against their goals. The talk will include a quick refresher on CSP.
The talk will based on the Book "Modelling and Analysis of Security Protocols", Ryan, Schneider, Goldsmith, Lowe, Roscoe.
November 24, 2003 1pm, CLT.519
Computability and Complexity: Selected Topics 2
Maciej Koutny: The talk will cover some of the basic notions and results concerning computability and complexity, and will include discussion of decidability, NP-completeness and PSPACE-completeness.
November 17, 2003 1pm, CLT.519
Computability and Complexity: Selected Topics 1
Maciej Koutny: The talk will cover some of the basic notions and results concerning computability and complexity, and will include discussion of decidability, NP-completeness and PSPACE-completeness.
November 10, 2003 1pm, CLT.519
Logic Synthesis Avoiding State Space Explosion
Victor Khomenko: The behaviour of asynchronous circuits is often described by Signal Transition Graphs (STGs), which are Petri nets whose transitions are interpreted as rising and falling edges of signals. One of the crucial problems in the synthesis of such circuits is deriving equations for logic gates implementing each output signal of the circuit. This is usually done using reachability graphs. In this work we avoid constructing the reachability graph of an STG, which can lead to state space explosion, and instead use only the information about causality and structural conflicts between the events involved in a finite and complete prefix of its unfolding. We propose an efficient algorithm for logic synthesis based on the Incremental Boolean Satisfiability (SAT) approach. Experimental results show that this technique leads not only to huge memory savings when compared with the methods based on reachability graphs, but also to significant speedups in many cases.
November 5, 2003 1pm, CLT.519
Applying Process Algebra and Model-checking to Security Protocols
Peter Ryan: I give an overview of approaches to the analysis of security protocols. I then describe the use of the process algebra CSP to encode security protocols, their security goals and the capabilities of the adversary. I will also outline the use of the CSP model-checker FDR to perform refinement checks of protocols against their goals. The talk will include a quick refresher on CSP. The talk will based on the Book "Modelling and Analysis of Security Protocols", Ryan, Schneider, Goldsmith, Lowe, Roscoe.
November 3, 2003 1pm, CLT.519
An Introduction to Coloured Petri Nets
Maciej Koutny: This talk will look at some general issues concerning Coloured Petri nets, including the motivation, syntax and basic verification methods.
October 27, 2003 1pm, CLT.519
Synthesis of Petri nets from Transition Systems and Application to Construction of Protocols
Alex Yakovlev: In its first part the talk introduces the idea of synthesis of Petri nets from sequential specifications (Transiation Systems) using theory of regions. In the second part it presents a modification of the general synthesis procedure that constructs Petri nets as compositions of processes that interact "asynchronously" (via places whose state is tested by means of read arcs).
October 20, 2003 1pm, CLT.519
Asynchronous Logic and Petri nets, Part 2
Alex Yakovlev: This talk will consider the relationship between Hardware Design and Petri nets, particularly from the point of view of circuit modelling, analysis and synthesis.
October 13, 2003 1pm, CLT.519
Asynchronous Logic and Petri nets, Part 1
Alex Yakovlev: This talk will consider the relationship between Hardware Design and Petri nets, particularly from the point of view of circuit modelling, analysis and synthesis.
June 20, 2003 1pm, CLT.519
Theoretical Challenges Raised by Information Security
Peter Ryan: Throughout its history, information security has thrown up many, deep intellectual challenges. Early work in the field was often conducted in and presented in rather ad hoc models of computation etc which often tended to obscure the essence of the problem. A prime example of this is the notion of information flow, or more precisely its absence, as embodied in the notion of non-interference. Early attempts to generalise this to non-deterministic systems tended to flounder on issues of compositionality, refinement and so forth. Eventually, powerful theoretical tools and frameworks were brought bear on the issue, in particular process algebras such as CSP and CCS. This immediately throws the essence of the problem into sharp focus: ultimately it can be viewed as a problem of characterising the equivalence of processes, a notoriously difficult but thoroughly studied problem in the theory community. Problems of compositionality are also closely studied by the theorists and so immediately a vast apparatus of theory becomes available to the security community. Of course the flow in not purely one way: information security has also benefited the theory community by providing many fascinating challenges. Several advances in the state-of-the-art in model checking were stimulated by the challenge of analysing the more complex protocols encountered in information security. Similarly, attempts to find notions of refinement that preserve security properties have stimulated a deeper understanding of the nature of and various flavours of non-determinism. Indeed security properties themselves are significantly different in character from the "safety" style properties more usually studied by the theory community. Many challenges and open research questions remain, some of which I will try to outline. It seems probable that the Petri-Net community will find many stimulating challenges in the area of information security and be able to bring new perspectives and insights of their own. For example, it is clear that causality is closely related to information flow. Similarly, causality is critical in the analysis of security protocols. Given that causal structures are rather more explicit in Petri-Nets and has been extensively investigated in the Petri-Net community, it seems likely that new insights on information flow properties and security protocols can be achieved.
June 18, 2003 1pm, CLT.519
A syntax for Petri nets
Kamal Lodaya: Petri nets are a well known graphical notation for describing concurrent behaviour. 1-safe Petri nets are those which are restricted to a bounded amount of concurrency. We seek syntactic characterizations for the poset behaviour of finite 1-safe net systems, by proving the analogues of Kleene/Myhill-Nerode/Buchi theorems known for finite automata. We are able to characterize the series-parallel poset behaviour of finite 1-safe net systems, and some subclasses. We also sketch ongoing work to extend the characterization to all poset behaviour.
May 30, 2003 3pm, CLT.519
The pi-calculus with types: a tool for representation
Kohei Honda: The pi-calculus is based on two ideas, name passing and simple forms of composition of processes. Through the study of many researchers, a stunning expressive power of this combination has been uncovered for representing dynamics and algebra of diverse classes of computation. However there is certain lack of precision in known representations (for example they are rarely equationally fully abstract). Recently Berger, Yoshida and I found that a use of a simple notion of types, suggested from Linear Logic and game semantics, can make the representation of known programming languages semantically exact. The representability extends from higher-order procedures to imperative constructs (such as references and control) to objects to generic computation to concurrency to elements of distributed computing. In this talk I would illustrate how and why the use of types makes the pi-calculus a powerful tool for representing computation, and how we can apply such representation to theory and practice, both through concrete examples. Among others I shall focus on basic ideas of typing, how behavioural theories can be derived from syntax, and how they can be applied in practice. If time allows, I would also suggest how these theories may serve as a useful tool for the study of specification/verification methods for open distributed systems.
May 9, 2003 1pm, CLT.519
A tutorial on using SAT based techniques to solve hard problems
Victor Khomenko: I will give a brief introduction into Boolean Satisfiability (SAT): the problem itself, techniques of its solving, ways of reducing other problems to SAT, and some applications.
May 2, 2003 1pm, CLT.519
Formal investigations of correctness of an Asynchronous Communication Mechanism
Neil Henderson: This talk will describe a my attempts to prove correctness of an ACM, first using refinement, and then using a compositional rely-guarantee method for "interleaved" concurrent processes. I will discuss the merits of my results in comparison with other proof methods, and the lessons learned from the work.
March 28, 2003 , CLT.519
Testing in the direct mapping synthesis domain
Deepali Koppad
March 14, 2003 , CLT.519
Can we Render Asynchrony to our Industry Caesars? Part 2
Alex Yakovlev
February 28, 2003 , CLT.519
Can we Render Asynchrony to our Industry Caesars?
Alex Yakovlev
February 21, 2003 , CLT.519
Strategic Meeting
Maciej Koutny and Alex Yakovlev
February 7, 2003 , CLT.519
Low-Latency Control Structures with Slack
Alex Bystrov
January 31, 2003 , CLT.517
Introduction to pi-calculus 3
Maciej Koutny
December 13, 2002 , CLT.517
Introduction to pi-calculus 2
Maciej Kounty
December 6, 2002 , CLT.517
Introduction to pi-calculus 1
Maciej Koutny
November 29, 2002 , CLT.517
Unfoldings of coloured Petri nets
Victor Khomenko
November 15, 2002 , CLT.517
Detecting State Coding Conflicts in STGs Using SAT
Victor Khomenko
November 8, 2002 , CLT.517
Visualisation and Resolution of Coding Conflicts in Asynchronous Circuits Design
Agnes Madalinski
October 25, 2002 , CLT.517
STG Optimisation in the Direct Mapping of Asynchronous Circuits
Danil Sokolov
October 18, 2002 , CLT.516
A tight packing scheduling algorithm using closeness tables
Frank Burns
July 3, 2002 2pm, Room T516
Specifying communications in temporal logic
R. Ramanujam
May 20, 2002 3pm, Room T516
Lock-free data structures
Tim Harris
April 24, 2002 2pm, Room T516
High Level Synthesis Of Asynchronous Digital Systems, Continued...
Susan Tyerman
April 22, 2002 3.10pm, Room T516
High Level Synthesis Of Asynchronous Digital Systems
Susan Tyerman
March 18, 2002 3.10pm, Room T922
Causal Time in Practice
Hanna Klaudel
February 18, 2002 3.10pm, Room T516
Discussion: translating high level specifications expressed in Balsa into Petri nets
Open
February 11, 2002 3.10pm, Room T516
Design Flow for Self-Timed Controllers
Alex Yakovlev
February 4, 2002 3.10pm, Room T922
Detecting State Coding Conflicts in STGs Using Integer Programming
Victor Khomenko
January 1, 2002 1pm, E4, Basement, Merz Court, School of EECE
Trellis Processes : a Tool for Distributed System Monitoring
Eric Fabre
December 12, 2001 10am, Room T517
Synthesis of Asynchronous Circuits
Alex Smirnov
December 5, 2001 10am, Room T517
Compositional Development in the Event of Interface Difference: using FDR2 for automatic verification
Jon Burton
November 28, 2001 10am, Room T517
Canonical Prefixes of Petri Net Unfoldings
Maciej Koutny
November 14, 2001 10am, Room T517
Analysis of dynamic behaviour of multi-flops
Oleg Maevsky
November 7, 2001 10am, Room 831
Parallelisation of the Petri Net Unfolding Algorithm
Victor Khomenko
October 31, 2001 10am, Room 831
Unfolding-based approach to LTL model-checking
Javier Esparza
October 24, 2001 10am, Room 831
Incompletely self-timed systems: in search of a 'complete' solution for Giga-LSI?
Alex Yakovlev
October 17, 2001 10am, Room 831
Direct mapping of asynchronous circuits from STGs
Alex Bystrov
October 10, 2001 10am, Room 831
Improving the efficiency of constructing unfoldings
Victor Khomenko
May 29, 2001 10am, Room 922
Modelling and Verification of Broadcast Protocols
David Kendall
May 15, 2001 10am, Room 922
"foldings" of unfoldings
Discussion
May 1, 2001 3.30pm, Room 831
A tool for visualising state graphs for concurrent systems
Stuart Grey
May 1, 2001 10am, Room 922
Temporal Logic and Compositionality
Ben Moszkowski
March 6, 2001 1pm, Room 922
Modelling Communication Protocols
Neil Henderson
March 6, 2001 12.30pm, Room 922
Abstraction Mechanisms in CSP
Jon Burton
February 20, 2001 10am, Room 922
Net unfoldings
Discussion Session 2
February 6, 2001 10am, Room 922
Net unfoldings
Discussion Session 1
December 12, 2000 9.30am, Room 922
Experiences with testing VLSI chips
Delong Shang
December 5, 2000 9.30am, Room 922
Asynchronous Communication Mechanisms
Fei Xia
November 28, 2000 9.30am, Room 922
Identifying CSC conflicts in STGs using unfoldings
Agnes Madalinski
November 21, 2000 9.30am, Room 922
CSP and Abstraction Mechanisms
Maciej Koutny
November 14, 2000 9.30am, Room 922
Introduction to CSP (continued)
Maciej Koutny
October 24, 2000 9.30am, Room 922
Basic ideas behind CSP
Maciej Koutny
October 17, 2000 9.30am, Room 831
Synthesis and implementation of an Asynchronous Communication Mechanism
Alex Yakovlev
September 20, 2000 , Room 922
Various talks on Petri Nets, Box Algebra and Time
BAT Workshop
May 19, 2000 10am, Room 922
Model Checking using Net Unfoldings
Fitto Alamsyah
May 18, 2000 , Room 831
Petri Nets, Box Algebra and Time
BAT Workshop
May 12, 2000 10am, Room 922
Compositional model of Petri Nets: Part 2
Maciej Koutny
May 5, 2000 10am, Room 922
Compositional model of Petri Nets: Part 1
Maciej Koutny
March 31, 2000 10am, Room 922
Petri Net Unfolding
Fitto Alamsyah
March 24, 2000 10am, Room 922
Verification and Abstraction Mechanisms
Jon Burton
March 17, 2000 10am, Room 922
Linear programming and Model Checking
Victor Khomenko
March 10, 2000 10am, Room 922
Behavioural Equivalences
Maciej Koutny
March 3, 2000 10am, Room 922
Synthesis of Asynchronous Circuits (Part II)
Alex Yakovlev
February 25, 2000 10am, Room 922
Synthesis of Asynchronous Circuits (Part I)
Alex Yakovlev
January 20, 2000 12pm, Room 922
Formal Modelling of Asynchronous Hardware
Alex Yakovlev
August 19, 1911 11am, CPD room (M413) , Merz Court
Leading Edge Mobile Media Processors
Kelvin Gardiner: The increase in mobile devices, in particular the recent explosion of tablet computing, has lead to a demand for low power media processors that can deliver high performance in the post-PC era. This talk introduces ZiiLABS ZMS series of mobile media processors, which feature a flexible SIMD array which can deliver media acceleration, 3D graphics and OpenCL while using dynamic power management to deliver low power requirements. The architecture of the chip is outlined and a number of features highlighted. An overview of the design flow and test infrastructure is given. The relationship between software and hardware is also discussed.
November 30, 1999 ,
November 30, 1999 ,
November 30, 1999 ,