AGENDA
(updated version)
Day 1 (Mon, 25 May 1998)
9:30 - 10:00: Opening Session
Morning session, Chair: Zhou Chaochen, UNU/IIST
The Ethics of Safety-Critical Systems
Time: 10:00 - 11:00
Speaker: Jonathan P. Bowen - The University of Reading, UK
Abstract: Safety-critical systems require the utmost care in their
specification and design to avoid errors in their implementation,
using state of the art techniques in a responsible manner. To do
otherwise is at best unprofessional and at worst can lead to
disastrous consequences. An inappropriate approach could lead to
loss of life, and will almost certainly result in financial
penalties in the long run, whether because of loss of business or
because of the imposition of fines. Legislation and standards
impose external pressures, but education and ethical
considerations should help provide more self-imposed guidelines
for all those involved in the production of safety-critical
systems. This presentation considers some of the issues involved,
with pointers to material providing greater depth in particular
areas, especially with respect to the use of formal methods.
11:00 - 11:30: Tea Break
UNU/IIST's Advanced Development Projects
Time: 11:30 - 12:00
Speaker: Chris
George - UNU/IIST
Abstract: We give an overview of UNU/IIST's advanced development projects.
We explain our aims in running them, how we choose them, the
themes which run through them. We also explain the method we use,
and describe some examples.
Combining Duration Calculus with RAISE
Specification Language
Time: 12:00 - 13:00
Speaker: Xia Yong - UNU/IIST, from East China
University of Science and Technology
Abstract: The goal of our work is two-fold:
(1) to extend RSL with real-time features, called TRSL,
and (2) to bridge TRSL with DC.
TRSL is an extension of RSL with time constructors, wait and etc., proposed by C.W.George. This talk will give an operational semantics, in the core syntax of TRSL, and define preorder and test equivalence relation among them. The consistency between proof rules of (T)RSL and the operational semantics is proved.
The work to bridge TRSL with DC is on-going. In order to prove DC theorems with RAISE Justification tool, Anne Haxthausen and I embed DC into RSL and setup a Proof Assistant, DC/RJ. An "operational semantics with explicit states" is given, and some satisfaction relations between TRSL and DC are defined. We are now working on a proof system.
13:00 - 14:30: Lunch break
Afternoon session, Chair: Chris George, UNU/IIST
A Compositional Semantics of SL Using Duration Calculus of
Weakly Monotonic Time
Time: 14:30 - 15:30
Speaker: Paritosh Pandya, Tata Institute for
Fundamental Research (TIFR), Mumbai, India
Abstract: Synchronous reactive languages are given semantics under the synchrony
hypothesis that states that computation and communication do not take
time. As a result, instantaneous dialogs can occur between concurrent
processes. Duration Calculus of Weakly Monotonic Time (WDC) is an
extension of DC which incorporates the view that a discrete sequence of
states can arise at the same time point in a behaviour.
As a result, it is well suited to give semantics of synchronous languages.
SL is a synchronous reactive language related to Esterel. While it is less expressive that Esterel, every SL program is guaranteed to be coherent and deterministic. We will describe a compositional semantics of SL using a variant of WDC which incorporates infinite intervals and state quantification. The semantics translates every SL program into a WDC formula capturing its behaviour.
The MIICI Project
Time: 15:30 - 16:30
Speaker: Zheng Hongjun - UNU/IIST,
from Beijing University
Abstract: An enterprise is a socio-economic organisation created to produce
products or procure services, and to make profit. Enterprise
modelling is about building models for various aspects of the
enterprise, in order to better understand how the enterprise works,
to capitalise acquired knowledge, to support management decisions,
to analyse, simulate, build and re-build parts of the enterprise.
Creating enterprise models incurs problems not unlike those for
design of complex dynamic systems. We exploit this analogy in the
MIICI project to study how formal methods can provide notations,
methods and tools to treat the enterprise as an engineering
artifact.
In this overview talk we examine methods to describe an enterprise formally, to relate descriptions at different levels of abstraction, to compose and refine such descriptions.. Adopting abstraction is crucial to unify representations, apply common modelling principles and tools, build models which cross organisational boundaries (extended/virtual enterprise).. Here we adopt a concrete (but popular) perspective on the manufacturing firm where it consist of a set of resources and a set of processes (with priorities) which execute concurrently on the resources. A process is really a sequential program which executes on the enterprise resources, subject to some management decisions. We believe a combination of abstract data types to model resources and calculi for concurrency to model processes as well as interactions between enterprises, provide the right modelling tools on this level. We carry out a sequence of examples to illustrate the issues involved and convey intuitions.
16:30 - 17:00: Tea break
The MultiScript Project
Time: 17:00 - 18:00
Speaker: Richard Moore - UNU/IIST
Abstract: The project is studying the creation and presentation of documents
in which more than one language is used, for example a
dictionary from one language to another. Particular emphasis is
being placed on support for languages which are not read and
written in the standard European style (left to right and top to
bottom), for example Japanese, Chinese, Mongolian, and Arabic, and
on how these can be combined in a single document while all still
retaining their traditional directionality.
A comprehensive study of a wide range of existing multi-lingual documents has been carried out, on the basis of which a formal model of generic multi-directional multi-lingual documents has been defined. This forms the basis for work on the definition of how such documents can be displayed, edited, etc.
The requirements for a software system supporting the creation and browsing of multi-lingual documents are also being defined, and these will be used as the foundation for the design and implementation of a prototype software system in the next phase of the project.
Day 2 (Tue, 26 May 1998)
Morning session, Chair: Hans Rischel, Danish Technical University
Operational and Logical Semantics for
Polling
Real-Time Systems
Time: 9:30 - 10:30
Speaker: Henning Dierks -
Oldenburg University
Abstract: PLC-Automata are a class of real-time automata suitable to
describe the behavior of polling real-time systems. PLC-Automata
can be compiled to source code for PLCs, a hardware widely used in
industry to control processes. Also, PLC-Automata have been
equipped with a logical and operational semantics, using Duration
Calculus (DC) and Timed Automata (TA), respectively.
In the talk we summarize some theoretical results on PLC-Automata and explain in more detail the relationship between both semantics. The three main topics of this talk are:
10:30 - 11:00: Tea break
DC/P: A Proof Assistant for Interval Logics
Time: 11:00 - 12:00
Speaker: Hu Chengjun - UNU/IIST, from Changsha Institute of Technology
Abstract: The Duration Calculus Prover (DC/P), is an interactive proof
assistant for a family of dense time interval logics, namely,
Neighbourhood Logic, dense time Interval Temporal Logic, Mean
Value Calculus, and Interval Calculus. DC/P is implemented by a
semantic encoding of the logics in a higher order logic. In this
paper, we mainly introduce our implementation of a proof system -
a Gentzen style sequent calculus. We show that this proof system
is sound and relatively complete. An advantage of our approach is
it is quite general, it can be applied to other proof systems such
as tableaux methods, resolution, etc. Finally, we also give a
comparison of our system with Skakkebæk's PC/DC.
Program Theories in Duration Calculus
Time: 12:00 - 13:00
Speaker: Xu Qiwen - UNU/IIST
Abstract: A real-time program contains lower level primitives representing
computation steps and advance of time. The discrete actions are
usually considered instantaneous, and subsequently several such
actions may happen at the same real time point governed possibly
by a causal order. Such abstraction, proposed initially in the
work on synchronous languages, provides substantial simplification
in verification. Intertwining with recursions, real-time program
can exhibit a rich variety of behaviours. Duration Calculus has
been extended to the so-called weakly monotonic time, infinite
intervals and with fixed-point operators. Based on such extensions
of Duration Calculus, we develop formal theories of real-time
programs. These include semantics of real-time concurrent
languages, such as the hardware description language Verilog,
verification and refinement methods for time automata, and
assumption-commitment paradigm for compositional reasoning.
13:00 - 14:30: Lunch break
Afternoon session, Chair: Richard More, UNU/IIST
Provably Correct Hardware Compilation
Time: 14:30 - 15:30
Speaker: Jonathan Bowen - The University of Reading, UK
Abstract: The availability of Field Programmable Gate Arrays (FPGA) allows
the fast generation of hardware by a purely software process. This
enables the automatic compilation of a high level description of
hardware into a "netlist" of individual digital hardware
components. The compilation scheme may be verified, allowing an
arbitrary number of circuits to be compiled with the same level of
assurance, instead of needing to be checked individually. The
compilation theorems also may be rapid-prototyped very directly in
a logic programming language such as Prolog. The high level
language used for the circuit description is based on Occam, which
includes parallel constructs, allowing algorithms for (naturally
parallel) hardware to be coded conveniently and efficiently.
A Process Calculus Based on the Agent-Place
Model
Time: 15:30 - 16:00
Speaker: Kenji Taguchi, Kyushu University, Japan
Abstract: Recently, the notion of mobile agents is proposed in order to capture
the new form of computation in the communication network. A mobile agent
is a computer program which can move around different hosts on the network
while carrying code and data. A number of programming languages such as
Telescript, FACILE, Obliq are proposed to support this new computation
paradigm.
We will present a new process calculus for mobile agents called the AP (Agent and Place)-calculus. The calculus is based on the agent-place model which is a basis for mobility of an agent language Telescript. The calculus is not developed as a foundational calculus, but rather as a formal framework for specifying and verifying mobile applications such as electronic commerce and virtual shopping mall. We will describe its operational semantics and give simple examples in order to demonstrate its applicability.
Using Functional Programming in The
First Programming Course
Time: 16:00 - 16:30
Speaker: Hans Rischel - Danish
Technical University
Abstract: To be given
16:30 - 17:00: Tea break
Incremental Refinement for
Fault-Tolerance
Time: 17:00 - 18:00
Speaker: Tomasz Janowski - UNU/IIST
Abstract: This presentation is about design of reliable systems from unreliable
components. In particular, we consider how weak assumptions about
faults affect the complexity of the design for fault-tolerance. This
leads us to study an incremental refinement to tolerate such faults
gradually (one at a time), where every step increases or at least
preserves the current level of fault-tolerance. Such refinement can be
used on system components, thereafter allowing to deduce
fault-tolerance about the system itself. We cast those ideas in the
semantic framework which extends CCS (for implementation) and
mu-calculus (for specification and verification) to account for
unpredictability of faults: fault-tolerance must be invariant under
the removal of an arbitrary set of fault from the assumptions. As an
illustrative example we use a distributed database which supports
atomic transactions despite faults affecting its components.
19:30 - 21:30: Workshop Dinner
Day 3 (Wed, 27 May 1998)
Morning session, Chair: Dang Van Hung, UNU/IIST
Duration Algebra
Time: 9:30 - 11:00
Speaker: Burghard von Karger - Kiel University
Abstract: Temporal Algebra is an algebraic calculus that encompasses many
temporal logics, including linear temporal logic, CTL* and
interval logic. In our lecture we will give an account on how the
duration calculus of Zhou, Hoare and Ravn is modelled in temporal
algebra. As an application we will establish a proof rule for
control loops.
11:00 - 11:30: Tea break
Deductive Reasoning in Duration Calculus
Time: 11:30 - 12:00
Speaker: Michael
R. Hansen - Danish Technical University
Abstract: To be given
A Calculus of Durations on Abstract Domains:
Completeness and
Extensions
Time: 12:00 - 13:00
Speaker: Dimitar Guelev, UNU/IIST, from
University of Sofia
Abstract: This paper presents a completeness theorem for
duration calculus and some of its application-oriented extensions
with respect to an abstractly specified class of frames, as opposed
to the result on the standard real-time frame coped with in
[HZ92]. The choice of abstract semantics gives the opportunity to
prove completeness of duration calculus not relative to a semantically
defined set of axioms, as needed for its completeness on the
standard frame. The abstract semantics captures the essential
property of finite alternation of states, as present in
duration calculus, which is actually given axiomatization in the
framework of interval temporal logic, where from proof systems for
duration calculus and some extensions of its are derived. These
include two-dimensional interval logic, two-dimensional duration
calculus and duration calculus for weakly monotonic time [PD97]
13:00 - 14:30: Lunch break
Afternoon session, Chair: Burghard von Karger - Kiel University
Linking Interval-based and Point-based Temporal
Verification of Real-time Systems
Time: 14:30 - 15:00
Speaker: Wang Ji, UNU/IIST, from
Changsha Institute of Technology
Abstract:
In this paper, we propose a new framework for reasoning about real
time systems. The formalism, called DCTL, is a combination of Choppy
Logic (by Pnueli) and
Duration Calculus with Weakly Monotonic Time (by Paritosh and Dang), and
hence one can specify in DCTL the duration of states as well as the
temporal order of events and actions. Thus, the new logic can be
used to reason about the super-dense computation model of real-time
systems and also acts as a bridge between Duration Calculus and
Linear Temporal Logic. A distinguish feature of this logic is that a
rule characterizing the natural induction is available and one can verify
a property in DCTL for a real-time program by using the same
technique as in the reactive case.
On Checking Real-Time Systems for
Linear
Duration Invariants
Time: 15:00 - 15:30
Speaker: Dang Van Hung - UNU/IIST
Abstract: In this talk we
define timed regular expressions to describe the timed behaviour of
parallel real-time systems and consider the problem of checking
algorithmically the set of timed behaviours defined by timed regular
expressions for a real-time requirement specified by a linear
duration invariant. In general, the problem can be solved by using
the mixed integer linear programming techniques. We show that in
many cases, the problem can be reduced to a finite number of linear
programming problems.
On Checking Parallel Real-Time Systems for
Linear Duration Properties
Time: 15:30 - 16:30
Speaker: Zhao Jianhua - UNU/IIST, from Nanjing University
Abstract: The major problem of checking a parallel composition of real-time
systems for a real-time property is the explosion of untimed
states and time regions. To attach this problem, we define define
a compatibility relation, which is a one-direction simulation
relation between two configurations. Based on this technique, we
develop an algorithm for checking a real-time automaton network
with shared variables w.r.t. a linear duration property. Using
Fischer's mutual exclusion protocol as a case study, we show that
our algorithm can avoid exhaustive state space exploration
significantly in some cases in comparison to some other tools in
the literature. We will also roughly discuss for what kind of
automaton this technique is effective and some potential usage of
this technique.
16:30 - 17:00: Tea break
Duration-Constrained Regular Expressions
Time: 17:00 - 18:00
Speaker: Li Xuandong - Nanjing University
Abstract: In this presentation, we introduce duration-constrained regular
expressions to model real-time and hybrid systems. It is an
extension of regular expressions with duration constraints. For a
class of linear hybrid automata called loop-closed automata in
which any variable tested in a loop is reset or tested to exact
values in the same loop, we show that the formalism of
duration-constrained regular expressions is equivalent in
expressive power to this class of linear hybrid automata so that
based on duration-constrained regular expressions, we can attack
some verification problems of this class of linear hybrid
automata.
Day 4 (Thu, 28 May 1998)
Morning session, Chair: Michael R. Hansen, Danish Technical University
Towards a Theory of Sequential Hybrid Programs
Time: 9:30 - 10:30
Speaker: Wang Hanping - UNU/IIST, from Beijing University
Abstract: A theory of Sequential Hybrid Programs (SHP) is studied. SHP is a
programming notation for representing hybrid systems. It contains
a phase statement and the normal sequential programming constructs
such as assignments, conditionals and iterations. Time dependent
dynamical activities of the system are specified by phase
statements. Intermixing of these two features leads to programs
with a rich diversity of behaviours including super dense
computations, infinite executions, finitely divergent executions
and instantaneously divergent executions. Duration calculus is
extended with super dense states, fixed-point operators and
infinite intervals to give a logic USDCI. A compositional
semantics of SHP programs is defined using the logic USDCI.
Several high level proof rules are derived for establishing
specific kinds of properties of SHP programs such as total
correctness and invariance. These high level proof rules provide a
modular and syntax directed method for establishing the properties
of SHP programs with the program structure guiding the proof of
correctness.
10:30 - 11:00: Tea break
Executable Specification of Concurrent Real-Time
Systems
Time: 11:00 - 12:00
Speaker: Li Xiaoshan, University of
Macau
Abstract: In general, a real-time industrial control system consists of several
interactive physical components, such as plant, actuators, sensors, and
controlling computer. Therefore, it is natural to design and specify the
system into several parallel processes. Interval Temporal Logic can be
used to present the specification of high-level abstract requirements,
such as safety and liveness. Meanwhile the executable subset of
ITL can also be used to specify the low-level design. And
this concurrent executable specification of the system design has an
advantage which other formal methods do not have. That is to
simulate the design so that the consistency of specification and
partial correctness of design, i.e., whether the design satisfies the
requirements, are checked before formal verification.
A method for developing timed RSL specifications
Time: 12:00 - 13:00
Speaker: Chris George, UNU/IIST
Abstract:
13:00 - 14:00: Lunch break
Afternoon session, Chair: Jonathan Bowen - The University of Reading
14:00 - 16:00: Discussion about further cooperation
16:00 - 19:30: Macau Tour
Day 5 (Fri, 29 May 1998)
One-day visit to Zhuhai, China