- Dr. MEHMET A. ORGUN, UNU/IIST visitor, from
Department of Computing,
Macquarie University,
Sydney, NSW 2109
15:00, Monday 8 Jan 2001
Title: Intensional logic, possible worlds semantics and logic
programming
Abstract:
Recently, there has been a considerable interest in extensions of
logic programming based on intensional logic. Intensional logic
programs are a set of logical axioms, based on the Horn subset of
intensional logic, which are interpreted as statements true
at all possible worlds (in the sense of Kripke). Note that we
regard temporal and modal logics as instances of intensional logic.
These extensions raise many interesting questions, including whether
they admit complete proof procedures or not, and whether they enjoy
the established properties of standard logic programming such as
the minimum Herbrand model and the fixed-point semantics [1].
Although there have been several attempts at developing semantics for
these new languages, each of those attempts focuses on a specific
language and/or a group of languages with some common features.
Results from such attempts therefore fail to generalize to other
languages and systems.
In this talk, we discuss a language-independent, model-theoretic
framework which can be used to study the conditions under which
intensional logic programming languages enjoy the properties of
standard logic programming. The framework, which has been first
outlined in [2], is based on algebraic and neighborhood semantics
for intensional logics of Scott and Montague [3]. In the framework,
the meanings of intensional operators are formulated as mappings
over the power set of the universe of possible worlds. In particular,
we identify four properties of intensional operators, namely,
monotonicity, conjunctivity, universality and finitariness, and
discuss the implications of these properties on intensional logic
programming languages. The main result is a sufficiency condition
which shows that given an intensional logic whose operators satisfy
all the four properties, then logic programming languages based on
the logic enjoy an extended minimum Herbrand model and the fixed-point
semantics. We show that this result can be applied to many other
temporal and modal logic programming languages. It can also be used as
a template to design a new language with certain desired properties.
(This is joint work with Professor William Wadge of University of
Victoria,
Victoria, Canada)
REFERENCES
[1] J. W. Lloyd, Foundations of Logic Programming , Springer-Verlag,
1984.
[2] M. A. Orgun and W. W. Wadge, Towards a unified theory of intensional
logic programming, Journal of Logic Programming , 13(4):413-440,
1992.
[3] D. Scott, Advice on modal logic. In K. Lambert, editor,
Philosophical
Problems in Logic , pages 143-173, D.Reidel Publishing Company,
1970.
- Dr. MEHMET A. ORGUN, UNU/IIST visitor, from
Department of Computing,
Macquarie University,
Sydney, NSW 2109
15:30, Monday 8 Jan 2001
Title: Towards a logical basis for modelling and querying multi-dimensional
databases
Abstract:
We present a formalism for modelling and reasoning about
multidimensional databases. It is supported by a rule-based system based
on
a multidimensional logic, which we call ML(omega), extended
with aggregation meta-predicates. The system supports a hierarchy of
aggregation dimensions by mapping those dimensions to actual dimensions
of ML(omega), and aggregation meta-predicates basically perform
data transformations over specified aggregation dimensions.
We demonstrate that the rule-based system can be used as a deductive
front-end to a multidimensional database stored in a data warehouse and
can be used as an aid in decision suport systems.
When coupled with a programmable visual user interface,
the implementation of MLP will allow the user to view and
analyse multidimensional relations from different perspectives
by providing facilties for OLAP operations.
(This is joint work with Dr Raymond Wong of University of New South
Wales,
Sydney, Australia, and Associate Professor Weichang Du of University of
New Brunswick, Fredericton, Canada)
- Dr Chen Yifeng, UNU/IIST visitor, from
University of Leicester, UK
10:00, Wenesday 4
April, 2001
Title: Cumulative Computing
Abstract:
This talk presents a general semantic model called cumulative computing to unify a number of important
computational models including real-time systems, reactive
processes, costs and sequential programming. The key concept is
resource cumulation, which can be either resource
consumption or production. Resource cumulation is modeled by
cumulators in which the use of a volume function turns out to
capture the dynamics of resource cumulation.
Instead of requiring any model that it unifies to satisfy a
certain property, we discuss a series of healthiness criteria.
Some of them are more obligatory while others are rather optional.
Resources are formalised as cumulators. A complex cumulator can be
constructed from simple ones. Interesting phenomena of concurrency such as
termination, fairness, synchronisation and overflow become special
cumulators.
Recursions must be unified properly. Plausible techniques are
reviewed, and shortcomings explained. A general
technique called strongest negative fixpoint is then introduced.
All programming compositions that we are aware of satisfy this condition
and previous fixpoints become its special cases.
- Professor J. C. P. Woodcock, UNU/IIST visitor from Oxford
University Computing Laboratory
10:00, Thusday 12 April 2001
Title: Circus: a unifying theory of Z and CSP
Abstract: Circus is a new language
that combines specification statements with imperative CSP, in the
same manner that Morgan's refinement calculus combines them with the
guarded command language. The specification statements in Circus
are operations on a state described using the Z notation. Circus
has a formal model, and we're in the process of deriving refinement
laws to form a calculus. A Circus specification denotes a Z
specification, and the formal model is given in He & Hoare's
Unifying Theory of Programming.
State components may be referred to directly in the CSP processes
of a Circus specification, with an implicit finalisation containing
all references; this means that the Z paragraphs may be refined
separately. The Circus specification is not permitted to make any
reference to the underlying failures-divergences model.
A number of case studies have driven the design of Circus: Abrial's
safety-critical steam boiler, Alcatel's safety-critical dwarf
signal, Handel-C's secure IP-packet firewall, and Mondex's secure
smart card. Extracts from these specifications will be used to
illustrate Circus specifications and their analysis.
- Professor Dines Bjørner, UNU/IIST visitor, from Technical
University of Denmark
10am - noon, Tuesday 17 April and
10am - noon, Wednesday 18 April
Title: What is a Method? An Essayistic Talk on Some
Aspects of Domain Engineering
Abstract: We discuss a concept of method in terms of its postulated
principles, techniques and tools for the realm of software engineering.
Software engineering is here seen as a confluence of domain engineering,
requirements engineering and software design. Our scope is the concept
of domains and domain engineering, and, our span is the concept of
domain facets. For the domain facet area of software development we
then identify, exemplify and investigate, the latter rather briefly,
a number of domain facet development principles and techniques. The
main contribution of this work are believed to be the identification of
the domain facet concept, and the collection (including identification),
classification, part investigation, and "fitting into a larger whole",
of domain facet principles and techniques, as well as the thereby
substantiated claim that these principles and techniques help
characterise methods.
- Professor Dines Bjørner, UNU/IIST visitor, from Technical
University of Denmark
10am - noon, Thursday 19 April
Title: Towards E-Commerce Semantics
Abstract: To understand E-Commerce, we must first understand
"The Market". We introduce such market concepts as Buyers and
Sellers, collectively known as Traders, Supply Chains, Agents
and Brokers. Buyer and Seller actions such as Inquiry, Quotation,
Order, Confirmation, Delivery, Acceptance, Invoicing, Payment,
etc. will be modelled -- and we speculate on how such models
can serve as a basis for understanding E-Commerce.
- Dr Kinshuk, UNU/IIST visitor from Massey University, New
Zealand
15:00, Monday 30 April 2001
Title: Client-server based adaptive
and intelligent tutoring
Abstract: The advent of the Web has brought us
widespread connectivity, shared protocols, and software languages
that can migrate between platforms, and enabled the development of
client-server systems for delivery of advance functionality as well
as material, on a variety of platforms. The client-server systems
provide the Intelligent Learning Systems community with more viable
options for getting systems delivered in the "real world". I shall
discuss how client-server approach has been extended to improve
student model's effectiveness and efficiency in the TILE project,
which aims to provide an integrated system for the management,
authoring, delivery and monitoring of education at a distance.
Adaptivity and intelligence in such systems is achieved using
"Multiple Representation Approach" and "Exploration Space Control"
methodologies.
The Multiple Representation Approach attempts to arrange the
individual multimedia objects (such as audio, pictures, animations)
into a multimedia interface world where the relationships of the
objects to the world are governed by the educational framework.
Learners are provided with various forms of interactivity to suit
the pedagogical goals of the intelligent learning systems.
Exploration Space Control is a methodology for supporting
exploratory learning which attempts to limit learning space, called
exploration space, to adequately control the cognitive load the
learners would face in their exploration process. A combination of
Multiple Representation Approach and Exploration Space Control in an
intelligent learning system ensures adaptivity towards both domain
content and learner, hence providing a higher degree of intelligence
to the learning systems.
I shall conclude my presentation by providing concrete examples of
the issues discussed in the talk.
- Prof Dong Jinsong, UNU/IIST visitor, from NUS,
Singapore
10:00, Monday, 7th May 2001
Title: Integrated Modelling Notations
Abstract:
The design of complex systems requires powerful mechanisms for
modeling state, concurrent events, and real-time behaviour; as
well as for visualising and structuring systems in order to
control complexity. Methods integration has become a recent
research trend in software specification and design. In the
graphical area, many object-oriented methods have merged into
one, Unified Modeling Language (UML). Although traditional formal
methods have not scale-up well, new integrated formal methods show
good promise. This seminar will present an integration of
state-based Object-Z and event-based Timed CSP, Timed Communicating
Object-Z (TCOZ), and transformation techniques from TCOZ to
to UML diagrams. An XML web environment for projecting integrated
formal models to UML diagrams will also be demonstrated.
Bio:
Dr. Dong, Jin Song received the BInfTech degree (with 1st class honours)
and the PhD degree from the University of Queensland (UQ) in 1992 &
1996. From 1995-1998, he was a Research Scientist and then a Senior Research
Scientist at the Commonwealth Scientific and Industrial Research
Organisation (CSIRO) in Australia. Currently, he is an Assistant
Professor at the National University of Singapore (NUS). He served on
the program committee of numerous international conferences and is a
steering committee member of Asia Pacific Software Engineering Conference
(APSEC). Some of his papers can be found at: www.comp.nus.edu.sg/dongjs
- Wang Zhuo and Wang Yanjie, UNU/IIST fellows from Southwest
Jiaotong University
10:00, Thursday 10 May 2001
Title: Supporting Collaborative Design
Abstract:
Collaborative systems provide a rich but potentially chaotic
environment for their users. During collaborative design process,
when different users share a common object, concurrent access
control is the necessity to keep the shared object consistent. We
have developed a new access control model for meeting the new
requirements, which can not be met by using existing models
developed for non-collaborative domains. This model provides
designers an inheritance-based scheme for specifying the
collaboration rights. Lock mechanism is used here. We formally
specify the process of concurrent access control for collaborative
design and implement a prototype based on the specification.
- Professor Gerard Huet, UNU/IIST visitor, from INRIA,
France
15:00, Wednesday, 30 May 2000
Title: 25 Years of Formal Methods and Tools at INRIA: An Overview
Abstract: The French National Institute for Research in Computer
Science and Automatic Control (INRIA) is a public scientific and
technological establishment under the double supervision of Research
Ministry and the Ministry of Economy, Finance and Industry. It
targets to be a research institute at the heart of the information
society. INRIA aims to network skills and talents from the field of
information and computer science and technology from the entire French
research system. Such networks will allow scientific excellence to be
used for technological progress, for creating employment and wealth
and for new uses in response to socio-economic needs.
In this lecture, Professor Gerard Huet will discuss the main concepts
studied at INRIA for formalisation of programming, the tools developed
and their application to certification of safety-critical
software. Professor Huet will illustrate his talk with a few success
stories from INRIA start-up companies in this area and will conclude
with future prospects.
- Professor Augusto Sampaio, UNU/IIST visitor, from Federal
University of Pernambuco, Brazil
15:00-17:00, on June 04, 11, 12, 14 and
18
Title: An Interpreter-Based Approach to Teaching
Programming Language Concepts and Paradigms
Abstract: We use object-oriented concepts (and, in particular, Java as
a meta language) to study programming language concepts and paradigms
through the design of execution environments (interpreters).
We start our study defining a very simple language of expressions and
building an interpreter for it in Java. The language is then
incrementally extended into a higher-order functional language;
the interpreter is extended accordingly, showing the impact of introducing
each new construct. The modular structure provided by the object-oriented
design of the interpreter (which eases its evolution) will be emphasised.
We will briefly explain how the same approach can be uniformly adopted to
extend the expression language into an imperative and then into an
object-oriented language. Opportunities for the students to carry out practical
projects extending the presented languages in various directions will also be
discussed.
- Professor Guo-qing Gu, UNU/IIST visitor, from
College of Science and Technology, East China Normal
University, Shanghai 200062, PRC
15:00, Friday 15 June 2001
Title: Region Labeling and Its Applications to Form Recognition
Abstract:
The chain code is important to the image processing. The Freeman chain
code is explained. A boundary-labeling automaton is constructed, whose
output is the vertex chain code of region boundary, and an efficient
method of labeling region in two-value digital images is proposed. The
methods using VCC to calculate the region area and Euclidean distance
between two points on boundary are developed as well. The application
of region labeling to the form recognition is introduced in detail.
Speaker's Resume:
From March 3, 2001: Professor, College of Science and Technology,
East China Normal University
From May 1, 1999 to March 2: Dean, College of Computer Engineering,
University of Shanghai for Science and Technology
From May 1, 1995 to April 30: Dean, College of Systems Science and
Systems Engineering, University of Shanghai for Science and Technology
From Oct. 1, 1995 to March 2: Vice Chairman, Academic committee,
University of Shanghai for Science and Technology
From 1995: Supervisor of Candidate for Doctor Degree
From Oct. 31: 1992 Professor
From Oct. 5, 1990 : Associate Professor
From July 1, 1988: Lecturer
Obtained Doctor Degree on July 11, 1988, in Physics Department, Fudan
University
From Sep. 1985 to July 1988: Candidate for Doctor Degree, in Physics
Department, Fudan University
From Sep 1976 to March 1976: Graduate Student, in Physics Department,
Fudan University
From Sep 1973 to July 1976: Undergraduate Student, In Philosophy
Department, Fudan University
Research area Theoretical Physics, Pattern Recognition
- Professor Irshad Kamal Khan, UNU/IIST fellow, from the
Chittagong University, Bangladesh
15:00, Friday, 13 July 2001
Title: Computer Science Curriculum for Bangladesh
Abstract: In this talk we propose an undergraduate curriculum in Computer
Science for Bangladesh based on CC2001, the latest curricular
recommendations of ACM and IEEE-CS, as a reference model. The
groundwork for the concrete curriculum is laid through a study of
several curricular recommendations, actual curricula in various
countries, Computer Science departments, and curricular and academic
practices in Bangladesh. The strategy adopted for curricular
implementation involves: compactness, student-friendliness,
incremental approach, emphasis on Software Engineering and
interdisciplinary grounding.
- Juliano M. Iyoda, UNU/IIST fellow, from Centro de Informatica,
Universidade Federal de Pernambuco, Recife, Brazil
15:00, Tue, 24
July 2001
Title: An Algebraic Synthesis of Verilog
Abstract: Synthesis of hardware is the process of deriving a
hardware implementation from its specification. For
rapid prototypes, usually the specification is
described in a hardware description language (HDL)
and the implementation is performed by a reconfigurable
hardware.
This seminar presents an approach to synthesise a
subset of Verilog HDL into the netlist language
XNF. Netlist languages declare a set of hardware
components connected by shared wires, and is
eventually downloaded to an FPGA (Field-Programmable
Gate Array) -- a popular reconfigurable hardware.
The approach transforms a subset of Verilog into a
normal form by applying semantics preserving
transformations (algebraic laws of the language).
The final step maps the Verilog notation to XNF.
A prototype in Prolog is developed to illustrate
the approach.
- Wang Jinsong and Wang Zheming, UNU/IIST fellows, from Tianjin
Institute of Technology, PRC
15:00, Thursday 26 July, 2001
Title: A course structure model to support distance learning
Abstract:
The internet makes ity possible to replace traditional classroom
teaching with distance learning. The greatest benefit of the new
technology is the transformation from traditional teacher-centered
education to learner-centered. To realize the transformation, the
problem of making the developed courseware sharable among different
distance learning platforms should be resolved.
The seminar presents the definition of a course structure model using
the RAISE specification language. With the model, the benefits such
as accessibility, interoperability, reusability and durability of the
course resources can be realized.
- Prof. Hong Zhu, UNU/IIST visitor, from Dept. of Computer Science, Fudan University, Shanghai,
China
15:00, Friday 3 August 2001
Title: A simple and efficient parallel sorting algorithm on star graph
Abstract:
In the first part of this paper, we give a new explanation of
extended Gray code. With this explanation the n! permutations on
n-star graph can be easily listed, and based on this new indexing
scheme a simple and efficient sorting algorithm on n-star graph has
been designed. The complexity of this sorting algorithm is O(n3 log
n). In the second part of this paper, a generalization Dn,k of An,k is
introduced and the diameter bound of Dn,k is analyzed.
- Prof Han-Fu CHEN, UNU/IIST visitor, from the Chinese Academy of
Sciences (CAS)
11:00-12:00, Monday 6 August, 2001
Title: Stochastic Approximation and its Applications
Abstract:
This talk will use examples from control and signal processing to brief
audience about the Stochastic approximation algorithm, which can be applied to
various fields.
Bio: Prof Han-Fu CHEN is a
professor of the Laboratory of Systems and Control, Institute of Systems
Science, Academy of Mathematics and Systems Science, Chinese Academy of
Sciences (CAS). Prof. Chen is a Member of CAS, and the President of the
Chinese Association of Automation. He is currently a visiting professor of
Hong Kong University of Science and Technology.
- Professor Jay Bagga, UNU/IIST visitor, from Ball State
University, Muncie, Indiana, USA
10:00 August 6th, 7th, 9th and 10th,
2001
Title: Visibility Graphs and Graph Drawing Algorithms
Abstract:
Graphs have applications in many areas of computer science and computer
engineering including networks, graphics, software engineering, databases, and
VLSI design. In the context of graphical user interfaces, the geometric
representation of graphs and their visualization play important roles. This
has led to a substantial amount of recent research and results in the subject
of graph drawing.
An important subarea of computational geometry is that of visibility graphs.
These are used to study problems such as finding optimal obstacle avoiding
paths between pairs of objects in a given collection of objects, and such as
placement of objects to optimize "visibility". This has applications in
robotics and architecture.
In this series of lectures, we will discuss some of the above mentioned topics.
Monday 6 August, 10:00
Lecture 1 : Introduction and basic properties; topological graph theory and
planarity algorithms.
Tuesday 7 August, 10:00
Lecture 2: Visibility graphs, algorithms, and applications.
Thursday 9 August, 10:00
Lecture 3: Graph drawing and planar graph drawing algorithms.
Friday 10 August, 10:00
Lecture 4: Complexity of graph drawing algorithms. Software tool for graph
drawing and other graph algorithms
- Siba K. Udgata, UNU/IIST fellow, from Dept. of Computer Sc., Berhampur University, Berhampur, Orissa, India
15:00, Thu 30 Aug 2001
Title: A formal model for channel allocation in distributed mobile
computing system
Abstract: The wireless channels are the most important resources in a mobile
comuting system. Each communiction session that involes a mobile host
requires a channel to be allocated. The possibility of reuse of wireless
channels in different cells subject to satisfying the reuse constraint
is the main concern for optimizing the channel usage. The channel
allocation problem deals with optimization of the channel usage in the
mobile computing system.
We present a formal model for channel allocation problem in a
distributed mobile computing system using Duration Calculus. We propose
a new distributed dynamic channel allocation algorithm based on the
formal model. The proposed algorithm attempts to bring in the best
features of the permission-based and token-based principles.
- Victor Bos, UNU/IIST visitor, from
Eindhoven University of Technology,
Eindhoven, The Netherlands
10:30, Thursday, 20 September
2001
Title: Formal Analysis of Production Systems
Abstract: In mechanical engineering and production research,
much effort is put in designing and analyzing efficient and reliable
production systems. Examples of conventional analysis techniques are
simulation languages, queueing theory, and CAD/CAM techniques. These
techniques are adequate for several purposes, like determining
throughput and cycle time or analyzing physical design, but they are
insufficient when it comes to verification of behavior of production
systems. We propose formal methods as additional analysis techniques
that can be used to do verification tasks. To this end, we used
process algebra techniques to formalize an existing simulation
language, called Chi, for production systems. The mathematical
framework that resulted and the support tools we build have been
applies in several small case studies.
- Victor Bos, UNU/IIST visitor, from
Eindhoven University of Technology,
Eindhoven, The Netherlands
12:00, Thursday, 20 September
2001
Title: Continuous Time in a Systems Engineering Modeling Language
Abstract: The systems engineering modeling language Chi is
developed to specify and analyze production systems. We defined a
process algebra for Chi that enables formal verification of production
systems. Formalization of continuous time features of Chi was a
substantial part of defining the process algebra; we wanted to stay
close to existing continuous time process algebras, but at the same
time, the result had to be practical in the sense that efficient
formal tools could be build to support verification of production
systems. In this talk I will discuss the process algebra of Chi and in
particular its continuous time features.
- Bernhard K. Aichernig, UNU/IIST visitor, from
Institute for Software Technology,
Graz University of Technology,
Austria
15:30, Thursday, 20 September 2001
Title: Test-Case Calculation through Abstraction
Abstract: The talk discusses the calculation of test-cases for
interactive systems. A novel approach is presented that treats the
problem of test-case synthesis as a formal abstraction problem. It is
shown that test-cases can be viewed as formal contracts and that such
test-cases are in fact abstractions of requirements specifications.
The refinement calculus of Back and von Wright is used to formulate
abstraction rules for calculating correct test-cases from a formal
specification. The advantage of this abstraction approach is that
simple input-output test-cases, as well as testing scenarios can be
handled. Furthermore, different testing strategies like partition
testing and mutation testing can be formulated in one theory.
- Bernhard K. Aichernig, UNU/IIST visitor, from
Institute for Software Technology,
Graz University of Technology,
Austria
17:00, Thursday, 20 September 2001
Title: Validating Voice Communication Requirements Using Lightweight
Formal Methods
Abstract: During the last few years so called lightweight
approaches to formal development methods have been proposed in order
to facilitate the technological transfer of these techniques. These
lightweight formal methods take the advantages of a precise and
unambiguous specification language to raise the quality of a system's
specification, without focusing on proofs. The talk presents the
results and experiences gained in two industrial projects, in which
the Vienna Development Method (VDM) has been applied in such a
light-weight manner in the domain of voice communication for
air-traffic control. The techniques raised both the quality of the
informal system specification as well as the efficiency of the system
test suites. We will discuss the costs, benefits and drawbacks of our
use of executable specifications regarding black-box testing.
- Marko Schuetz, UNU/IIST visitor, from
Johan Wolfgang Goethe Universitat,
Frankfurt, Germany
15:30, Thursday, 27 September 2001
Title: Demand Analysis: Theory, Calculi and Applications
Abstract: ADE and CADE are practically applicable calculi for
performing demand analysis. Demand analysis aims at answering
questions such as "For which values as its arguments will this
function fail to terminate?" or "For which values will this function
yield a finite list?". Its applications include a variety of semantic
program analyses: e.g. strictness analysis, absence analysis and
termination analysis. Other applications are program verification,
program understanding and optimization.
The question to be analyzed is represented as a constraint consisting
of a program expression with free variables and a demand. In many
cases the calculi are successful in solving this input constraint and
thus in providing a representation of the answer. A lambda-calculus
extended with constructors and a case-constant for their distinction
is used as the programming language. The language of demands serves
to specify sets of program expressions. It provides constructs for
non-termination, for specific values, for higher-order expressions,
and for data structures obtained by combining the above.
Additionally, constructs for forming unions and intersections of such
sets are available. As a consequence demands can specify sets of
programs very precisely. ADE and CADE differ only in the available
rules: some rules not allowed in CADE are allowed in
ADE. Consequently, while both ADE and CADE are sound, CADE is complete
(if it terminates) but ADE, in general, is not complete.
In the seminar I will present demand analysis and the two calculi
performing this analysis; I will introduce theoretical foundations and
discuss examples demonstrating the strengths as well as the
limitations of the calculi.
- Raoudha Beltaifa, UNU/IIST visitor, from
National School of Computer Science (ENSI),
Tunisia
17:00, Thursday, 27 September 2001
Title: Towards a Systematic Reuse Based on both
General-purpose and Domain-specific Approaches
Abstract: Several advances towards systematic software reuse
have recently been reported, including library systems,
classification techniques, creation and distribution of
reusable components and reuse support environments. Despite
these efforts, we argue that reuse has not delivered yet on
its promise to significantly increase productivity and quality.
We therefore suggest a systematic reuse approach which supports
more formal and disciplined practice of reuse. The proposed
approach is based on: (1) a domain meta-model incorporating
the necessary knowledge to carry out reuse in specific domains;
(2) a component meta-model providing the components with
abstract descriptions to facilitate their reuse; (3) a search
process to support a strategic and intentional component
retrieval; and (4) a set of certified reuse libraries
accessible through Internet and Intranet networks, from where
reusable components could be retrieved and selected. We also
report on a formalisation of this approach using the RAISE
specification language, with C++ source code generated from
formal specifications.
- Catalin DIMA, UNU/IIST visitor, from
Verimag, Gieres, France
10:30, Tuesday, 2 October 2001
Title: N-automata: A New Discretization Technique for Timed Automata
Abstract: We present a theory of n-words, which are finite words
with n distinguished positions. n-words are accepted by n-automata,
which are finite automata with n accepting sets, one for each
distinguished position. In general, regular expressions over n-words
have an undecidable emptiness problem, while n-automata are decidable.
This mismatch is due to nonclosure of n-automata under Kleene star. We
then provide a property which assures closure under Kleene star for
n-automata. As applications, we show how to encode the time
constraints occuring in timed automata into n-automata, and thus how
to apply the n-automata algorithms to check emptiness of timed
automata.
- Catalin DIMA, UNU/IIST visitor, from
Verimag, Gieres, France
12:00, Tuesday, 2 October 2001
Title: Real-time Fault-tolerant Scheduling
Abstract: We present a formalization of the fault-tolerant
scheduling problem for a set of tasks with data dependency constraints
onto a given architecture with distributed resources, by taking into
account task duration. Also, we consider processor and media failures
of the "fail silent" type. Fault tolerance is achieved by replicating
tasks on different processors, and data communications on different
media, fault detection is achieved with the aid of timeouts, while
reconfiguration is achieved by discarding tasks that have not received
all their data until their timeout is reached. We formalize this by
defining a scheduling to be tolerant to a family of failures if it is
a combination of "plain" schedulings of the task family onto the
sub-architecture resulting after each family of failures. The
particularity of such a fault-tolerant scheduling is that it contains
several copies of the same data dependency, and first one which is
"communicated" is taken into account, the others being discarded. We
formalize such schedulings as "quasitopological orderings" of some
special families directed acyclic graphs, by similarity to
"topological orderings" which is the natural formalization of plain
schedulings. We also consider graphs labeled with integers, modeling
task durations. We then show how to compute quasitopological orderings
of directed acyclic graphs and derive an algorithm for computing the
"latest execution time" for each node. We finally derive two
heuristics for computing fault tolerant schedulings of a given task
family onto a given architecture graph, with the "latest execution
times" being used as timeouts for failure detection.
- Prof. Hrushikesha Mohanty, UNU/IIST visitor, from
University of Hyderabad,
India
15:45, Tuesday, 2 October 2001
Title: On Mobile Computing Application Development
Abstract: Currently, mobile computing is a reality because of the
developments in both communication and computing technologies.
The devices are handy for users to carry because of these are
very small in size. However, the size has become a limitation
with less memory and limited battery power. Again, mobile computing
suffers due to vegaries of unreliable wireless communication.
With all these features, mobile computing exhibits a different
computing paradigm.
In this talk, on introducing mobile computing environment I'll
introduce typical environment characteristics like join, migrate,
hoard and clone. Also, I'll discuss on the computing models for
such an environment. Further, I'll discuss about the need for
developing software engineering approaches for developing
mobile computing applications.
- S. Alejandra Cechich, UNU/IIST visitor, from
University of Comahue,
Neuquen, Argentina
17:00, Tuesday, 2 October 2001
Title: Towards a Formal Specification of Design Patterns
Abstract: Most object-oriented application development methods
impose certain modelling concepts that are generally accepted
across many current methods and modelling tools. Frameworks
and patterns express examples of good practices that can be
used to help object modellers achieve more effective results.
But object-oriented patterns are invariably specified by means
of natural language descriptions, class and collaboration
diagrams, and examples of their use in some programming languages.
This means that such specification could be ambiguous or even
inconsistent. Defining a more formal notation allowing
application developers to express statements accurately,
completely, and concisely remains a major challenge.
In this talk, our first contribution is an abstract description
of the essential elements that constitute design patterns.
We formalise these components as RSL modules in such a way
that common properties of patterns, that is semantic constraints
on their use, can be reused. We also introduce some examples
and discuss future extensions.
- Professor Yakup Paker, UNU/IIST visitor, from Queen Mary,
University of London, Mile End Road, London E1 4NS, UK
10:30,
Friday 19 October 2001
Title: Convergence of Internet and Digital
Television: Challenges and Achievements
Abstract: The technology of TV
delivery has changed surprisingly little over the years; the main
advances were the introduction of colour in the fifties and
satellite transmission in the eighties. A new technology is taking
over the TV, however, called digital TV. In Europe, alongside the
analogue channels, the digital TV is being introduced, using
standard TV transmission channels (terrestrial, satellite or cable).
With almost 6 million digital TV subscribers in the UK, it is a
matter of time and political will to turn off the analogue
transmission for pure digital TV.
Since 1970, around four decades after the start of TV for home
reception, the Internet was introduced. Over the years, in
particular due to the World Wide Web, the Internet has become the
main medium for information exchange and communication, creating a
universal space for everyone, with no restriction of geography or
country. The telecommunication companies first using the existing
infrastructure for voice transmission have started to develop
infrastructure for digital data communications and the Internet.
More recently, to respond to the needs of fast Internet connection,
telecom companies started to introduce broadband technologies (ADSL)
to take advantage of the copper wire that exists for telephony.
As TV technology converts to fully digital, the transmission medium
so far used by broadcasters only as a "push" medium to transmit
programmes becomes also a vast digital channel where all sorts of
digital data including Internet and the Web content can be
transmitted. At the same time, the increased bandwidth to home
provided by the telecommunications operators to respond to the
demands of the Web "pull" technology is also giving rise to a new
medium for TV broadcasting called the Web Television. This talk will
introduce some of the issues involved in convergence of TV and
Internet. We will present the achievements of a recent European
project called SAMBITS which has implemented novel ways of combining
the Internet and TV broadcasting, and demonstrated the value of
standards such as MPEG-4 and MPEG-7 in this domain.
- Professor Barrett R. Bryant, UNU/IIST visitor, from Department
of Computer and Information Sciences, The University of Alabama at
Birmingham, 1300 University Blvd., Birmingham, Alabama 35294-1170,
U. S. A.
15:00, Thursday, October 25
Title: Object-Oriented Natural
Language Requirements Specification
Abstract: Recent advances in software
technology such as the development of the Unified Modeling Language
(UML) have not reduced the need for better requirements
specification. Natural language remains the method of choice for
producing such documents. These informal specifications must be
turned into more formal designs on the way to a complete
implementation. These formal requirements are necessary not only
for the rapid prototyping of the evolving software systems but also
to provide a standard reference model upon which all successive
implementations should be constructed. This presentation describes
on-going research in automating the construction of software systems
from a natural language requirements specification, building upon
the theories of Two-Level Grammar (TLG), object-oriented design and
the
Vienna Development Method for formal specification.
Keywords: Natural language, Requirements specification,
Object-oriented software development, Two-Level Grammar, Vienna
Development Method
- Chen Chang, UNU/IIST fellow, from East China Normal University,
ShangHai, China
15:00, Wednesday, October 24th, 2001
Title: Hardware/Software Interface Design
Abstract: Hardware/Software Interface
plays an important role in co-design of the embedded computer
system. It links the software part and the hardware part of the
system. The design process supports software interface
implementation and hardware interface synthesis. This report shows
how the hardware and software interfaces can be implemented by using
bus extended technology in embedded computer system, which includes
the primitive interface, the synchronous interface and the data
communication protocol between the hardware and the software.
- George Oparah, UNU/IIST fellow, from Lagos, Nigeria
15:00,
Friday, October 26th, 2001
Title: XML and Formal Specifications, A Case
Study in VISA Invoice Modelling
Abstract: XML is a method for putting
structured data like spreadsheets, emails, address books, financial
transactions, technical drawings, etc. into text files, then to make
such files available to application programs. Many organizations
that rely on the electronic as well as paper-based exchange of
structured data create their own data formats and exchange
protocols, and publish them as XML Document Type Definitions (DTD).
An example is the official format for invoices and credit card notes
adopted by VISA International (c). The format covers both on-line
and paper-based activities, is well suited for both established
trading partners and for ad hoc purchases, and works across every
possible country, industry sector, and tax and accounting regime.
The format provides enough functionality to satisfy very broad and
diverse needs of VISA but also to serve as a standard, non-VISA XML
Invoice.
The purpose of this talk is twofold. First, to introduce XML, its
applications and some of the surrounding technologies by means of
the VISA Invoice example. Second, to investigate, using the same
example, what kind of useful role formal specifications can play for
XML. In particular, we demonstrate why it is important to formalize
XML DTDs and how this can be done with RSL. A long-term goal is to
lead the way to the rigorous development of XML-processing software.
- Kim Pyong Sam, UNU/IIST fellow, from Pyongyang City, DPR Korea
15:00, Monday, 29 October, 2001
Title: Towards a Dynamic Semantics of an
Assemble Language
Abstract: In this paper,we first present a kind of
assemble language and give its dynamic semantics, and then research
the special properties of assemble programs. Also, we consider the
translation from simple sequential program to our assemble program,
mathematically.
Keywords: assemble program/language, internal/external label(jump),
forward/backword jump, right/left closure, simlicity, translation.
- Kim Yong Chun, UNU/IIST fellow, from Pyongyang City, DPR Korea
15:00, Monday, 30 October, 2001
Title: Specification and Verification of
Spatial Data Types with B-Toolkit
Abstract: Spatial data types provide a
fundamental abstraction for modeling geometric structure of objects
in space, their relationships, properties and operations. In this
talk, we present a formal specification and verification of spatial
data types with the B-Toolkit. First, we give a formal
specification of a realm and operations over it using AMN.
Performing algorithmic refinement before data refinement, we refine
and implement realm update operations. Finally, we discuss about a
formal verification of realm update operations with B.
- Professor Lin Huimin, UNU/IIST visitor, from
Institute of Software,
Chinese Academy of Sciences
10:00-12:00, Thursday, November 22;
10:00-12:00, Tuesday, November 27;
10:00-11:00, Thursday, November 29
Title: An Introduction to CCS
Abstract:
CCS, for "Calculus of Communication Systems", is one of the most
popular models for concurrency. It studies properties and behaviours
of systems consisting of several components running in parallel,
cooperating with each other by exchanging messages via communication
channels. A typical example of such systems is computer networks. The
aim of this series of lectures is to present the basic theories of
CCS, in an informal style. Topics will include operational semantics,
bisimulation equivalence and its properties, and how to specify
and reason about properties of concurrent systems.
- Professor Fiadeiro, UNU/IIST visitor, from ATX Software
SA, Lisbon, Portugal
10:00,
Monday December 10
Title: Coordination: the evolutionary dimension
Abstract:
Whereas object-oriented techniques like inheritance and clientship
have provided useful tools for taming the complexity of system
construction, it is now clear that the same kind of support cannot be
extended to evolution. Yet, the volatility of business requirements,
namely as a result of e-economics, is putting an increasing pressure
on the ability to accommodate changes and extensions in run-time,
even performed directly by customers, and with minimal impact on the
rest of the system.
In this paper, we will argue for the adoption of a third structuring
principle: coordination, which that treats components as black boxes
and is compositional with respect to change. This principle is
supported by techniques borrowed from Parallel Program Design
(superposition) and Configurable Distributed Systems (architectural
connectors).
We provide a formal semantics based on Category Theory that admits an
implementation via design patterns that we shall demonstrate as an
environment for coordinating Java components. Finally, we discuss its
impact on software development methodology.
- Professor Lu Ruqian, UNU/IIST visitor
15:00, Monday 10
December 2001
Title: Commonsense Knowledge
Base and Artificial Intelligence
Abstract: First we discuss the significance of commonsense knowledge processing
for artificial intelligence. Then a commonsense knowledge base,
called Pangu, with its knowledge representation and architecture
will be introduced. We will also present our experience of using the
Pangu knowledge base to support various applications, including a
try of children Turing tests. At last, we discuss some theoretical
issues, including the consistency and completeness problems of
commonsense knowledge base.
- Speaker: Gafurov Davrondjon, UNU/IIST fellow, from Tajikistan
10:00, Wednesday 12 December 2001
Title: Developing a Spell Checker for Tajik Language using RAISE
Abstract: Tajik is spoken in the Republic of Tajikistan where it is an
official language since 1989, and the neighbouring areas of Uzbekistan
and Kyrgyzstan. It is closely related to the Persian spoken in Iran
and Afghanistan, with some Turkic and Russian influences. Its script
has evolved from Arabic (till 1930), Latin (from 1930 till 1940), to
Cyrillic (since 1940). Tajik does not currently have a spell checker.
In this seminar we describe the process of developing a spell checker
for Tajik using RAISE. The spell checker is supposed to: check the
spelling of a given text according to the rules of the language and
existing dictionaries; decompose correct words into prefixes, roots
and suffixes; and offer the alternatives to correct the words which
are misspelled. The development process starts with formalising the
rules for constructing Tajik words from prefixes, roots and suffixes.
The spell checker is built based on this model by capturing the
requirements with specifications and then making the specifications
more concrete until software can be obtained from them directly.
This work addresses the concrete needs of Tajik language
spell-checking. At the same time, the resulting word model could be
reused to build other processors for Tajik (grammar checkers, voice
synthesisers, text recognizers etc.), and the development could be
partly re-applied to build spell checkers for other related languages.
- Professor R.Sadananda, UNU/IIST visitor, from Asian Institute
of Technology
10:00, Thursday 13 December 2001
Title: A Naive Revisit to
Mythical Man Months
Abstract: I begin with disclaimers. I do not practice
software engineering. I do not even teach this subject although I
teach several other topics in Computer Science. This book has
impressed me when I only recently read this book. Many points
raised here must have been met already - are perhaps in the process
of resolution. But the points are profound and far-reaching beyond
the domain of software profession. Eve
ry one knows about this book
- it may be regarded as classic. There are perhaps few books that
can be regarded classic in the Computer Science literature.
Therefore I was not sure if the subject matter would be appropriate
for a seminar at an Institute dedicated for software technology. But
recently when I started inquiring who has read the book in a
gathering of well-known software professionals, I hardly found a few
confirmations although every one knew about the contents. That has
given some confidence to open the topic. Given these considerations,
I propose this as a matter for a discussion and not a Seminar.
Thank you for your consideration.
