- Tsend Ganbat, UNU/IIST fellow, from the Software Engineering
Department, Institute of Computer Science and Management,
Mongolian Technical University of Ulaanbaatar, Mongolia
Friday,
9 Jan 1998
Title: Specifications of Public Service Systems: Four Case
Studies for Use in Lecture Courses on RAISE
Abstract: Four example RSL
specifications have been developed for use as case studies in
courses on RAISE. All four examples are built around the general
idea of a "Public Service System". The first three deal with
specific examples of public service systems: a supermarket, a petrol
station, and a bank. Each is self-contained, and so is suitable to
be used individually, for example on a short course. The fourth
example deals with a general public service system which
incorporates all the features of the first three examples. This is
primarily intended to be used together with the specific examples as
an extended case study on longer courses.
- Yun Xiaochun, UNU/IIST fellow, from Harbin Institute of
Technology, Harbin, PRC
Friday 23 Jan
1998
Title: Fault-Tolerance and Semantics of Software Built from Pre-Existing Components
Abstract: Design from pre-existing components becomes a de-facto practice of
software development. While it saves on time and the cost of design,
it also creates an uncertainty about the meaning of composition from
in principle unknown components, which uncertainty tends to accumulate
with each level of reuse. In this talk we present some engineering
methods to achieve reliable composition from unreliable components:
- Wrapping: extra layer of design, generated from the component's
specification, for the purpose of detecting errors at run-time.
- Dynamic invocation: instead of requesting a concrete component,
request any one satisfying given run-time property.
- Run-time mediation: deciding by broker which of the components
satisfying the request should ultimately be used.
We also address briefly the problem of interference under sharing of
components. Such run-time methods may be used when static analysis is
impossible, e.g. the implementation is not available for inspection,
or may complement verification. Applications open up for modern
component technology like e.g. distributed object computing by CORBA,
linking them with formal methods. Part of the presentation is
informal, part is formal model in RSL.
- Marcel Fouda, UNU/IIST Fellow
Tuesday, 17th February
1998
Title: Formal Modelling of Spatial Information Systems. A Case Study:
Water Resources Management
Abstract: We present an experiment in modelling and analysis of an application domain:
Water Resources Management. The resulting model, which is specified
formally in the RAISE specification language RSL, captures the typical
functionality and structure of such domains, including the
representation of data at different levels of abstraction, as well as
their intrinsic properties: incomplete data, heterogeneousness,
federation of platforms, etc. It is in fact sufficiently abstract to
describe not just water resources management systems but very general
spatial information systems.
- Tran Manh Thang and Nguyen Hong Viet, UNU/IIST Fellows, from
Vietnam Airlines
Friday 20th February 1998
Title: Flight Effectiveness Analysis in Airline Business: A Formal Model
Abstract: Flight effectiveness analysis is a process employed by airline
companies to assess, and hopefully improve, the effectiveness and the
profitability of their flight operations. Essentially, it involves
the study and comparison of various aspects of data about flights (the
passengers and cargo carried, the aircraft used, the cost involved,
the revenue obtained, etc.), from which decisions about changes to the
flight operations are derived.
In this talk we describe the essential aspects of flight
effectiveness analysis (FEA), in particular the data that it requires
and how this is used to generate IATA standard reports on FEA. The
first part of the talk gives an informal description of FEA. The
second part gives a formal specification of this using the RAISE
specification language, RSL.
- Prof. Chen Nengkuan, Academican of Chinese Academy of Sciences
Vice Director, Division of Technical Sciences, CAS
Monday, 23 Feb
1998
Title: Science, Technology and China's Sustainable Development
Abstract: Since the 1992 United Nations Conference on Environment &
Development , the principle of sustainable development has become
the consensus of opinion of the people and governments all over the
world. In November 1997, another important meeting, the 1997 China
Environment Forum held in Beijing. Many delegates came from within
China and abroad to discuss issues of environmental sustainablity in
general and how to cope with China's environmental problems in
particular. Opinions from this forum were highly regarded by the
Chinese government. Now China as a developing and most populous
country in the world is facing the urgent tasks of developing its
economy, protecting environment and raising its people's standard of
living. We are speeding up to develop our economy. Meanwhile we must
stick to our national fundamental policy to protect the ecological
environment. The strategy of sustainable development is therefore
considered as a fundamental principle to guide the China's
all-around social and economical developments.
In this talk three problems will be addressed. First the
characteristics of China with respect to her sustainable
development. Secondly, modern science & technology serve as the
dynamic driving force for China's sustainability. Thirdly, how
Chinese scientists react to the importance of China's ustainability.
- Dr. Jian Zhang, UNU/IST Visitor, from the Software Institute,
Chinese Academy of Sciences
Mon 9 March 1998
Title: Satisfying Logical
Formulas
Abstract: Many problems can be regarded as satisfying a set of
logical formulas. For the propositional logic, the SAT problem is a
well-known NP-hard one. The satisfiability problem in the
first-order logic is undecidable in general. In this talk, I will
describe techniques and tools for satisfying first-order formulas in
small finite domains, and compare them with other related
approaches. I will also breifly mention their applications, with
emphasis on program verification and testing (e.g., generating test
cases, refuting conjectures).
- Pablo Giambiagi, UNU/IIST fellow, from University of Buenos Aires
10:00, Thu 12 Mar 1998
Title: Semantics and Proof Rules for Timed Automata
Abstract:
During the last few years, automata theoretic formalisms have been
successfully applied to the specification of reactive systems first, and
real-time systems, later. They have also proved quite useful for the
automatic verification of system properties written in some temporal
logics.
Whereas Duration Calculus was introduced to specify and reason about
embedded real-time systems and has been used to reason about circuits,
digital designs, hybrid systems, etc., this logic takes a continuous and
global view of the system that does not match the usual synchrony
assumptions present in most automata formalisms. However, with the
introduction of super-dense time models, extensions of DC can now
accommodate for these assumptions and we show here how WDCI -Duration
Calculus of Weakly-monotonic time and Infinite intervals-, can be used
to give semantics to Timed Automata, one of such formalisms. This
prepares the field for importing into DC many results on the deductive
verification of temporal formulas and system implementation, which we
illustrate by coding, in WDCI, rules for proving invariance and
refinement (in the sense of timed language inclusion). We also prove
their soundness in the extended calculus.
This work is currently underway in collaboration with Xu Qiwen and
Gerardo Schneider.
- Dr R. Ramanujam, UNU/IIST visitor, from the Institute of Mathematical
Sciences, Chennai, India
10:00, Mon 16 Mar 1998
Title: An automata theoretic account of
the assumption - commitment framework
Abstract: A distributed presentation
of a regular language L is a system of communicating automata
accepting L, where the constraint on distribution is given in the
form of a distributed alphabet. We study such presentations in the
assumption - commitment framework, where each process makes
assumptions about other processes in the system. Symmetrically, each
process makes commitments which the other processes can rely on. We
show that every regular language can be thus decomposed and
present a version of Kleene's theorem using top-level parallelism.
By imposing constraints on the assumption structure, we get
different subclasses of regular languages. The work presented is
joint with Swarup Mohalik.
- Dr R. Ramanujam, UNU/IIST visitor, from the Institute of Mathematical
Sciences, Chennai, India
10:00, Tue 17 Mar 1998
Title: Model checking temporal properties
Abstract: Automata theoretic methods have proved extensively useful
in the context of model checking in temporal logics, where we are given
a finite program or state transition system and a formula of temporal
logic, and asked whether every behaviour of the system satisfies the
formula. In recent years, so-called partial order methods have proved
useful in model checking, whereby we can exploit locality or concurrency
information in speeding up verification. We present the basics of this
approach, discuss the problems involved, and briefly highlight some of
our work in this context.
- Prof. To-yat Cheung, UNU/IIST visitor, from Department of Computer
Science, City University of Hong Kong, Hong Kong
15:00 Tue 17 Mar
1998
Title: Some current development in Petri nets for system
verification
Abstract: This talk starts by reviewing the capability of Petri
nets as a model for the specification, verification and testing of
software systems. Discussion will be based on four issues: 1)
Variations in capability for specification. 2) Availability of
methodology for verification and testing. 3) Relationships with
other models frequently used for protocol investigation, such as
SDL, ESTELLE, LOTOS, CCS, CSP and CCSP. 4) Current extensions of
Petri nets for the study of object-oriented systems. The second
part of the talk concentrates on three kinds o f property-preserving
transformations on basic Petri nets for system design. The first
kind preserves liveness; the second kind preserves invariants; and
the third kind preserves inheritance in object-oriented software.
Extension to coloured Petri nets and application to feature
interactions will be briefly described.
Speaker: To-yat Cheung got his PhD in Computer Science from the
University of Wisconsin, USA. He had been with many industrial firms
and the University of Ottawa in USA and Canada before returning to
Hong Kong in 1995. Currently, he is the Professor of Computer Science
Department, City University of Hong Kong. His current research
interest is in databases and distributed computing, especially in
he use of formal methods for the specification, verification and
testing of distributed and object-based software.
- Professor Martti Tienari, UNU/IIST Visitor, from
Department of Computer Science,
University of Helsinki
10:00, Wed, 1 April 1998
Title: Behavioural
Equivalences in the Verification of Concurrent Systems
Abstract: Labeled transition systems form a well-established formal model of
concurrent systems. Many formal specification languages (e.g. CSP,
CCS, and LOTOS) can be provided with semantics expressed in terms of
transition systems. Behavioural equivalences between transition systems
can be used widely in the verification of concurrent systems.
The lecture gives an introduction to process equivalence concepts
and shows with application examples their utility in the verification
of some simple class-room size examples of concurrency. Minimization
of labeled transition systems with respect to behavioral equivalences
is a current research area at the University of Helsinki. Recent research
results achieved in this area are surveyed.
- Prof Gerard Huet, UNU/IIST visitor, from
INRIA, Rocquencourt, France
Friday, 10 April 1998
Title: Prooflets: A general paradigm for self-certifiable mobile code
and its implementation in the Coq Proof Assistant
Abstract: The Paradigm of mobile code is gaining wide applicability with the
development of Java and its variants. However, unchecked execution of
possibly hostile mobile code is clearly problematic for security
reasons. Type-checking and other static analysis may reveal some
unsafe programs, but such techniques are not sufficient to guarantee
that a piece of code will respect some security policy, or will
achieve its intended aim. Using authentication protocols based on
cryptography is the only practical solution to this problem today, but
this limits significantly the distribution model and it suffers from
export restrictions and national regulations concerning encryption
technology.
Another paradigm is to send not just the executable code, but a proof
of its safety specifications as well. This proof may be checked at
reception, prior to execution of the code. Variants of this general
scheme may generate the program from the proof, or conversely generate
the proof from an appropriately annotated version of the program. This
general methodology is simple to understand, but not easy to implement
in a feasible manner. One needs to agree on a format for such
"proof carrying code", the proof assistant where the proof has been
developed must be able to represent it as a formal object of
manageable size, the client must be equipped with a trustable proof
checker efficient enough for on-the-fly verification, the problem of
incremental proof libraries must be dealt with, the whole scheme must
be consistent with version management of the proof assistants, etc. We
shall describe in this talk an implementation of this paradigm in the
Coq proof assistant, and provide experimental measurements showing
its practical feasibility.
This talk describes joint research with Ajay Chander, from ITT Delhi.
- Xia Yong, UNU/IIST fellow, from East China University of Science
and Technology, PRC
15:00 Mon, 13 Apr 1998
Title: Operational Semantics
of TRSL
Abstract: The reliability of software is an increasingly important demand,
especially for safety critical system. RAISE is a mathematically based
method which has shown to be useful in the industrial development
of many kinds of software systems. However, RAISE has no features for
specifying real-time requirements, which often occur in safety critical
systems.
Adding time constructors, wait and etc., to RAISE will make
the new specification language, Timed RAISE Specification Language
(TRSL),
has the power of specifying real-time application. Then the work of
finding
theoretical foundation for TRSL comes.
In this report, Operational Semantics of TRSL will be first introduced.
Then we will define pre-order and test equivalence relation to TRSL.
Proof rules of TRSL will be briefly reviewed, and then their soundness
corresponding to our operational model will be explained.
At last we will prove the consistency between TRSL and originaly RSL.
Future works on relating TRSL with DC will be shortly discussed after
the report,
for the speaker would like to have more instructions/comments to proceed
the
next work.
- Kathleen Steinhöfel, UNU/IIST visitor, from GMD FIRST, Rudower Chaussee 5, 12489
Berlin
11:00, Wed 22 April 1998
Title: Two Simulated Annealing-Based Heuristics for the
Job Shop Scheduling Problem
Abstract: The job shop scheduling is among the hardest combinatorial
optimization problems. For the classical, general problem setting,
where the objective is to minimize the makespan two simulated
annealing-based heuristics are presented. The problem is defined
for a set of jobs and a set of machines. Each machine can handle
at most one job at a time and each job consists of a chain of
tasks. Each task needs to be processed during an uninterrupted time
period of a given length on a given machine. A schedule is an
allocation of the tasks to time intervals on the machines. The
underlying neighborhood relation of the heuristics involves a
non-uniform generation probability, as opposed to the commonly used
uniform generation probability. To obtain the neighbors of a schedule
the order of tasks on a single machine is rearranged and a control on
the increase of the makespan is performed. The selection of the tasks
depends on structural properties of the actual schedule. Two cooling
schedules have been designed which employ a detailed analysis of the
objective function.
Both heuristics have been implemented and tested on small to
large benchmark problems. The computational experiments have shown
that within short series of consecutive trials relatively stable
results equal or close to optimal solutions are repeatedly obtained.
This is a joint work with A. Albrecht and
C.K. Wong from The Chinese University of Hong Kong
- Dr Sun Yong, UNU/IIST Visitor, from the Department of Computer
Science, The Queen's University of Belfast, Northern Ireland
15:00,
Wed 29 April 1998
Title: A Case Study in Non-monotonic Reasoning: an
Alternative Analysis of the Yale Shooting Problem
Abstract: Non-monotonic
reasoning is often used in daily life, e.g. lacking evidence to the
contrary of B we infer B. This kind of logic has its application in
queries to knowledge bases, very large databases and deductive
bases. This case study uses the "Yale Shooting" problem to present
non-monotonic reasoning from a proof-theoretic standpoint. Basic
knowledge of first order logic and many-sorted algebras is assumed.
This talk will be based on the author's paper appearing in the
journal of Informatica, Vol. 21, No. 2, pp.249-254, 1997
- Prof Zhang Naixiao, UNU/IIST Visitor, from Beijing University, PRC
10:00, Thusday, 14 May 1998
Title: Garment - A mechanism for
abstraction and encapsulation of languages
Abstract: Domain_specific
languages are closely related to interface languages of
domain_oriented software. Thus, the specifications of such software
can be abstracted to specifications of language systems, and
implementation of such sotware can be abstracted to implementation
of the language systems. As a unified model to support software
development and research, a mechanism named Garment for abstructing
and encapsulating languages is proposed. Garment provides a unified
framework for defining languages and describing relations between
languages. Finally, an experimental environment, which supports
software development with Garment, is introduced briefly.
- Gustavo Lugo, UNU/IIST Fellow, from CPGEI/Federal Centre for
Technological Education of Paraná State, Brazil
15:00, Friday, 15 May 1998
Title: Enterprise Modelling and Formal Methods
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. They
are used to better represent and understand how the enterprise works,
to capitalise acquired knowledge and know-how, to support management
decisions and management of change, 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 to demonstrate how formal methods can be applied
to enterprise modelling, providing notations, methods and tools to
treat the enterprise as an engineering artifact. We examine in
particular how to describe an enterprise at different levels of
abstraction (one is a specification, the second an implementation),
how to relate such descriptions formally, how to define an
implementation from components which are themselves enterprises etc.
This is an overview talk. We carry out a sequence of examples to
illustrate the issues involved, all related to marketing and
manufacturing (one-product market, discrete parts assembly), and using
the formal notation of RAISE.
- Professor John Mylopoulos, UNU/IIST Visitor, from the University of
Toronto
11:00, Wednesday, 20 May 1998
Title: Modeling Organizations for Business
Process Analysis and Design
Abstract: We argue that the analysis and design of organizations demands
an understanding of organizational intentions and objectives. For instance,
in the area of claims processing, insurance companies might ask questions
such as:
- Why does it take so long to have a claim settled after an
automobile accident?
- Why does the company hire appraisers to assess damages?
- How else can claims be settled?
- What other concerns would arise if these new ways of handling
claims were to be adopted?
Traditional modeling techniques, such as structured analysis, data flow
diagrams and entity-relationship modelling focus on the modelling of
activities and entities. While these are important concepts for systems
analysis, they offer little help in the search for innovative
alternative solutions to business problems. More generally, existing models
have been designed for describing "what" a business process is like, but
they cannot express "why" the process is the way it is. The motivations,
intents and rationales behind the activities and entities are missing from
these models.
In response to this challenge, we propose a new set of concepts for
capturing organizational intentions. The concepts are described and their
power is illustrated through an example. In addition, we discuss a toolset
under development to be used for the modelling and analysis of alternative
organizational structures and business processes. The work reported in the
presentation has been conducted in collaboration with Eric Yu (University
of Toronto), and Yves Lesperance (York University).
- N. Sathya Prakash and D.H.S. Sarma, UNU/IIST fellows, from
Hyderabad, India
Friday 22 May 11am
Title: Port Management
Abstract: The basic idea of a cargo port is simple: cargo is moved
from ship to shore or vice versa. But the detailed monitoring and
control of this is complicated. As well as ships and cargo there are
many port facilities involved: anchorages, channels, pilots,
tugs, lighters, berths, storage, cranes, trucks, ... Reliable and
up-to-date information is essential if the port is to be managed
efficiently.
The Port Management project started last September and the first phase
is almost completed. In this presentation we describe how the
problems of such a system were tackled, what we achieved and what we
learned.
- Dr. Paritosh K. Pandya, UNU/IIST visitor, from TIFR Mumbai,
India
15:00, Monday, 22 June 1998
Title: Duration Calculus of Timed State
Sequences
Abstract: The notion of timed state sequences has found a
widespread use for modelling behaviour of timed systems. In this
talk, we will present a variant of Duration Calculus, called
DC(TSS), which can be interpreted over the timed state sequences. A
decidable subset of DC(TSS), called NDC(TSS), will be identified.
Many of the existing case studies in DC literature can be captured
within this subset. Application of the decidability result on model
cheching will be discussed.
- Dr. Hrushikesha Mohanty, UNU/IIST fellow, from Department of Computer
and Information Sciences, Central university of Hyderabad,
Hyderabad, India
10:00, Thursday 30 July 1998
Title: Specifying a Communication Protocol And Composing
Transaction Schedules For A Mobile Environment
Abstract: We have seen computer networks with static configuration in the sense
that when ever there is a dislocation of a computer in such a network,
connectivity in it is lost. At the advent of wireless communications one
can manage to retain network connectivity in spite of change of location
of a computer. Such an environment is called a mobile computing
environment where a person can move with his computer keeping its
connection to the network
intact. Though wireless communication provides seamless connection still
there are some disadvantages with it. There are two main limitations
that exist in a mobile environment. One is, due to limited
battery power supply, a mobile computer may like to switch off thus
causing a temporary disconnection. The other one is tracing of a mobile
environment. We will discuss these two features subsequently in the
section describing mobile computing model. Transaction processing
processing needs to be studied in this
environment as the environment is different from the usual computer
networking model. There have been some studies on transaction
processing in mobile environment. However, we have not seen any work on
formal specifications of transactions taking mobile environment
characteristics into considerations. Here we plan to study the uses of
formal methods for the purpose. In particular, we investigate usability
of RAISE for the purpose.
- Toshiyuki Tanaka, UNU/IIST fellow, from Kyushu University, Japan
10:30, Thursday 30 July 1998
Title: Proving Properties of a Security Protocol Specified in RSL
Abstract: With the birth of a secure application system like electronic commerce
over an insecure network such as the Internet, the security of
communication between computers becomes a critical issue. To
establish secure connections between computers, security protocols are
used. In designing a security protocol, one of most important
problems is how to guarantee security properties of the protocol. It
should be also justified that the protocol is secure against attacks.
The aims of this study are to model communication systems over the
network with attacks and to provide formal specification and
verification techniques for security protocols.
We select one security protocol which is called the Secure Sockets
Layer (SSL) Protocol as a case study. The SSL Protocol uses a simple
handshake protocol to establish a secure connection between
principals. The SSL Protocol document provides informal specification
of the protocol and various attacks which might be made against the
protocol. The document says that the SSL Protocol defeats these
attacks.
We use the RAISE Specification Language (RSL) to give formal
specification of the SSL Protocol and to describe the attacks. We can
show that the protocol correctly works by proving some properties of
the RSL specification. Since the specification is written in
applicative style, we can easily prove these properties.
- Professor He Jifeng, UNU/IIST Senior Research Fellows
15:00, Wed
12 August
Title: Unifying theories of programming
Abstract:
Unifying theories of Programming provides a coherent and consistent
basis for specification, design and implementation of programs and
compiler systems. It is wide ranging in style, approach and subject
matter.
A theory of programming starts with a complete boolean algebra of
specifications and defines healthiness conditions which exclude
infeasibility of implementation. These are expressed in algebraic laws
useful for transformation and optimisation of designs. Programming
notations and languages must be restricted to those preserving all
the healthiness conditions.
- Professor He Jifeng, UNU/IIST Senior Research Fellows
15:00, Wed
19 August
Title: Theory of design
Abstract: In this talk, we work towards a more precise characterisation of
the class of predicates that are most useful in program design, namely those
that are expressible in the limited notations of a particular programming
language.
The main goal is to solve the paradox of non-termination presented
in the previous talk. We need therefore to define a class of predicates P
which
can be proved to satisfy the zero laws
True; P = True = P; True
- Professor He Jifeng, UNU/IIST Senior Research Fellows
15:00, Wed 2nd September 1998
Title: Unifying theories of presentation
Abstract:
The methods of explaining the meaning of the notations of a programming
language can be classified under three headings:
denotational, algebraic and operational.
Each of these three styles of presentation has its distinctive advantages
for a study of the theory of programming. To combine these advantages,
a comprehensive theory of programming treats a programming language in all
three styles, and proves that the definitions are consistent with each other
in the appropriate sense. We give the denotational semantics
first, which provides a basis for proof of the laws needed in the algebraic
presentation. At the certain stage, the klaws are sufficiently powerful to
derive and prove correctness of the transition relation of an operational
semantics.
- Professor He Jifeng, UNU/IIST Senior Research Fellows
15:00, Wed 23rd September 1998
Title: Unifying theories for parallel programming
Abstract:
The progress of science involves a constant interplay between diversification
and unification. Diversification extends the boundaries iof science to cover
new and wider range of phenomena; successful unification reveals that a range
of experimentaly validated theories are no more than particular cases of some
more general principle. We suggest that the time has come to attempt a unifying
classification of theories of parallel programming. Idealy, this should provide
a common basis for reasoning about specifications and the correctness of
designs, for optimising programs by algebraic transformation, and for
implementing them in a range of technologies on a variety of machine
architecture, to satify the needs of a wide range odf applications.
- Professor He Jifeng, UNU/IIST Senior Research Fellows
15:00, Wed 7th October 1998
Title: Unifying theories of healthiness conditions
Abstract:
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 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 Kleisli. The uniformity maintains for all paradigms a single notion
of correctness throughout the chain that leads from specifications
through designs to programs that are proved to meet the original specification.
- Zdenek Binder, Visitor from
Laboratory of Automation, University of Grenoble
17:00, Tuesday 15 September 1998
Title: Robust and Decentralised Production Control System Organization
Abstract: Hierarchical approach for the control and organization of
production systems is presented. A decomposition through space, time
and decision-level axis lead us to introduce the COordinated
DEcentralised Control Organization (CODECO). Decision-maker's
autonomy, knowledge distribution equilibrium and robustness by way of
cooperation and coordination relations are the main characteristics of
the CODECO structure. An application for this organization approach is
described in the aim to control an electroplating workshop. Robustness
concept is shown through the exploitation of existing margin to absorb
any disturbances which can affect the process functioning.
Keywords: Control, Decision, Decomposition, Electroplating,
Organization, Robustness.
- William Shu, UNU/IIST fellow from Department of Mathematics and Computer Science, University of Buea, P.O
Box 63 Buea, Cameroon
15:00, Wednesday 30 September 1998
Title: Dynamically Reconfigurable University I: Formally Specifying Core
Operations
Abstract:
Computerising a university over an extended period of time is open to changes
or redirection due to technological advances, funding sources, and social
expediencies that include market and political forces. Hence, specifying
university requirements has to allow for possibly unknown and unforeseen
changes to be dynamically incorporated, without introducing errors. At the
same time the normal daily constraints on the university's computing services
must be met. We identify and formally specify in the RAISE Specification
Language core operations to restructure a functioning university as it evolves
over time. Besides allowing other desired operations to be defined from them,
these operations allow for exploratory versions (prototypes) of universities
that may simulate their evolution over time. These latter are perhaps in
anticipation of what will happen or as experiments on what could happen.
Additionally, we adapt from conventional text editors an "edit environment"
in which restructuring and prototyping of universities may take place.
- Tomasz Janowski, UNU/IIST research fellow
10:00, Friday 16 October 1998
Title: Coalgebraic Semantics for Object-Oriented Concepts
Abstract:
This talk is an introduction to coalgebras, mathematical
structures considered recently as a foundation for object-oriented
languages and programming. I will introduce some basic theory like
duality between algebras and coalgebras, initial algebras and terminal
coalgebras, definitions and proofs by induction and coinduction,
congruence and bisimulation... Then I will demonstrate how this theory
can be applied to formalise some basic OO concepts like objects,
classes, inheritance etc. I will conclude with discussion of possible
future work applying coalgebraic techniques to (applicative) RSL.
- Chris George, UNU/IIST senior research fellow
17:00, Friday 16 October 1998
Title: Proving safety of an authentication protocol
Abstract:
It is important to be certain that security protocols have the
properties that they are supposed to have, and can withstand attack.
We present a proof of correctness of the Needham-Schroeder
Authentication Protocol. This was specified in RSL and the proof uses
the RAISE justification editor. The specification is aimed to be
minimal so as to clarify what properties should hold and to avoid any
unwarranted assumptions. The accompanying proof technique is general
and could be applied to similar encryption-based protocols.
- Prof. Dr. Armando M. Haeberer,
Diretor do Laboratorio de Metodos Formais,
Departamento de Informatica,
Pontificia Universidade Catolica do Rio de Janeiro,
Brazil, UNU/IIST visitor
10-11.30 am, Friday 23 October 1998
Title: The very idea of software development environments:
a conceptual architecture for the arts* environment paradigm
Abstract:
During the last three years we have been building an instantiation of a
system's development paradigm, called ARTS. The paradigm consists of a
view of what a system development environment is, in general terms, and a
methodology for instantiating the paradigm for particular and specific
domains of application.
The motivation for and the explanation of the paradigm are derived from
extant epistemological models of the method of Natural Science. We assert
that these models are directly applicable to the domain of software and
systems construction, and that, from them, we can derive principles and
explanations for what a software development environment should be.
We present briefly the Statement View of scientific theories, a conceptual
architecture for software development environments whose rationale is
given in terms of the Statement View of scientific theories and some
examples of how the present version of ARTS realises this conceptual
architecture.
- Professor He Jifeng, UNU/IIST Senior Research Fellows
15:00, Wed 11th November 1998
Title: Unifying theories for parallel programming
Abstract: The progress of science involves a constant interplay between
diversification and unification. Diversification extends the
boundaries of science to cover new and wider ranges of phenomena;
successful unification reveals that a range of experimentally validated
theories are no more than particular cases of some more general
principle. The cycle continues when the general principle reveals more directions for experimental investigation. This talk suggests that the time has come to
attempt a unifying classification of theories of parallel programming.
Ideally, this should provide a common basis for reasoning about specifications
and the correctness of designs, for optimising programs by algebraic
transformation, and for implementing them in a range of technologiees
on a variety of machine architectures, to satisfy the needs of a wide range
of applications.
- Dr Ma Huadong, UNU/IIST fellow, from Department of Computer
Science and Technology, Beijing University of Posts and
Telecomunications, PRC
15:00, Monday, 16 November 1998
Title: Introduction to Modeling Computer Animation & Multimedia System
Abstract: The report describes the concepts of computer
animation & multimedia system, then some previous
works on computer animation and multimedia will be introduced. Finally,
the working plan in UNU/IIST is discussed.
- Mr Bijay K Das, Manager, TCS (Tata Consultance Service, India)
Hong Kong
11:00-12:00, Wednesday, 18
November 1998
Title: The Millenium Crisis and Solutions by Tata Consulatncy
Services
Abstract:
TCS Corporate profile
TCS' Year2000 Solutions
TCS' Infrasturcture for Y2K Solutions
Q&A
- Professor Paul A. Bailes, UNU/IIST Visitor, from
Centre for Software Maintenance,
Department of Computer Science and Electrical Engineering,
The University of Queensland
11:30, Thursday, December 10th
1998
Title: Programming Without Data: Towards a Totally Functional
Programming Style
Abstract:
There is a useful distinction to be made in forms of language extension,
between what we term "interpretational" and "definitional" styles. The
perhaps-surprising ubiquity of language extension as a metaphor for
programming in general, combined with the apparent disadvantages of the
interpretational style, leads us to attempt to promote definitional
techniques as a general programming style. The essence of "definition" is
the use of "platonic combinators": (higher-order) functions to represent the
computational information that we propose is inherent to various data types.
The more use that can be made of platonic combinators, the more a program is
totally functional, in both senses of the word. Finally, there would appear
to be interesting parallels between this programming style and analog
computation, which appears to be on the verge of a revival. TFP offers
promise as an effective high-level specification/design language for analog
machines.
AUTHOR DETAILS
Professor Paul Bailes is Director of the Centre for Software Maintenance at
The University of Queensland (UQ), and is currently also serving as Head of
the Department of Computer Science and Electrical Engineering/Head of School
of Information Technology. He earned his BSc (Hons) and PhD in Computer
Science from UQ in 1978 and 1984 respectively. Prof. Bailes' research lies
in the field of programming language design and implementation, currently
focussing on problems of software reengineering, design recovery and
conversion. In addition to his academic work, Prof. Bailes has served as a
consultant to organisations such as Fujitsu, Oracle Corporation and the
Australian Defence Science and Technology Organisation on the development of
reengineering tools for a variety of targets.
- Ms He Hua, UNU/IIST fellow from Department of Informatics,
School of Mathematical Science, Peking University, Beijing, 100871, P.R. China
10:00 Thursday, 17 December 1998
Title: A Prettyprinter for the RAISE Specification Language
Abstract: A prettyprinter without losing comments for RSL is presented. The input to
this prettyprinter is the abstract syntax tree of the source code of RSL. It
works in three phases: BOX generating, comments adding and formatted code
producing. The reliability of this prettyprinter is also discussed.
- Elsa Clara Estevez, UNU/IIST fellow, from Agentina
10:00 Friday, 18 December 1998
Title: Bisimulation Abstraction for
Selecting Software Components in RAISE
Abstract: Two main concepts for building software from components are refinement
and abstraction. Refinement helps to construct individual components,
abstraction helps to select and replace components within the
composition (as long as it does not affect the observable behaviour).
Reusing syntax helps in refinement. Composition, in contrast, should
be only concerned with external behaviour of individual components. In
this talk we consider how bisimulation can play the role of
abstracting equivalence for selecting components described as RSL
modules. We take into account partial as well as internal (autonomous)
functions, also allow to compare modules written in different styles
(applicative and imperative). Expressing and proving bisimulation in
RSL does not require any extension to the existing language. We use
simple examples to illustrate refinement and abstraction in RSL, and
briefly present our case study on communication protocols.
