DeTfoRS: Design Techniques for Real-Time Hybrid Systems

II/1/1/1 DeTfoRS: Design Techniques for Real-Time Hybrid Systems

Synopsis

Real-time hybrid systems form an important class of today's computer-controlled systems, such as computer controlled lifts, robots, assembly lines, etc. Typically they are computer-embedded systems, where computers interface to and control physical equipment. Such systems are often required to respond to externally generated stimuli with specified real-time constraints. Safety and reliability of systems are extremely critical.

The DeTfoRS project conducts research with UNU/IIST Fellows and Visitors on formal design of real-time hybrid systems using a formal system called Duration Calculus (DC).

The DC was proposed by C. Zhou, C.A.R. Hoare and A.P. Ravn, and developed initially with several other colleagues in the ProCoS project (ESPRIT BRA 3104).

The duration calculus is a logic for describing and reasoning about the real-time behaviour of systems, where states change over time and are represented by functions from time (reals) to the Boolean values (0 and 1).

It is an extension of Interval Temporal Logic (Moszkowski & Manna), but with continuous time, and uses integrated durations of states as interval temporal variables. Assuming finite variability of state functions, the axioms and rules of the DC constitute a complete logic (relative to Interval Temporal Logic).

By using DC as a formal system for specifying and reasoning about real-time hybrid systems, the project has extended DC further, has developed several techniques for specification and verification, and has investigated mechanical support. Many fellows have been trained and dozens of reports have been produced since 1993 by the project. The project has made UNU/IIST an acknowledged leader in the field of DC.

Period

1993 - 1998

Aims & Objectives

DeTfoRS aims to develop formal techniques for designing real-time hybrid systems. The techniques include

• design calculi based on Duration Calculus and its extensions, to specify and reason about behaviour of real-time dynamic systems, e.g. schedulers, auto pilots, computer-embedded systems, communication protocols, etc.

• formal semantics of real-time languages (e.g. Timed CSP, Esterel, Verilog, etc),

• deductive verification methods and tools for real-time programs

• decidability issues of Duration Calculus, model-checking techniques and tools for real-time systems based on DC

DeTfoRS also aims to contribute to

1. communication between developing countries and the international computer science community.

2. training of qualified computer scientists and engineers for the advanced software design and development.

Staff responsible

Zhou Chaochen
Dang Van Hung
Xu Qiwen

Cooperations

• The research project DeTfoRS was in cooperation with the EC project ProCoSy II (ESPRIT BRA 7071) in Europe under ESPRIT Exploratory Activity KIT 010 in the period of 1995-1997. The European partners were from Kiel University, Oldenburg University, Oxford University and Technical University of Denmark.

• In 1993-1995, the project was also in cooperation with the Chinese 863 HiTech Programme. The Chinese partners were from Beijing University of Aeronautics and Astronautics, Changsha Institute of Technology, Nanjing University and Shanghai Jiao Tong University.

Partner Institutions

Beijing University, P R China
Beijing University of Aeronautics and Astronautics, P R China
Shanghai Jiao Tong University (SJTU)
Changsha Institute of Technology, Hunan, P R China
Chengdu Institute of Computer Applications, Academia Sinica, P R China
Institute of Information Technology, Hanoi, Vietnam
De La Salle University, Manila, The Philippines
University of Indonesia, Indonesia
Nanjing University, P R China
Tata Institute of Fundamental Research, India
University of Hyderabad, India
Catholic University of Pelotas, Brazil
East China University of Science and Technology, P R China
University of Buenos Aires, Argentina
National University of Hanoi, Vietnam
University of Macau, Macau
Kiel University, Germany
Oldenburg University, Germany
Oxford University, United Kingdom
Technical University of Denmark, Denmark

Deliverable

54 Technical Reports have been produced in the projects until March 1998. Among them 30 have been published in journals or refereed conference proceedings. Please see III/1 for more information of these reports, many of which can be obtained by ftp.

Achievements in 1997

After successes in earlier periods, in 1997 UNU/IIST staff and Fellows, together with visitors and collaborators, have studied new DC-based techniques for specification, refinement and verification of real-time and hybrid systems, and also tools to support these techniques. The achievements include:

1. Some new specification and verification techniques for designing real-time reactive systems have been developed. These are two-dimensional time interval logics, which can express the behaviour of real-time reactive systems both at the abstract and at the detailed level. With these techniques, one can also specify and verify unbounded liveness & fairness easily. (See [1][2][3][4])

2. A new variant of Duration Calculus, which includes super-dense states, fixed points and infinite intervals is proposed. Based on it, a comprehensive theory of sequential hybrid systems has been developed. (See [5][3][6])

3. A geometric approach to solving the inverse kinematics for all 3-joint placeable robotic manipulators. This technique might be generalised to 6-joint manipulators as well. (See [7])

4. Mechanical verification of the Biphase Mark Protocols using DC model and a PVS (a theorem proving system developed at SRI) based DC tool; the results can be applied to choose an optimal value for the parameters of the protocol used in industry. (See [8])

5. A comprehensive proof of the decidability of an important class of DC under synchronous interpretation. The result shows that one can check the consistency of real-time requirements by an algorithm. (See [9])

6. Techniques and tools for checking a class of real-time, hybrid, parallel systems for linear duration calculus invariants, an important class of DC formulas in specifying real-time, hybrid systems. That means that in many cases we can decide the correctness of a system automatically by using a computer. This is a great help for system designers since verification is not only tedious but also very difficult and complicated. (See [10][11])

7. Verification techniques for real-time parallel systems. In particular, the assumption-commitment rule is embedded in two-dimensional DC. (See [12])

8. An initial attempt to formalise the semantics of shared variable parallel programs, aiming at eventually formalising the semantics of Verilog (a hardware description language widely used in VLSI design).

9. Specification and verification of a fault-tolerant algorithm in hybrid systems. (See [13])

The research achievements in 1997 resulted in 12 publications and reports.

DeTfoRS: Design Techniques for Real-Time Hybrid Systems