AGENDA
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.
A Process Calculus based on the Agent-Place
Model
Time: 12:00 - 12:30
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: 12:30 - 13:00
Speaker: Hans Rischel, Danish
Technical University
Abstract: To be given
13:00 - 14:30: Lunch break
Afternoon session, Chair: Chris George, UNU/IIST
Unifying Theories of Programming
Time: 14:30 - 15:30
Speaker: Jifeng He -
Oxford University, UK
Abstract: A theory of programming starts with a complete Boolean algebra of
specifications, and defines healthiness conditions which exclude
infeasibility of implementation. These are expressed as algebraic
laws useful for transformation and optimisation of designs.
Programming notations and languages must be restricted to those
preserving all the healthiness conditions. We have explored a wide
range of programming paradigms, including non-deterministic,
sequential, parallel, logical and probabilistic. In all cases, we
have found a single healthiness condition, formalised by
constructions due to Karoubi and to Kleisli. The ultimate goal of
the investigation is to maintain a clear notion of correctness
throughout the chain that leads to programs that are proved to
meet the original specification. The main contribution of this
work is the introduction of a bit of category theory to codify a
rather wide range of healthiness conditions needed in a general
theory of programming, and to show how they are all special cases
of the same construction. We also illustrate how the programming
features can be added to a category one at a time, using a
succession of different Kleisli triples, and how they can be
combined without change of the relevant healthiness conditions.
Market-Driven Symbolic Execution
of Models of
Manufacturing Enterprises
Time: 15:30 - 16:30
Speaker: Zheng Hongjun - UNU/IIST
Abstract: We apply formal description techniques, in particular RSL to
model, compose and give operational meaning to the class of
reactive systems representing manufacturing enterprises. The
enterprise is a discrete-parts manufacturer which pursues its
business activities to best compete with other such entities,
together comprising a market. It does so by means of resources and
processes that execute concurrently on them, subject to internal
(resource) and external (market) constraints. In some cases the
enterprise is a consumer, in others a supplier of products. Some
modelling techniques are familiar for reactive systems:
shared-memory concurrency, resource-bound synchronous executions,
priorities and scheduling, external and internal choice. Other are
specific to this domain: undetermined (human) choice, transfer of
products during one-to-one (one consumer, one supplier)
synchronisation, marketing decisions and how they affect
many-to-one (one consumer, many suppliers) synchronisation. The
result is a relatively new application of FDTs, as well as a
contribution to the semantics of the emerging discipline of
enterprise engineering.
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: Jifeng He, Oxford 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:
(1) The operational semantics using TA.
(2) A minor extension of the logical semantics using DC, and a proof that this semantics is complete relative to our operational semantics. This means that if an observable satisfies all formulas of the DC semantics, then it can also be generated by the TA semantics.
(3) A proof that the logical semantics is sound relative to our operational semantics. This means that each observable that is accepted by the TA semantics constitutes a model for all formulas of the DC semantics.
10:30 - 11:00: Tea break
Program Theories in Duration Calculus
Time: 11 - 12: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.
Towards a Theory of Sequential Hybrid Programs
Time: 12:00 - 13:00
Speaker: Wang Hanping - UNU/IIST, from Peiking 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.
13:00 - 14:30: Lunch break
Afternoon session, Chair: Hans Rischel, Danish Technical University
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.
Combining Duration Calculus with RAISE
Specification Language
Time: 15:30 - 16:30
Speaker: Xia Yong - UNU/IIST, from East China University
Abstract: RAISE is a product consisting of a development method, an
associated formal specification language (RSL) and a collection of
computer based tools. RAISE has turned out to be useful in the
development of many kinds of software systems. However, RSL has
no " real-time" features, and hence, it is difficult to specify
real-time applications using RSL.
The Duration Calculus (DC) is a formalism which can be used for that. However, DC is "just" a logic, and for practical purposes it would be nice to have a richer language providing modules, facilities for declaring symbols to be used in DC formulas etc.
The goal of our work is two-fold: (1) to extend RSL with real-time features, and (2) to provide a specification language and tools support (e.g. a syntax and type checker, a justification assistant, etc.) for DC.
A first step towards this goal, is to combine DC and RSL achieving the power of both. So far, we have encoded DC in RSL and set up a proof assistant tool, called DC/RJ, to verify (encoded) DC formulas using the RAISE Justification tools. DC/RJ is constructed from encoding of both DC semantics and proof system of Interval Logic & DC.
In our report, we will introduce how DC can be integrated with RSL in detail, and then the construction and hierarchy of DC/RJ are explained. The Gas Burner example is used to show how the assistant works.
Adding time constructors, wait and etc., to RSL will make the new specification language, TRSL, has the power of specifying real-time application. Then the work of finding theoretical foundation for TRSL comes. This is our work of second period. We give an operational semantics to TRSL. What is more, we define pre-order and test equivalence relation to TRSL. We prove the soundness of original proof rules of RSL and our extended rules for TRSL based on our operational semantics. The TRSL development methods are being developed too.
Now, we enter the third period of our work : relate TRSL to DC. We give an "operational semantics with explicit states" to TRSL, and then define some satisfaction relation between TRSL and DC. We will set up a proof system, and prove the soundness with respect to the above operational model. The Gas Burner example will be used again to demonstrate how our proof system apply to an real-time applications.
16:30 - 17:00: Tea break
Fault-Tolerant Composition of Software
from
Verified and Unverified Components
Time: 17:00 - 18:00
Speaker: Tomasz Janowski - UNU/IIST
Abstract: We consider composition of software from coarse-grained
components. A component provides operations to read and write its
internal state. It is: specified by pre- and post-conditions for
write operations in terms of read operations, implemented
combining in various ways operations by sub-components, and proven
correct from specifications of sub-components, under correctness
of their implementations. We relax this assumption by
systematically introducing fault-tolerance into the
implementation: (1) Wrapping: extra layer of design, generated
from sub-component's specification, for detecting run-time errors.
(2) Late binding: requesting any/all sub-component(s) satisfying
given run-time property. (3) Brokering: deciding at run-time which
sub-component satisfies the request. We provide a simple model for
component design and analysis, implement such techniques and
justify fault-tolerance of the result, replacing the assumption
about static correctness of implementations of all sub-components
by non-simultaneousness of their failures at run-time. We also
discuss applications to modern component technology, in particular
CORBA, linking such technology with formal methods.
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
Duration-Constrained Regular Expressions
Time: 12:00 - 13: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.
13:00 - 14:30: Lunch break
Afternoon session, Chair: Burghard von Karger - Kiel University
On Checking Real-Time Systems for
Linear Duration Invariants
Time: 14:30 - 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
A Calculus of Durations On Abstract Domains:
Completeness and
Extensions
Time: 17:00 - 18: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, tow-dimensional duration
calculus and duration calculus for weakly monotonic time [PD97]
Day 4 (Thu, 28 May 1998)
Morning session, Chair: Michael R. Hansen, Danish Technical University
A compositional semantics of SL using the Duration Calculus of
Weakly Monotonic Time
Time: 9:30 - 10:30
Speaker: Dr 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 langauges.
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.
10:30 - 11:00: Tea break
Executable Specification of Concurrent Real-Time
Systems
Time: 11:00 - 12:00
Speaker: Dr 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.
DC/P: A Proof Assistant for Interval Logics
Time: 12:00 - 13:00
Speaker: Hu Chengjun - UNU/IIST, from Chansha 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 Skakkebak's PC/DC.
13:00 - 14:30: Lunch break
Afternoon session, Chair: Jonathan Bowen - The University of Reading
14:30 - 16:30: Discussion about further cooperation
16:30 - 20:30: Macau Tour
Day 5 (Fri, 29 May 1998)
One-day visit to
Zhuhai, China