- Dr. Peter Gorm Larsen, IFAD (Inst. For Applied Datalogy),
Odense, Denmark
Friday, 5-Jan-96
Title: Lessons Learned from Applying
Rigour in Industry
Abstract: At British Aerospace Systems & Equipment
(BASE) an experiment which consisted of the parallel development
of a small security-critical system, was carried out. Within
BASE, two teams of engineers independently developed a
security-critical device called a trusted gateway to the level of
software prototype. One team used the BASE development
methodology, supported by RTM for requirements tracing and
Teamwork for data-flow-based system description; the other team
used the same techniques plus formal specification in the Vienna
Development Method's specification language VDM-SL. Throughout
the development process, we were able to compare the progress of
the two teams in terms of the effort required to complete each
development phase, as well as the characteristics of each of the
design artifacts produced (system specifications, test plans,
etc.). This presentation focus on the lessons learned from this
experiment rather than the actual specifications produced.
- Dr. Peter Gorm Larsen, IFAD (Inst. For Applied Datalogy),
Odense, Denmark
Monday, 8-Jan-96
Title: Towards Proof Rules for the
Full Standard VDM-SL
Abstract: This Presentation provides an
introductionary overview of my PhD work. However, the main focus
of this presentation is on what is considered the most import of
the results reached during this work. This is illustrated by a
small language which combine under-determinedness with recursion.
The model-theoretic and proof-theoretic semantics for this small
language is presented in detail and it is shortly discussed how
this approach could be lifted to be usable for VDM-SL.
- Dr. Peter Gorm Larsen, IFAD (Inst. For Applied Datalogy),
Odense, Denmark
Wenesday, 10-Jan-96
Title: A Short Overview of VDM-SL
Abstract: This presentation will provide a short overview of the VDM-SL
notation and the concepts used in this language. The presentation
will introduce some of the notation such that the attendees can
see the differences to for example RSL. Finally, the structure of
the VDM-SL standard will be identified without going into debt
with the semantic details.
- Dr. Peter Gorm Larsen, IFAD (Inst. For Applied Datalogy),
Odense, Denmark
Friday, 12-Jan-96
Title: The VDM-SL and VDM++
Toolboxes
Abstract: This presentation will be carried out as a
combination of a slides presentation to provide a rough idea about
the functionality provided by the VDM tools developed by IFAD
(these two tools support the VDM-SL and the VDM++ notations).
Afterwards, those who are interested in having a more in-debt
demonstration can see the tools working on a portable computer I
am bringing with me. It will naturally be possible to get such a
demonstration during my entire stay here in Macau.
- Dr. Peter Gorm Larsen, IFAD (Inst. For Applied Datalogy),
Odense, Denmark
Tue, 16-Jan-96
Title: Modeling of Realms in VDM-SL
- From Informal to Formal
Abstract: This presentation will use the
modeling of Realms I have been working on last week to illustrate
how one move from an informal description of a problem to a formal
model. Thus, the presentation will both introduce the notion of
realms, but just as important it will discuss the rationale behind
the design decisions which have been made in the formalisation.
- Prof. Dines Bjørner, Director, UNU/IIST
Tuesday,
23-Jan-96
Title: Models of Business Management: Strategy, Tactics &
Operations -- Case Study Applied to Airlines and Manufacturing
Abstract:
- Professor Kees Middelburg, UNU/IIST Senior Research Fellow
Thursday, 25-Jan-96
Title: A short overview of SDL
Abstract: SDL is a
specification language which is primarily used for software
development in telecommunications. During the presentation, the
concepts used in this language will be explained and illustrated by
excerpts from an SDL specification. Some semantic issues concerning
the language will be introduced and its relationship with Duration
Calculus will be touched upon.
- Prof. Dines Bjørner, Director, UNU/IIST
Thursday,
21-Thursday-96
Title: Decision Support Systems for Sustainable
Development and their relation to Geographic Information Systems
Abstract:
Development is about changing natural and other resources.
Sustainable Development is about maintaining certain Indicators
(Constraints, Objectives) while subject to Development. Decisions
is about selecting among alternative Development Analysis, Planning
and Execution choices. We analyse therefore, the notion of DSS for
SD. Then we suggest a Federated GIS "Shell" being accessed by the
DSS for SD, and show the relations between the two otherwise
independent notions. The Seminar thus illustrates the use of Domain
Analysis to rather novel concepts.
- Dr. Paul Curzon from the University of Cambridge
Laboratory
Monday, 25 March, 1996
Title: Overcoming the Practical
Problems of Formal Hardware Verification
Abstract: Machine-assisted proof
has the potential to give stronger verification results than
traditional methods such as testing. However, machine-assisted
proof has so far not achieved widespread industrial use. This is
partly because it is perceived as a difficult and time-consuming
process. We describe our work using the HOL theorem proving system
to verify real communications hardware: the Fairisle switching
fabrics used in ATM switches. In particular, we reflect on the
practical problems encountered and the bottlenecks that slowed the
progress of the proofs. We suggest how some of these problems might
be overcome.
- Dr. Tomasz Janowski, UNU/IIST Research Fellow
Thursday, 28
March, 1996
Title: Dynamic Scheduling in the Presence of Faults:
Specification and Verification
Abstract: For a distributed real-time
program, executed on a limited set of hardware resources and
required to satisfy timing constraints, despite anticipated
hardware failures, to statically determine the task execution order
is often infeasible. The talk will show how to formally reason
about these programs when scheduling decisions are made on-line and
take into account deadlines, load and hardware failures. I will use
Timed CCS as a process- and resource-description language, define a
language to describe anticipated faults and apply a version of a
mu-calculus to specify and verify timing properties. This allows
the property of schedulability to be the outcome of an
equation-solving problem. And unlike conventional reasoning, the
logic is fault-monotonic: if correctness is proved for a number of
faults, correctness for any subset of these faults is guaranteed.
- Myatav Erdenechimeg, UNU/IIST fellow, from Electronics and
Software Department of National University of Mongolia
Thursday
4th April, 1996
Title: Multi-lingual Script Processing
Abstract: Many
information systems require support for pieces of text in different
languages. Although a wide range of systems providing such support
is available, most of these impose the restriction that the text
must be written in the standard European style (left to right and
top to bottom). We report on a thorough analysis of multi-lingual
documents, based on which we develop a model of text in which
different languages can be mixed while retaining their traditional
writing style. We also discuss the requirements for a tool which
could produce such text using text generated by different existing
tools as its input.
- Dr. Rogerio de Lemos, New Castle Upon Tyne University,
UK
Friday 3rd May, 1996
Title: Extended RTL in the Specification and
Verification of an Industrial Press
Abstract: Extended Real Time Logic
(ERTL) is proposed for the modelling and analysis of hybrid
systems, taking as a basis Real Time Logic (RTL). RTL is a first
order logic with uninterpreted predicates which relate events of a
system to the time of their occurrence, thereby providing the means
for reasoning about absolute timing properties of real-time
systems. The extensions provided by ERTL allow reasoning about
system behaviour in both value and time domains through predicates
defined in terms of system variables. We illustrate the use of
ERTL through the modelling and analysis of an industrial press.
- Paritosh K. Pandya,
TIFR, Bombay, India
Thursday, 9th May, 1996
Title: A Logical Semantics
of ESTEREL
Abstract: ESTEREL is a novel programming notation for writing
reactive programs. It is based on the true synchrony
hypothesis which allows complex patterns of reaction to input to
be encoded using sophisticated control structures such as
concurrency, preemption and suspension. ESTEREL is supported by a
comprehensive set of tools and it has found use in the design of
some large and sophisticated safety critical systems.
In this talk, we will explain the programming notation ESTEREL
using the language of Mean-Value Calculus.
- Dr. Xu Qiwen, UNU/IIST Research Fellow
Thu, 16th May, 1996
Title: Semantics and Verification of the Extended Phase Transition Systems
in the Duration Calculus
Abstract: A hybrid system is usually modelled by
piecewise continuous functions. The system evolves continuously when
the control laws are fixed. Discrete changes occur when control
laws are switched. Usually, discrete actions are considered atomic.
To support the design of discrete controllers, we need to refine
discrete actions into programs which not only are non-atomic but
also may contain some forms of iterations. We extend Manna &
Pnueli's phase transition systems with notations for programming.
The semantics of the new phase transition system is given by mapping
to a variant of the Duration Calculus, a real-time logic based on
the Interval Temporal Logic. We embed program logics into the
Duration Calculus and this facilitates effective reasoning of the
system.
- Mao Xiao Guang, UNU/IIST Fellow, from Changsha, China
Thursday,
6 June, 1996
Title: A Proof Assistant for Interval Logics
Abstract: I have built a
proof assistant for Interval Logics, including Neighbourhood Logic,
Interval Temporal Logic and Mean Value Calculus of Durations. This
seminar will give a brief introduction to the semantic encoding of
those logics in PVS, and how to transfer from one to the other.
- Dr. Venkat P. Reddy, UNU/IIST fellow, from India
Thursday, 13
June 1996
Title: Constraint tableau system for integer time tense logic
Abstract:
We present a tableau system for a propositional tense logic with
time structure Z. The notion of codesignation is used to deal with
temporal information, and is alternative to unification.
Codesignation is defined in terms of arithmetic cheques.
- Dr. Liu Zhiming, from the Leicester University, UK
Fri, 21 Jun
1996
Title: Verification of Fault-Tolerance and Real-Time
Abstract: A
transformational method is given for specifying and verifying
fault-tolerant real-time programs. Such a program needs to be
provably correct according to its both functional and real-time
requirements, despite of the presence of possible system failures.
The paper demonstrates that a suitably expressive logic for
real-time systems allows to naturally model the state changes by
system failures and determine their effect on the functional and
real-time properties of executions.
- Dr. Venkat P. Reddy, UNU/IIST fellow, from India
Thursday, 27
June 1996
Title: Machine versus human computation
Abstract: In this talk I present
a simple model of machine computation, and then present a model of
human computation, which is indeed a generalisation of the former
one. To point out what machines find hard to imitate in human
thinking, I present how the human computation model explains in a
simple way cognitive tasks such as perception, understanding,
learning, reasoning, discovery, etc. Ultimately, I would also
address a philosophical issue: the ontological position of
knowledge, and an answer to it.
- Paritosh K. Pandya, UNU/IIST Visitor, TIFR, Bombay,
India
Thursday 25 July 1996
Title: A Duration Calculus of Weakly
Monotonic Time
Abstract: Some models of real-time computation assume that
time has a fine structure which allows a sequence of state changes
to occur at the same (macro) time point. Such a notion of time is
called weakly monotonic.
In this talk we will present a duration calculus of weakly monotonic
time. The resulting logic allows features such as true synchrony
and digitisation to be formalised. As an example of this, we will
present a semantics of Timed CSP assuming the true synchrony
hypothesis.
- Dr. Yong Sun, UNU/IIST Visitor, Department of Computer
Science, The Queen's University of Belfast, Northern Ireland
Wed,
14th August 1996
Title: SOFL: Formal Engineering Method for Industrial
Applications
Abstract: There is a strong challenge to formal methods that
they cannot be easily and widely adopted in industry. A major
reason for this is that they are difficult to use and their
application consumes prohibitive amounts of resource. Much
research on the integration of available formal methods (e.g. Z,
VDM, B-method) and either Structured Methodology or
Object-Oriented Methodology has been conducted to make formal
methods more practical, but its success has been very limited.
However, no effort has been made to integrate properly formal
methods, structured methodologies and object-oriented
methodologies to take advantage of the desirable features of the
three approaches.
As one approach to the solution of these problems, we propose a
language called SOFL (Structured Object-oriented Formal Language)
for system development. It supports the concept that a system can
be constructed using the structured methodology in the early
stages of its development, and by using object-oriented
methodology at later, more detailed levels. During the complete
system development process, formal methods are applied in a manner
that best uses their capabilities. SOFL integrates Structured
Methodology based on extended data flow diagrams, Object-Oriented
Methodology (e.g. classes and inheritance), VDM-SL, and Petri
nets.
Our research is an international collaboration between Hiroshima
City University (Japan), The Queen's University of Belfast
(Northern Ireland), George Mason University (USA), and Queensland
University of Technology (Australia). It is financially supported
by Japanese Education Ministry, Hiroshima City University, and The
Queen's University of Belfast.
- Mr. Glenn Evans, UNU/IIST Visitor, Department of Computer
Science, The Queen's University of Belfast, Northern Ireland
Wed,
14th August 1996
Title: Demo of GUI for SOFL
Abstract: A SOFL specification
contains both visual and textual information, namely the CDFDs and
the SOFL text. It is clear that these pieces of information are
largely, but not completely, isomorphic. So, whilst it was
necessary to provide both a visual and textual editor in the GUI for
SOFL, it was also possible for both of these editors to manipulate
the same abstract data structure. There will be a discussion of the
early stages of the creation of the GUI, a demonstration of it's
functionality and an example system will be specified to demonstrate
the ease of use of both SOFL and the GUI.
- Dr. Henrik Esbensen, UNU/IIST Visitor, Department of Electrical
Engineering and Computer Sciences University of California, Berkeley
U.S.A.
Thursday 8th August, 1996
Title: Explorer: An Interactive
Floorplanner for Design Space Exploration
Abstract: Traditional
floorplanning/placement approaches combines the cost criteria
considered using relative weights and/or bounds and generates a
single compromise solution. However, in practice it may be very
difficult or even impossible to define the weights and/or bounds
such that the output solution represents a satisfactory compromise
of the cost dimensions. Explorer is an interactive floorplanner
aiming at eliminating this fundamental problem. It is based on the
GENETIC ALGORITHM and optimizes layout area, aspect ratio, maximum
path delay and routing congestion simultaneously. Explicit design
space exploration is performed by using a vector-valued,
4-dimensional cost function and searching for a set of distinct
solutions representing the best tradeoffs of the cost dimensions.
From the output solution set, the designer can ultimately select the
preferred solution. In contrast to existing approaches, neither
weights nor bounds are needed. Instead, the design requirements are
refined interactively as knowledge of the obtainable tradeoffs is
gained. Experimental results illustrates the unique features of
this approach.
- Prof Chen ZongJi, UNU/IIST Visitor, BUAA, PRC
Thursday 15 Aug,
96
Title: Fault Tolerant Control System
Abstract: This seminar discusses the
following problems:
- The concept of fault tolerant control system and an introduction
to a quadratic redundant flight control system.
- A fault tolerant control system can be abstracted as
a hybrid system.
- Equivalent discrete event model of time evolving
subsystem of a hybrid system.
- Simulation (modeling and verification) of fault
tolerent control systems is necessary.
- A formal method to design the decision maker (redundancy
management) is needed.
- Prof Yuan Chongyi, UNU/IIST Visitor, Dept. of CS, Peking
University, PRC
Thursday, 22 Aug, 96
Title: Petri nets: theory and
applications --an introduction
Abstract: "Petri Nets" is known for its
power in expressing concurrency and its graphical presentation. But
in essense, its theory is by far more important. General Net Theory
(GNT for short) consists of 4 main branches, namely CONCURRENCY,
SYNCHRONY, ENLOGY and NET TOP- OLOGY. It's fair to that a successful
net application is impossible without the guidance of GNT.
This talk presents the basics of Petri Nets. With two application
examples, the role played by GNT is touched.
Example 1: The Puzzled Prisoner
Example 2: From data dependence to data independence.
- Dr. Dao Nam Anh, UNU/IIST Fellow, from Vietnam
Airlines
Thursday, 5 Sep, 1996
Title: Formal Modelling of Large Domains
Abstract:
In the literature, there are many examples illustrating the use of
domain analysis for modelling software systems in the initial stages
of their development. The case studies chosen are, however, often
of small systems or of small parts of large systems.
In this paper we show that the techniques can be as readily applied
to very large domains and how a manageable formal model of the
domain can be obtained by abstracting appropriately. We illustrate
this with a case study based on the airline business domain. We also
discuss how this formal model can be developed towards software
support systems for the airline industry which capture a wide range
of different requirements, and how it might be applied more
generally.
- Prof. Dr. Vladyslaw m. Turski, UNU/IIST Visitor, from Institute
of Informatics, Warsaw University, Poland
14:30, Tue, 10 Sep 1996
Title: Behavioural specifications
Abstract: Many computer applications (from
operating systems to text editors to on-line control systems) do not
compute any "final results", although they include many "local"
computations. The purpose of specification of such applications is
to prescribe certain desirable behaviour of a system visible to the
user. The presentation will introduce a novel way for writing such
specifications, describe some applications and show a way of
simulation of specified behaviour directly from the specification
- Prof. Dr. Vladyslaw m. Turski, UNU/IIST Visitor, from Institute
of Informatics, Warsaw University, Poland
14:30, Tue, 17 Sep, 1996
Title: If
software is so bad why does it sell so well?
Abstract: This presentation,
aimed at a more general audience, will explore some current myths
about software quality and contest the notion of software crisis.
The presentation will be based on previous lectures by Prof. Tony
Hoare and the Author, as well as on the Panel Discussion organized
and chaired by the Author at the ICSE 18 in Berlin, March 1996.
- Prof. Dr. Vladyslaw m. Turski, UNU/IIST Visitor, from Institute
of Informatics, Warsaw University, Poland
14:30, Wed, 18 Sep, 1996
Title: Where
to from here?
Abstract: Based on personal experience of 30 years active
involvement in computing, computing research and computing science
education, the presentation will consider the possible future
pattern of informatics evolution and the steps that could be taken
by academic/research community to best prepare for the challenges
and demands of the next decades.
- Prof. Dr. Vladyslaw m. Turski, UNU/IIST Visitor, from Institute
of Informatics, Warsaw University, Poland
16:30-17:30 every day during 9-13, 16-20 Sep,1996
Title: A general view of software development
Abstract: The goal of this presentation
is to provide an overview of a model software product development
based on sound logical foundations (Turski/Maibaum) and on the
iterated stepwise refinement approach (Lehman/Stenning/Turski).
Although the presentation will be expressed mostly in theoretical
terms, it requires but a rudimentary previousknowledge of formal
logic, and will provide direct hints at practical applications,
especially in organizing the software production process.
- Prof Tang ChiSong, Software Institute, Academia Sinica,
PRC
Thursday 19 Sept 96
Title: XYZ System and its Application
Abstract: XYZ
System consists of a temporal logic language XYZ/E as its kernel and
a toolkit. The basic characteristic of this TLL is its ability to
represent the dynamic semantics of the declarative specification
with a uniform formal framefork. As the result, it can serve as a
common basis for the entire software development process and make
the transition of the evolution steps smoothing on this unified
formal basis. Furthermore, some hard problems in formalization
become softer in this framework.
- Tomasz Janowski, UNU/IIST research fellow, (joint with Wojciech
Mostowski, UNU/IIST fellow, from Poland)
Thursday 3-Oct-96
Title: Towards
Semantically-Secured Interoperability: On-Line Model-Checking
Abstract: We
look at the problem of integrating heterogeneous applications:
written in different languages, running on incompatible machines,
using protocols that cannot talk to each other .. We look at how the
problems created in this environment are tackled within increasingly
accepted Common Object Request Broker Architecture (CORBA) and how
the new problems arise due to the lack of any semantic constraints
in the CORBA's (and any other we know) Interface Definition Language
(IDL).
A possible solution is to extend the IDL descriptions by axioms of
two kinds: representing the effects of one-step invocations of
interface functions (as equations) and representing the properties
that need to hold between the invocations (as modal properties). We
see the promise of using the first for formal verification
(off-line) and the second for `safety' checks (on-line), useful for
legacy systems and done by the generated, as part of the IDL
translation, model-checking engine. The talk will report on the
very initial stages in the implementation (metaphorically and
literally) of this idea: how to link equational specifications with
modal logics, via transition systems, and how to handle complexity
of the resulting descriptions.
- Prof. Yakup Paker, UNU/IIST visitor, Department of CS, Queen
Marry and Westfield College, University of London
Thu,
17-Oct-1996
Title: Parallel Computing for Advanced Multi-Media
Applications
Abstract: Recent multi-media workstations and networks are
capable of handling complex information like sound and video, making
it practical to implement applications like CSCW and
video-conferencing. However, the requirements of hight quality
images for broadcasting and some of the advanced applications like
Virtual Studios, tele-presence and Virtual Reality require much more
powerful facilities than is available today. Parallel processing
offers a scalable solution in order to meet the stringent real-time
requirements.
The ML-PVA (Mona Lisa - Parallel Video Accelerator) machine has been
developed to handle TV quality video streams in real-time. The
architecture of the ML-PVA and the software environment called
"Self Adaptive Parallel Servers" will be presented.
- Tomasz Janowski, UNUIIST Research Fellow, and Rumel V. Atienza,
UNU/IIST Fellow from De La Sale University, The Philipines
Mon,
30-Dec-96
Title: A Formal Model For Competing Enterprises, Applied to
Marketing Decision-Making
Abstract: Marketing models have long been used by
enterprises to predict and optimise the effects of their
decision-making, relative to their competitors. Recently, enterprise
models are also being used, aiming at `improved' coordination within
an enterprise. The talk will present a combination of both models,
that is, a model for enterprises competing in a one-product market,
and show its use for marketing decision-making. The model is built
in stages: market without marketing, marketing without limits (four
Ps: product, price, place and promotion) and marketing under limited
resources (four Ms: man, machines, materials and money). Before we
apply the model we justify abstraction, down to considering two
virtual enterprises (competing against us and cooperating with us)
competing for a virtual consumer. Then we capture the search for
the optimal marketing mix (four Ps) under given constraints (four
Ms) as the standard optimisation problem and apply the simplex
algorithm to show a generic solution. For the formal notation we use
RSL, the RAISE Specification Language.
