T1: Timed Multi-Threaded Formal Object Modeling Techniques
Jin Song DONG, National University of Singapore, Singapore


Abstract: The design of complex systems requires powerful mechanisms for modeling data, algorithms, concurrency, and real-time behaviour; as well as for structuring and decomposing systems in order to control local complexity. Method integration has become a recent research trend in software specification and design. In graphical area, many object-oriented methods merged into one, the Unified Modeling Language (UML) which has combined various diagrammatic modeling techniques to model static and dynamic aspects of software systems. In formal area, method integration is even more motivated as many traditional formal methods do not scale-up well. Integrated formal methods becomes a very active research area.

This tutorial presents powerful integrated formal object modeling techniques for specifying real-time, concurrent, and reactive systems. The notation Timed Communicating Object Z (TCOZ) builds on state-based Object-Z's strengths in modeling complex data and state, and on the event-based Timed CSP's strengths in modeling process control and real-time interactions. TCOZ is novel in that it includes timing primitives, properly separates process control and data/algorithm issues and supports the modeling of multi-threaded concurrency. In addition to the inherited CSP's channel-based communication mechanism, in which messages represent discrete synchronisations between processes, TCOZ is extended with continuous-function interface mechanisms inspired by process control theory, the sensors and the actuators. Those communication interfaces (channels, sensors and actuators) are given an independent, first class role in TCOZ. This allows the communications and control topology of a network of objects to be designed orthogonally to their class structure and reduces the need to reference other classes in class definitions, thereby enhancing the modularity of system specifications.

This tutorial includes: Introductions to Object-Z, Timed CSP and UML, Detailed presentations on TCOZ: active and passive objects, sensors and actuators, and linking TCOZ with UML.

In this tutorial, other approaches on integration of state-based and event-based notations are also discussed and compared to TCOZ. A number of examples and a non-trivial case study on using TCOZ are presented.


T2: Project on Global Information Processing Technology at Electrotechnical Laboratory
Kazuhito Ohmaki, Satoshi Sekiguchi, Nobuyuki Yamasaki, Yasuo Kuniyoshi, Computer Science Division, Electrotechnical Laboratory, Japan


(1) Kazuhito Ohmaki We are doing a five-year research project on global information processing technology since 1996. We have three research groups in this project to develop, 1) software technologies to be used in the Internet 2) seamless architectures in between hardware and software, and 3) theories and experiments for complex systems. I will introduce this project in my talk, and the following three speakers will give their research areas.

(2) Satoshi Sekiguchi Grid technology for high-end computing infrastructure.

This talk covers an overview of high-performance world wide computing systems, or "computational grids". Emerging high-performance networks enable a wide range of application concepts such as supercomputer ensemble, remote computing service, computing resource exchange market. Recent research activities in regards to this grid technology will be introduced and discussed.

(3) Nobuyuki Yamasaki Responsive Processor for Parallel/Distributed Real-Time Control.

This paper describes the design and implementation of Responsive Processor for parallel/distributed real-time control, which can control various embedded systems including robots, home automation, office automation, factory automation, etc. Responsive Processor integrates an MPU core (SPARC), four Responsive Links for real-time communication, and many peripheral functions including SDRAM I/F, DMAC, PCI, USB, PWM generators, A/D converters, D/A converters, etc. At the core part of the chip, Responsive Link provides the scalable real-time communication by four pairs of a two-way event link and a data link. Each packet on the link is prioritized to enable overtaking and shortcut routing. Many kinds of control systems can be composed by connecting Responsive Processors using Responsive Links.

(4) Yasuo Kuniyoshi Complex Real World Information Processing for A Humanoid Robot Authors: Yasuo Kuniyoshi, Olivier Stasse, Youichi Ishiwata, Gordon Cheng, Akihiko Nagakubo.

A whole body humanoid robot has many dozens of actuators and sensors which must be controlled and processed in a coordinated mannar under strict real time requirements. Moreover, the entire system must incorporate broad range of processing from motor control and signal processing to high cognitive functions such as situation recognition, inference, decisions, memory and planning. What makes it even more difficult are the real world effects such as noise and uncertainty. This paper presents our ongoing efforts developing a 46 joints whole body humanoid, high performance communication/control network called 'in-body LAN', a 'proper' real time kernel based on Linux called 'ART-Linux', and a versatile real time parallel software development and execution environment called 'PredN'. This system is used as a research tool to explore novel principles exploiting the characteritics of "global information structures" inherent in the sensor-motor interaction pattern information. Unlimited to robotic cases, we believe that such principles can be applied to more general complex information processing which has consistent underlying constraints.


Application of Formal Methods to Railway Systems
Jim Woodcock, Computing Laboratory, Oxford University, UK