- Miaomiao Zhang, UNU-IIST Fellow
16:00 Friday, 6 January, 2006
Title: Formal Analysis of Streaming Downloading Protocol for System Upgrading
Abstract: For a PC-mobile download system which is embedded with streaming download
protocol, there are problems that the data cannot be transmitted correctly
from the PC to the mobile, or the transmission is unacceptably slow. To
solve these problems, we carry out a formal analysis for the protocol with
some timing parameters and a given probability of loosing data using a
probabilistic model checking tool PRISM. We introduce a technique to
reduce the state space of the system modeling the protocol which is a
network of probabilistic timed automata. The experimental results in
PRISM give us a clear explanation to the problems, and are helpful in
identifying the optimal parameter settings to meet industrial
requirements.
- Antonio Cerone, UNU-IIST Research Fellow
15:00 Friday, 3 February 2006
Title: Formal Analysis of Human-computer Interaction using Model-checking
Abstract: The widespread use of computers in safety-critical and security
systems increases the need for human-computer interaction to be
designed in a way that reduces the likelihood of human errors.
Experiments with simulators allow psychologists to better
understand the causes of human errors and build formal models
of cognitive processes.
This seminar introduces an approach to task failure analysis
based on patterns of behaviour, by contrast to more traditional
event-based approaches. The approach is applied to a model of
an air traffic control (ATC) system which incorporates controller
behaviour. The cognitive model is formalised in the CSP process
algebra. Patterns of behaviour are expressed as temporal logic
properties. Then a model-checking technique is used to verify
whether the decomposition of the operator's behaviour into patterns
is sound and complete with respect to the cognitive model.
The decomposition is shown to be incomplete and a new behavioural
pattern is identified, which appears to have been overlooked in the
analysis of the data provided by the experiments with the simulator.
This illustrates how formal analysis of operator models can yield
fresh insights into how failures may arise in interactive systems.
- Rodrigo Ramos, UNU-IIST Fellow
11:00 Tuesday, 7 February 2006
Title: Towards a Model of coordination of rCOS components
Abstract: rCOS has been successfully joined two established formalisms,
state-based and event-based semantics. However, the current version of rCOS
can only model passive components. Coordinators are aimed to harmoniously integrate
complex components to accomplish a collective set of tasks. They are thus usually active entities
difficult to be described in rCOS..
This is a work-in-progress seminar. We will discuss the characteristics of coordinating
elements in component software systems, and the ideas for a possible extension to
rCOS in order to formally describe coordinators and their composition with components.
We will focus on what have been explored and achieved and in particular what we
will pursue further.
- Paddy Krishnan,Bond University, Gold Coast, Australia
11:00 - 12:00, Friday 24 February 2006 (first lecture)(the schedule of next classes/meetings will be decided on 21 February)
Title: Calculating Risk: A brief introduction
Abstract: Every new IT project or changing an existing system has associated risks
with it.
The issue is how to calculate the risk or change in risk. This can be done
at both the project level as well as the IT-group level.
The course will motivate this issue in the context of a government
department and provide the students with a list of relevant papers.
The students will also be given a simple model developed in Excel.
The students are expected to study the existing literature, if possible
interview people involved in new or changing IT projects and develop a
refined model.
There will be only a few official lectures. All other meetings will be
discussions on possible directions and the development of the risk model.
The main deliverable will be the refined risk model (using any suitable
tool).
- Zhiming Liu
15:00, Friday 3 March 2006
Title: Introduction and Discussion on Metropolis and Interface Automata
Abstract: Metropolis is an environment developed by Alberto Sangiovanni-Vincenttelli, et al, at UCB for the design
of heterogeneous embedded systems. It is used to integrate variety of analysis and synthesis tools.
It provides methods for assembling components so that their composition satisfies given properties.
We will discuss the features of this approach and the models of
systems.
Interface automata are proposal by Luca de Alfaro and Thomas Henzinger for support to component-based design
and analysis. We understand how to interface automata to model
components, how to compose them and refine them.
One of the main purposes of this discussion is to know and compare
different approaches to modelling a component.
- Vladimir Mencl
Mar 6 - Mar 10, 15:00-17:30
Title: MasterCraft Introduction
Abstract: This course will provide an introduction into software development with
MasterCraft. The course will start with description of the basic
concepts in MasterCraft, such as user roles, workspaces, and components.
Afterwards, the course will follow development of a sample application
in a team environment.
The objective of the course is to demonstrate the capabilities of
MasterCraft, and to allow us to get started in the project to apply rCOS
to MasterCraft model transformations.
The course will have a significant interactive part; the attendees will
work with MasterCraft and complete small tasks during the lectures.
- Zhiming Liu
10:00 - 12:00, 6-13 March 2006; 15:00 - 17:00 14-17 March 2006
Title: Unified Relational Method of Program Construction and Analysis
Abstract: Aims and Objectives*:
The aim of the course is to establish a good theoretical understand of
how to describe what programs do, how they do it, and why they work; and
to learn how to apply this understanding to the construction of
programs. The theme is to focus on
- The Basic concepts and techniques
- The Relational model
- The unifying views of different theories
- Hierarchy of program classes: building the more complex from the
simpler ones
- The historic trail and unifying understand of the relational theories
of programming
The materials in the course are those that must known for someone to
study and work with formal methods of computer systems development.
*Syllabus*:
Part 1: The Mathematical Preparation (this is prerequisite and will be
mostly omitted)
- Sets, functions, and relations
- Complete Partial Order (CPO)
- Complete Lattices
- Propositional and Predicate Logics
Part 2: Understanding the Essence of Computations
- States
- Computation as a change of states
- Programs as relations on states
Part 3: A Relational Methods of Imperative Sequential Programming
- Deterministic and terminating programs as functions of states
- Nondeterminism as a means of abstraction and nondeterministic and
terminating programs as relations between states
- Nonterminating programs and upward closure property
- Program specification in Hoare Logic
- Programs as predicate transformers
- Unifying Theories of Programming
Part 4: Advanced Topics
- A relation model of concurrent programs and the temporal logic of
actions
- Real-times systems
- Fault-tolerant programs
- A relational model of object-oriented designs
*References*:
1. Edsger W. Dijkstra (1976): A discipline of programming,
Prentice-Hall, INC.
2. David Gries (1981): /The science of programming/, Springer.
3. C.A.R. Hoare and He Jifeng (1998): Unifying Theories of programming,
Prentice Hall.
4. UNU-IIST Technical Report 323
5. UNU-IIST Technical Report 322
- George Buchanan,
University of Wales Swansea, UK
09:30 - 12:30
4 days from Tuesday 14 to Friday 17 March 2006
Title: How to Build Digital Libraries
Abstract: This course will introduce you to the operation, use and construction of
digital libraries (DLs). Starting from a simple introduction to basic
concepts, the course will take a "hands-on" approach to see how DLs work
from the inside. For those from a non-technical background, the course
will give you the confidence to install a library and build user-readable
collections from it; for those interested in extending DL systems for
their own needs, the course will also demonstrate the practical aspects of
adding new components to a running digital library. Some basic knowledge
of web-browsing and text editing is required.
Course Schedule:
Day 1: Introduction to Digital Libraries;
Review of "state-of-the-art" systems and how to perform
simple tasks in Greenstone.
Day 2: Hands-on: from installing Greenstone to building collections
Day 3: Advanced Material: Extending Greenstone for developers and
librarians
Day 4: Unscheduled Masterclass: answering questions from Days 1-3
Biography:
George Buchanan is an established international researcher in digital
libraries. After taking his first degree in Computer Science at the
University of York, England, he ran a software publishing house for
several years before returning to academia. He has been a member of
the leading New Zealand Digital Library research group, based at the
University of Waikato, since 1999 and has contributed major components
to the Greenstone Digital Library system. Dr. Buchanan also has a
strong profile in the mobile human-computer interaction community.
- Prof. A.W. Roscoe, Oxford University Computing Laboratory
1500-1700 on 22, 23, 24, 27, 28, 29 March 2006
Title: CSP and FDR in Concurrency and Security
Abstract: Please be suggested to look at the Prof. Roscoe's book that is available at
web.comlab.ox.ac.uk/oucl/work/bill.roscoe/publications/68b.pdf
Outline of the lecturers:
1. Introduction to CSP (Chapters 1-3 in the book)
2. Introduction to CSP_M and FDR (Appendix B and maybe C)
3. Modelling discrete timed systems using CSP and FDR (Chapter 14)
4. Analysing security protocols using CSP, FDR and Casper (Section
15.3 -printed version)
5.Security protocols II: pervasive computing and web services (Section 15.4)
6. Further topics in CSP and security (depending on the interest of the audience)
- Chris George, UNU-IIST
1500, 5 May 2006
Title: Specification and proof of the Mondex Electronic Purse
Abstract:
The Mondex Electronic Purse was originally specified in Z and proved
correct manually in 2000. Now it is being used as a challenge problem
for automatic correct development, as part of the Grand Challenge for
developing correct software. We will describe the specification of
Mondex in the RAISE specification language and its proof of correctness
using the RAISE tools, and look at the problems involved.
- Chris George, UNU-IIST
14:30 - 17:30, Friday 12 May 2006
Title: A short course on PVS
Abstract: This is a hands-on introduction to doing proof in PVS. After a brief
account of the PVS proof system we will complete some simple proofs
about numbers and then an example arising from a recursive data type.
- Prof Tom Maibaum, Canada Research Chair in the Foundations of Software Engineering, McMaster University, Hamilton, Ontario, Canada
2:30pm, Thursday 18 May
Title: Program Design via CommUnity and Modular Modelling of Aspects
Abstract: The first part of the seminar will be devoted to explaining the abstract
program design language CommUnity, invented by myself and Jose Fiadeiro
over 10 years ago. The language is an extension of Unity and languages
like IP that use super(im)position as a structuring mechanism. The
approach is 'architectural', and uses a semantics based on transition
systems and category theory.
CommUnity can be used to model systems built from components and
connectors, in the sense defined by Software Architecture. The system
defined by such a configuration of components is calculated using the
universal operation of colimit construction in Category Theory. Having
established this setting, we can see aspects as kinds of generic and
parameterised architectural patterns that can be applied to
(sub)configurations in a SW architecture to transform the architecture
to 'use' that aspect. Various examples of (dynamic and) non dynamic
aspects will be given.
- Mohamad Hani El Jamal
15:00, Monday 22 May
Title: Requirements Evolution and Impact On Safety
Abstract: Nowadays, many developers of complex systems use the term time-to-market,
where they develop many approaches in this area and they carry out many
studies, for the purpose of competing with other companies.
Accurately, in the manufacturing field, one can find also another concept,
which is abstracted by the following phrase 'faster, better and cheaper';
because first of all, the key for any kind of manufacture is productivity,
probably followed by cost. To attain this level, each of them tries to
apply many changes by adding a new set of functionalities, new features or
by integrating new technologies for their old systems during or after
development to respond to social and market needs. Unfortunately, as the
actual systems are more and more complex (integrating software and
hardware aspects), perhaps other issues can be affected by change
requests, such as: cost, delay or performance and in particular safety
issues (personnel, environment or hardware).
Our context of study is the requirement and system engineering framework,
based on the combination of three different standards (safety, system, and
requirement engineering standards). For this purpose, we developed a
traceability model (an information system) by using an RSL specification
based on the system engineering view. The aim of this model is divided
into two steps:
First, the model allows the developers to save time during
analyzing the
impact on safety (based on the concept of safety-related requirements)
when we have a submission for a change request during different phases of
development.
Second, when the safety constraints will be impacted by a change
request, the model helps developers to find the files which are impacted
by the change request. These files contain the formal specification of
system development at different levels of decomposition, and allow the
developers to check and to verify the non-violation of the safety
constraints (which mean properties in the context of a formal method) by
using the RSL-SAL translator.
- Prof. Sir Tony Hoare
5:00pm - 6:30pm, Friday 26 May 2006, STDM Auditorium of International
Libray of University of Macau
Title: The ideal of program correctness
Abstract:
- Prof Dr Menno-Jan Kraak
1100, Monday 29 May 2006
Title: Geospatial data infrastructure and e-governance and open source
software - ITC's contribution
Abstract: ITC, the International Institute for Geo-Information and Earth
Observation (http://www.itc.nl) aims at capacity building and
institutional development of professional and academic organizations and
individuals specifically in countries that are economically and/or
technologically less developed. It does this in the knowledge field of
geo-information science and earth observation, which consists of a
combination of tools and methods for the collection - through aerospace
survey techniques -, storage and processing of geo-spatial data, for the
dissemination and use of these data and of services based on these data.
ITC is active in education (Diploma, Master, Master of Science and PhD
level), research and projects services. For the United Nations
University it organizes education in the fields of Land Information and
in Disaster Management. In the Geo-Information world the development of
a Geospatial Data Infrastructure (GDI) does play an important role. A
GDI can be defined as: 'A GDI is the technology, policies, standards,
human resources, and related activities necessary to acquire, process,
distribute, use, maintain, and preserve spatial data.' Since of all
decisions made by individuals and governments around eighty percent is
based on location the access to and provision of geospatial data is of
great importance and especially relevant for e-governance. In its
education and research ITC aims to follow the guidelines of the Open
Geospatial consortium and use open source software. For this reason ITC,
together with the University of Munster and conterra founding member of
the 52North open source initiative. During the presentation several
examples in education and research will be highlighted.
Menno-Jan Kraak (1958) has a Doctors degree (PhD) in Cartography from
Delft University of Technology (1988). In 1981 he graduated in
Cartography from the Faculty of Geographical Sciences, Utrecht
University (cum laude). After his compulsory army service (military
geography unit) he started to work at the Faculty of Geodesy, Delft
University of Technology as (senior) lecturer in Cartography in 1983. In
1996 he started at ITC as professor in Geoinformatics, Cartography and
Visualization, now titled Geovisualization. In 1998 an additional
appointment followed as professor in new visualization techniques at
Department of Geographical Sciences (since 2003 Faculty of Geosciences)
at Utrecht University. Currently he is head of ITC's Geo-Information
Processing Department.
- Dr. Abhik Roychoudhury , National University, Singapore
1500, Monday 29 May 2006
Title: Scenario-based Methods for System Design
Abstract:
Message Sequence Charts (MSCs) are an appealing visual notation for
specifying patterns of interactions between processes. This notation
has found its way into many design methodologies. A variant of MSCs
called sequence diagrams is a part of the UML notational framework.
One main role of MSCs is to capture system requirements in terms of
"good" scenarios the implementation should exhibit and "bad" scenarios
it must avoid. A good part of research on MSCs, driven by this use,
focuses on mechanisms for specifying collections of MSCs, ways of
analyzing such collections and relating them to implementation models.
On the other hand, a broad extension of MSCs called Live Sequence
Charts (LSCs) have been proposed by David Harel and Werner Damm to
serve as a full specification language. Further, David Harel and
collaborators have developed a powerful execution engine called the
Play-Engine to support system designs based on LSCs. From a conceptual
standpoint, the models called netcharts, Communicating Transaction
Processes (CTPs) and Interacting Process Classes (IPC) also falls
within this framework. In this talk, we will discuss the concepts,
modeling examples, tools and applications surrounding these themes.
Brief Biography
Abhik Roychoudhury received his his M.S.and Ph.D. degrees (both in
Computer Science) from the State University of New York at Stony Brook
in 1997 and 2000 respectively. Since 2001 he has been an Assistant
Professor at the School of Computing, National University of
Singapore. His research interests are in models and methods for
reliable development of embedded software and systems, with specific
focus on software validation, analysis and comprehension.He holds a
patent and is currently involved in several funded research projects
in these areas. More details are available from his website
http://www.comp.nus.edu.sg/ abhik
- Dr. Abhik Roychoudhury , National University, Singapore
1000, Tuesday 30 May 2006
Title: Interacting Process Classes
Abstract:
Many reactive control systems consist of classes of interacting
objects where the objects belonging to a class exhibit
similar behaviors. Such interacting process classes appear
in telecommunication, transportation and avionics domains.
In this work, we propose a modeling and simulation technique
for interacting process classes. Our modeling style
uses standard notations to capture behavior. In particular,
the control flow of a process class is captured by a labeled
transition system, unit interactions between process objects
are described by Message Sequence Charts and the structural
relations are captured via class diagrams. The key
feature of our approach is that our execution semantics leads
to a symbolic simulation technique. Our simulation strategy
is both time and memory efficient and we demonstrate this
on well-studied non-trivial examples of reactive systems.
- Professor Paul Gartside, University of Pittsburgh
1500, 31 May 2006
Title: The Shape of Space
Abstract: For millenia people have looked at the night sky and seen shapes real or
imaginary. In the early 1990s astronomers compiling lists of the positions
of galaxies also started seeing shapes - filaments, voids, walls.
In this talk I will explain how techniques from computational topology can
be used to explain and describe the large scale structure of the universe.
In particular I will discuss algorithms for computing Betti numbers,
the importance of 'persistence' and the problems of software reliability
in the context of computational geometry/topology.
- Dines Bjorner, JAIST Japan Adv. Inst. of Sci. and Techn.
11:00, 2 June 2006
Title: Presentation and Critique of A Published Model of A Digitial Rights Language
Abstract: We review a published paper on digital rights languages
thereby also explaining to the lay seminar participant what could
be meant by digital rights. We point out problems in what appears
to be a "formal" explication of the semantics of a specific digital
rights language. We then reformulate the semantics in RSL.
- Dines Bjorner, JAIST Japan Adv. Inst. of Sci. and Techn.
11:00, Monday 5 June 2006
Title: Three License Languages
Abstract: I will show three slides. One gives the
the syntax of a generalised digital rights
license language for the "recursive" issue
of digital rights langauges which allow the
user to pay for, render, copy, edit, and reissue
licenses on works partially edited (derived) from
licensed works. The two other license languages
address issues of who does what in public admini-
stration and at hospitals!
- Dines Bjorner, JAIST Japan Adv. Inst. of Sci. and Techn.
10:30, Tuesday 6 June 2006
Title: Domain and Jackson's Problem Frames
Abstract: We will show a lengthy example of a domain model
and somewhat lengthy examples of the "derivation"
of four domain requirements. The purpose of this is
to relate this approach to software development to
that of Michael Jackson's Problem Frame approach.
(This was DB's keynote talk at a workshop on PFs at ICSE on
May 23rd in Shanghai.)
- Prof. Anders P. Ravn, Department of Computer Science, Aalborg University,
Denmark
1500, Tuesday 6 June 2006
Title: Hybrid Systems - theory and applications
Abstract: We shall consider, how continuous evolution of state variables may be
integrated into a programming framework. In this case, how we can
introduce a hybrid action as a conservative extension of the well
known action system framework of Back et al. It allows us to answer a
question like: "Is; 'x := 1' really an abstraction of what
happens in a digital circuit?
The talk is based on joint work, reported e.g. in:
Mauno Ronnko, Anders P. Ravn and Kaisa Sere, Hybrid Action Systems, Theoretical
Computer Science 290, pp. 937-973, January 2003.
- Prof. Anders P. Ravn, Department of Computer Science, Aalborg University,
Denmark
1500, Thursday 8 June 2006
Title: Hybrid Systems - in practice
Abstract: Here, I discuss how hybrid systems theory may be applied in control
engineering. In particular, we explore how the central concept of
stability translates into invariant properties on discrete state
variables of a hybrid automaton. This opens
up investigations on when such properties are decidable by model checking.
The talk is based on joint work, reported e.g. in:
Thomas Bak, Jan D. Bendtsen and Anders P. Ravn, Hybrid Control Design
for a Wheeled Mobile Robot In Hybrid Systems: Computation and Control
(HSCC 2003) (Eds.: O. Maler and A. Pnueli), LNCS 2623, pp. 50-65, April 2003.
- Dr. Zonghua Gu, Hong Kong University of Science and Technology
1500, Friday 9 June 2006
Title: End-to-end timing analysis of real-time systems with timed automata model-checking
Abstract: Real-time embedded systems must satisfy system-level timing
constraints between external sensor inputs and actuator outputs.
Real-time scheduling theory can be used to verify that the system is
schedulable, that is, no deadlines are missed, but that alone is not enough.
Given that the system is schedulable, how to verify that it satisfies
system-level end-to-end timing constraints, such as freshness, correla-
tion and separation? To address this question, we adopt the approach
of formal modeling and model-checking. Specifically, we use Timed Au-
tomata and the model-checker UPPAAL for verification purposes.
Bio:
Zonghua Gu is an assistant professor in the Department of Computer
Science at HKUST. He joined HKUST in August 2005. His research
interests are real-time embedded systems and software engineering.
Zonghua holds a Ph.D. degree from the University of Michigan at Ann Arbor
- Prof. Anders P. Ravn, Department of Computer Science, Aalborg University,
Denmark
1500, Tuesday 13 June 2006
Title: Embedded Systems - programming the invisible computers
Abstract: When computers are mentioned, most of us think of the office PC, the home PC
or the laptops we see everywhere. Yet, those are really a minority, as
almost all our appliances, machines etc. have many invisible computers
inside. These computers monitor and control the workings of the physical
things that we see, making them comfortable for us to use - think for
instance of the anti-blocking brakes on a car.
In this talk, I shall examine
why it is such a good idea to have these computers and how they require
intense collaboration between engineers and programmers (computer scientists)
to be successfully deployed. After all, we do not want to see bad effects from
the invisible agents. Computers are not embedded in appliances or machines
because they are inexpensive, as often it would be less expensive to do
without them. They replace and enhance dramatically mechanical monitoring and
control mechanisms, and they can do so, because they rely on digital
abstractions from the continuous reality. Furthermore, those embedded
computers use the digitized observations in symbolic processing, i.e.
processing by computer programs. The real power comes from the programs that
can embed engineering theories as active components of the machines. The
design of control mechanisms is no longer a matter of doing mathematics on
the drawing board; rather it is the devising of theories that can be embedded
directly in the machines. Yet, there is a cost. If the embedded
theories are wrong or the programming is faulty, the result is almost
unpredictable.
Contrary to simple analog mechanisms, where there is a direct link between
cause and effect, the computer program can store a long history and react on
it. Thus the cause of a failure may be very hard to pinpoint and even harder
to mend. In the conclusion of the talk, I shall highlight theories that have
evolved in recent decades about reactive, real-time and hybrid
systems. They give a handle on programming embedded systems and checking
their properties, so that we can take the step from building software to
engineering embedded software - software that keeps the computers invisible,
but provides the intended effects.
- Prof. Anders P. Ravn, Department of Computer Science, Aalborg University,
Denmark
1500, Thursday 15 June 2006
Title: Model Based Development - issues and challenges
Abstract: The talk reports on experience from three industrial collaborations which focus on
model based development of embedded systems in a context of object oriented analysis
and design. Also, the necessity of tool support will be illustrated. Finally, a
perspective on future trends will be given; it is based on participation in the
European ARTIST Network of Excellence.
- Vitus S. W. Lam, University of Hong Kong
1500, 16 June 2006
Title: Symbolic Model Checking of UML Statechart Diagrams with an Integrated Approach
Abstract: Though UML statechart diagrams have a well-defined graphical syntax,
their execution semantics is only described in informal English. A
precise definition of the execution semantics is a prerequisite for
performing a formal analysis on UML statechart diagrams. This seminar
discusses a new approach for the formalization and verification of
finite state systems expressed in UML statechart diagrams. The design of
a system is first specified in UML statechart diagrams, then formalized
in the pi-calculus and finally verified automatically by NuSMV. An
application of the proposed approach is demonstrated using the SET/A
protocol as an example.
Biography
Vitus Lam is currently working at The University of Hong Kong. He
received a PhD in computer science from University of Bath, UK. His
research interests include formal methods, UML, pi-calculus, model
checking and e-commerce. Vitus is a chartered member of the British
Computer Society and was the Vice Chairman of the British Computer
Society (Hong Kong Section) for 2001-2002. He is a chartered engineer
and a member of the IEEE.
- Prof. Zhu Hong, Fudan University, Shanghai, China
1100, Monday 19 June 2006
Title: The Minimum Manhattan Network Problem
Abstract: Given a set S of n points in the plane, a Manhattan network on S is
arectilinear network G with the property that for every pair of points in S,
G contains the shortest rectilinear path between them of length equal to
their distance in the L1-metric. The minimum Manhattan network problem is a
problem of finding a Manhattan network of minimum possible length.
I will introduce a 4/8-approximation whose proof is both elegant and
intact. I will also show you some ideas behind the 3-approximation. In fact
the mentioned 1.5-approximation was more or less an attempt to combine the 4
and 3 approximations, though without much success.
- Prof. Anders P. Ravn, Department of Computer Science, Aalborg University,
Denmark
1500, Monday 19 June 2006
Title: Components and their Aspects
Abstract: The lecture present a unifying conceptual framework for components, component
interfaces, contracts and composition of components by focusing on the collection of
properties or qualities that they must share. A specific property, such as
signature, functionality behaviour or timing is an aspect. Each aspect may be
specified in a formal language convenient for its purpose and, in principle,
unrelated to languages for other aspects. Each aspect forms its own semantic domain,
although a semantic domain may be parameterized by values derived from other
aspects. The proposed conceptual framework is introduced by small examples, using
UML as concrete syntax for various aspects, and is illustrated by one larger case
study based on an industrial prototype of a complex component based system.
- Prof. Anders P. Ravn, Department of Computer Science, Aalborg University,
Denmark
1500, Tuesday 20 June 2006
Title: A Ravenscar-Java Profile Implementation
Abstract: The lecture discusses an implementation of the Ravenscar-Java profile. While most
implementations of the profile are reference-implementations showing that it is
possible to implement the profile, our implementation is aimed at industrial
applications. It uses a dedicated real-time Java processor, because we want to
investigate whether the Ravenscar-Java profile, implemented on a Java processor, is
efficient for real applications. During the implementation some ambiguities and
weaknesses of the profile were uncovered. However, test examples indicate that the
profile is suitable for development of realistic real-time programs.
This is on-going joint work with Hans Sondergaard and Bent Thomsen.
- R Venkatesh, Tata Consultancy Services Limited, India
1100 Tuesday 27 June 2006
Title: Visual Specification of Information System Requirement and it's Formal Analysis
Abstract:
Visual notations such as the UML are popularly used by
practitioners to model different aspects of a software system. This talk
presents a semantics of UML object diagrams to
facilitate visual modeling of requirements for business systems.
The talk will also present a comprehensive method for defining and
validating the requirements of a system, based on formal analysis,
automatic scenario generation, and support for rapid prototyping.
Model-checking is used in the formal analysis to identify internal
inconsistencies in the specification, and to generate interesting
`scenarios' from the specifications that can help in identifying
potentially incomplete or anomalous requirements. Prototype tools
have been built for the automatable steps of the method, and it
has been experimentally used to model and validate the
requirements of two systems. The experiments resulted in
identification of many inconsistencies and anomalies in the
requirements of each of these systems.
- Jo kwonsik, UNU-IIST Fellow
15:00 28 June 2006
Title: Specifying a Reliable Banking System in RSL
Abstract:
we present the specification for a
reliable banking system, concentrating on opening an account,
depositing, transferring and withdrawing.
In order to specify the operations
of banking system we deal with head-office, branches, accounts, customers, clerks,
and reciprocal actions between them.
We also specify other requirements in the banking system such as
printing a statement, overdrawn reporting and database management.
The specification is presented using the RAISE Specification
Language.
In this seminar, we present the following research works;
- Identifying and specifying the main requirements for development
of the Banking Management System(BMS) via RSL.
- Checking confidence conditions of BMS specification via RAISE tool.
- Validating the Specification of the BMS via a test case
- Choe Changil, UNU-IIST Fellow
15:00 Thursday 29 June
Title: Model Checking Durational Probabilistic Systems against Probabilistic Linear
Duration Invariants
Abstract:
We define a Probabilistic Duration Calculus (PDC) which can express dependability requirements of real-time systems.
For a model of PDC, we choose a Durational Probabilistic System (DPS) which is simpler than Probabilistic Timed Automata but still good enough for many applications. We extend DPS with infinite time durations and call them infinite
DPS.
Then, we prove that each infinite DPS can be reduced to some finite DPS for the verification for a probabilistic LDI of PDC. This means that it's enough to develop a technique to verify a finite DPS against a probabilistic LDI. For this reason, we
concentrate on the verification of finite DPS and prove that for checking finite DPS against probabilistic LDI the consideration of simple adversaries suffices. This is very important result because the set of all simple adversaries of a finite DPS is finite and we can develop a technique to deal with it, in contrast to non-simple adversaries. Finally, we describe a technique to deal with simple adversaries for our purpose.
- Maria Clara Casalini
15:00, Friday 30 June 2006
Title: A Process Model for Collaborative Problem Solving in Virtual
Communities of Practice
Abstract:
Virtual Communities of Practice enable distributed knowledge
workers to share experiences, expand knowledge and seek solutions to
concrete problems in a given field of interest, all through
computer-supported interactions and collaborative work.
The seminar presents a new process model for collaborative problem
solving in Virtual Communities of Practice. The model relies on a
knowledge repository, comprising resources, properties and statements
in the style of RDF (Resource Description Framework), to underpin the
process of problem-solving. The process allows for formulating,
exploring, matching, decomposing and gradually refining abstract
problem descriptions (one kind of resource) into concrete solutions
(another kind of resource), expanding the underlying repository with
new resources, properties and statements in the process.
The model is defined formally using RSL - The RAISE Specification
Language. We also present a simple case study to illustrate the
process, and demonstrate the initial implementation. The
implementation is part of the UNeGov.net - Community of Practice for
Electronic Governance - portal at www.unegov.net.
- Irshad Kamal Khan
16:00, Friday 30 June 2006
Title: Impact Assessment for Electronic Government - A Practical Guide
Abstract:
Governments worldwide are establishing Electronic Government
and Public Sector Reform initiatives as technology and organizational
tools for better governance. A large percentage of such initiatives,
particularly in developing and transition economies, is considered a
partial or total failure. However, the precise notion of success is
often hard to define and assess objectively, particularly when it
covers the actual impact on the stakeholders and not just deliverables
of projects. There is a need for improving the effectiveness of such
initiatives through a systematic approach to impact assessment.
In this seminar, we present a practical guide to carrying out impact
assessment of e-Government projects. The guide is based on the general
conceptual and analytical frameworks of impact assessment and includes
a micro-economic perspective on the use of technology in the public
sector and beyond. Based on existing models, the guide prescribes a
sequence of practical steps and tools to carry out impact assessment
by e-Government practitioners, including the development of concrete
metrics and measures for assessing particular e-Government projects.
The guide is suitable for assessing e-Government through horizontal
(domain-independent) variables, like the number and maturity of
electronic public services offered to different sectors of the
society. It is also suitable for assessing vertical (domain-specific)
variables characteristic of various application areas - Health,
Learning, Security, Business, etc. For instance, the number of doctor
appointments in public hospitals made though e-Health applications, or
the number of citizens using electronic public services as a result of
e-Learning initiatives.
The guide is applied to assess the impact of some aspects of the
e-Macao Project, also indicating additional data requirements.
- Elsa Estevez
Time: 16:00, Tuesday 11 July 2006
Title: Government-Enterprise Ecosystem Gateway - A Communication
Framework for Electronic Government
Abstract: The seminar will present the Government-Enterprise Ecosystem
Gateway (G-EEG) - a communication/coordination framework through which
multi-organizational processes and applications can dynamically build,
apply and evolve complex communication structures, enabling
asynchronous exchange of messages in various application contexts.
Particular application context is Electronic Government, specifically
the delivery of Electronic Public Services through technology-enabled
collaborations between private- and public-sector organizations.
G-EEG comprises three components:
1) G-EEG-CORE - a core run-time framework providing basic
communication services on top of a plain messaging middleware,
2) G-EEG-EXTEND - a repository of horizontal (process-independent) and
vertical (process-dependent) extensions, along with a mechanism to
dynamically enable such extensions on top of G-EEG-CORE, and
3) G-EEG-DEVELOP - a development framework to rigorously specify,
design, compose and verify messaging extensions.
The seminar will present the motivation for G-EEG and explain
conceptual and formal models underpinning G-EEG-CORE and G-EEG-EXTEND,
defined in terms of RSL - The RAISE Specification Language. The
seminar will also demonstrate an example implementation of G-EEG, part
of e-Macao Software Infrastructure for Electronic Government.
- Dr. Volker Stolz, UNU-IIST Post Doctorial Research Fellow
15:00 Friday 4 August, 2006
Title: TEMPORAL ASSERTIONS FOR SEQUENTIAL AND CONCURRENT PROGRAMS
Abstract: In this talk we present an extension of the well-known concept of
assertions.
Temporal assertions allow the specification and validation of modal
safety properties of an application at runtime. We see this as a
necessary step in enforcing the growing number of implicit
requirements of software specifications, which are often only
informally defined in the documentation of application program
interfaces (API) and are beyond the reach of type checkers,
compilers, or model checkers. Also we show how our techniques can be
applied to existing programs without modifying the source code.
Although, like assertions, our approach cannot prove the absence of
errors, it gives the programmer a more powerful means of
automatically checking assumptions about his program at runtime.
- Liang Zhao, UNU-IIST Fellow
15:00, Wednesday , 9 August 2006
Title: A Type System for the Relational Calculus of Object Systems
Abstract: Being a successful technique in software practice, Object Orientation (OO) is a hot
topic in academic research fields. Among many formalisms, rCOS, a refinement
calculus of object-oriented systems based on Unifying Theories of Programming (UTP),file:///disks/x18/space/home/violetpun/unuiist/newrh/II/5/12/page.html
has been proven a promising one in the sense of its applications to incremental
software constructions, the formal use of UML, etc. However, equipped with a
semantics reasoning on both static and dynamic properties, rCOS is not designed for
static checking. We believe introducing static checking will extend the power of
rCOS. In this paper, we develop a type system for rCOS and prove some type safety
theorems. To make the theoretical results of this paper convincible and easy to be
understood, we follow the traditional approaches of type systems construction. That
is, we use an operational semantics as the basic explanation of rCOS language in
spite of the fact that rCOS is originally developed in a denotational
framework.
- Lu Yang, UNU-IIST Fellow
15:00, Friday, 18 August 2006
Title: A Brief Introduction of MOF 2.0 Query/Views/Transformation
Abstract: Model-to-model transformation is a key technology for MDA.
The need for standardization in this area has led to the MOF 2.0
Query/Views/Transformations(QVT) from OMG.
In this talk we will give a brief introduction to QVT specification and show how we
use QVT in our ongoing
research to make MasterCraft a real MDA tool. The discussion will be based on the
Point of Sale (POST) system.
- Vladimir Mencl (with Matej Polak), presented at the Fractal Workshop, July
3rd, part of ECOOP 2006
15:00, Friday, 25 August 2006
Title: UML 2.0 Components and Fractal: An Analysis
Abstract: The newly emerged standard UML 2.0 provides a framework for modeling
software components. In its design, the existing industrial component
models (EJB, CCM, COM+, and .NET) have been explicitly considered.
However, these models do not possess the features present in advanced
research component models, in particular hierarchical composition.
Yet, the rich set of modeling constructs available in UML 2.0 may be
sufficient even for these component models.
In this work, we analyze the component modeling framework provided by UML
2.0 with respect to how its abstractions match the concepts used in
currently available advanced component models. Based on our analysis, we
propose a mapping of UML 2.0 into the SOFA and Fractal component models
and define constraints such models must satisfy. We have implemented
checking of the constraints and the mappings in a plugin for the
Enterprise Architect UML tool, which also generates all the relevant code
artifacts.
- Prof. Willem-Paul de Roever, Christian-Albrechts-Universitaet zu Kiel, Germany
10:00 - 1230, Tuesday, 19 September 2006
Title: The Inductive Assertion Method
Abstract:
- Prof. Willem-Paul de Roever, Christian-Albrechts-Universitaet zu Kiel, Germany
15:00 - 1730, Tuesday, 19 September 2006
Title: The Inductive Assertion Method (Continued)
Abstract:
- Prof. Willem-Paul de Roever, Christian-Albrechts-Universitaet zu Kiel, Germany
10:00 - 1200, Wednesday, 20 September 2006
Title: Synchronous Transition Diagrams and A Compositional Semantics for Nested STDs
Abstract:
- Prof. Willem-Paul de Roever, Christian-Albrechts-Universitaet zu Kiel, Germany
1500 - 1700, Wednesday, 20 September 2006
Title: Assume-Guarantee Paradigm
Abstract:
- Olumide Gabriel Oteniya
16:00, Thursday, 21 September 2006
Title: Government-Wide Workflow Infrastructure - Enabling One-Stop Government
Abstract: The concept of One-Stop Government is a key trend in the development
of Electronic Government - access to public services should be based
on the needs of citizens/businesses and not the internal structure of
the government. In other words - a citizen need not know the internal
structure of the government in order to interact with it.
One-Stop Government is implemented by a combination of technical,
organizational, legal and financial arrangements. In particular, a
necessary technical support for One-Stop Government is an
inter-mediation hub to match expressed needs against provided services
and to coordinate the execution of services through government
processes, often spanning several government agencies.
In this seminar, we present a possible realization of this
inter-mediation hub - Workflow Infrastructure for One-Stop Government
(GovWF). Based on the Web Services Business Process Execution Language
(WS-BPEL), GovWF supports the operations of a hierarchy of agencies
providing collectively a set of public services, while offering a
uniform one-agency view to its customers (citizens, businesses,
government). Conceptual and formal models are provided to rigorously
describe the operations of GovWF, expressed in terms of RSL - The
RAISE Specification Language. This includes models for semantically
matching specifications of needs against specifications of services,
based on sets of qualitative and quantitative attributes, and for
configuring the execution of services as web service invocations. The
seminar will also discuss and demonstrate a partial implementation of
GovWF, part of e-Macao Infrastructure for Electronic Government.
- Sanne de Roever
14:00, Friday, 22 September
Title: Quality of Service in e-Government Services
Abstract: A great risk in larger software projects is the chance that relevant
agencies in the implementation process are not complying to the project
requirements or specifications. A transparent proxy/monitoring system
can help track responsibilities and the quality of service agencies are
providing. Secondly, complying to project requirements can be made
easier when inter agency communication is rigidly defined and can be
queried.
- Prof. Willem-Paul de Roever, Christian-Albrechts-Universitaet zu Kiel, Germany
15:00 - 1700, Friday, 22 September 2006
Title: Seminar on Verification of Multi-Threaded Java/Java monitors
Abstract:
- Norzima Elbegbayan, UNU-IIST Fellow
1500, Friday, 29 September 2006
Title: Model-checking Driven Design of Interactive Systems
Abstract: This seminar presents a model-checking based methodology to detect
systematic errors commonly made by non-expert users in interacting with web
interfaces. We focus on interactive systems intended for use among large groups of
people, with communication, collaboration, information exchange and interest
matching as the main goals. The human and computer components of the systems are
modelled separately. The human component consists of a general model of the user's
cognitively plausible behaviour, which can be then refined into specific instances
of behaviour that reflect relevant aspects of users' personalities and
skills.
We consider, as a case study, a formal model of an online interactive tool that
enables conference attendees to share thoughts and reactions and select matching
attendees to start communication with. Starting from the initial system design, a
model-checking technique is used to highlight system vulnerabilities that arise from
interactions with non-expert users and may lead to security violations. The results
of the analysis are exploited to improve the design by introducing safeguards that
reduce or even prevent security violations.
- Dr. Charles M. Schweik, Associate Professor, University of
Massachusetts, Amherst
1100, Monday, 9 October 2006
Title: Towards An "Open Source Commons" in Environmental Management
and Policy?
Abstract: Over the last 20 years or more, there has been substantial
progress in three important areas related to environmental management
and its intersection with information technology. First, the debate
over how to manage natural resource commons has matured, since Garrett
Hardin's famous "Tragedy of the Commons" was first introduced in 1968.
Second, vast improvements have been made in information technologies
- such as Geographic Information Systems, Remote Sensing instruments,
Global Positioning Systems, Computer-based models, and most recently,
environmental sensors - that help us better understand the current
conditions of our environment and how they are changing. Third, the
advances of the Internet and specifically the World Wide Web have led
to unprecedented progress and interest in on-line collaboration.
This talk will provide short discussions about the first two
categories of progress (commons governance and information
technologies used to monitor the environment), and then will focus
more specifically on the third topic - online collaboration - by
highlighting three projects the presenter is currently working on.
The first project, entitled the "Open Research System" is an online
metadata and data sharing system being used by two groups in the
United States: (1) The Baltimore Ecosystem Study Long Term Ecological
Research Group and (2) The Urban Ecology Collaborative based out of
Boston College.
The second project, called "ACORN", is an interactive website with
online mapping capabilities trying to reach non-industrial private
landowners in an attempt to better inform them on forest management
related issues and help them connect with professional foresters and
their neighbors.
The third project is an empirical study of open source software
collaboration, which is a form of "digital commons". This project, in
its second of five years, seeks to understand what factors lead to
success and failure in these online and sometimes global
collaborations. Its primary goal is to inform collaborations in other
areas - such as scientific collaboration on environmental problems -
by understanding what works and what doesn't in open source commons
settings.
The talk will conclude with some reflections of the above projects and
a description of potential opportunities in the future related to the
idea of "open source commons" in environmental management.
Bio: Dr. Charles M. Schweik is an Associate Professor with joint
appointments in the Department of Natural Resources Conservation and
the Center for Public Policy and Administration at the University of
Massachusetts, Amherst. He is also the Associate Director of the
National Center for Digital Government (www.ncdg.org). Schweik has a
undergraduate degree in computer science, a Masters of Public
Administration from Syracuse University, and a Ph.D in Public Policy
from Indiana University's School of Public and Environmental Affairs.
His research interests focus on environmental management and policy,
digital government, and the intersection of those domains. His overall
interest is to improve the way environmental policy makers, natural
resource managers, and citizens understand the effects of their
actions and policies, collaborate, and share information about lessons
learned through innovative applications of information technology
(IT). In 2005, he received one of the U.S. National Science
Foundation's Faculty Early Career Development awards to study
collaboration in open source programming communities and its
implications for promoting collaboration in scientific research.
- Dr. Yun Xiaochun, Harbin Institute of Technology and
Institute of Computing Technology, Chinese Academy of Science
11:00, Tuesday, 17 October 2006
Title: Cyberspace Security of Large-Scale Networks
Abstract: In this seminar, we discuss the problems of cyberspace
security in large-scale networks. The security properties of
large-scale networks are quite different from that of local networks
and hosts. We present the security model for large-scale networks
which includes early-warning and crisis control, followed by a
detailed discussion of the crisis control of malicious code. The key
to crisis control is timely location and fast response. We contribute
to three parts of this challenge: (1) design a platform of high
performance packet capture to realize the real-time data processing
under the broadband network environment, (2) develop a high-speed
detection engine to locate the malicious codes effectively under the
large-scale rule set, and (3) present a new isolation policy to
decrease the proliferation effect of many uncontrollable network nodes
and hosts.
BIO: Dr. Yun Xiaochun is Professor and PhD supervisor of Harbin
Institute of Technology and Institute of Computing Technology, Chinese
Academy of Science. He is also the Deputy Chief Engineer of the
CNCERT/CC and the Deputy Director of the Anti-Spam Committee of the
Internet Society of China
Dr. Yun's research interests focus on network and information
security. During the last five years, Dr. Yun has directed more than
10 research projects such as the National Natural Science Foundation
of China, National 863 Program, Pre-Research of National Defense,
National 242 Information Security Program, etc. Dr. Yun has published
more than 50 papers in journals or conferences. He has won the
National Science and Technology Progress Award twice, including one
first-class award and one second-class award, and was chosen into the
Program for New Century Excellent Talents in University of China.
Dr. Yun is currently supervising 10 PhD and 10 MSc candidates.
- Chris George, UNU-IIST
15:00, Wednesday, 18 October 2006
Title: How to give a good technical presentation
Abstract: Some simple ideas can improve your presentation skills.
This seminar shows how to present to your audience, so that they are
more likely to remember what you presented.
- Harold Thimbleby, University of Wales Swansea, UK
11:00, Friday, 27 October 2006
Title: Fun user interfaces to do serious things
Abstract: This informal seminar is open to all UNU-IIST staff
(including administrative staff) and fellows who wish
to attend, but attendance is not mandatory for fellows.
- Thomas Anung Basuki, UNU-IIST Fellow
15:00, Friday, 27 October 2006
Title: Formal Specification of Digital Library Using RSL
Abstract: Digital libraries (DL) are starting to play a central role
in traditional libraries as well as becoming an important tool for
publishers to present and sell their products. A lot of research has
been carried out to study the usability and data representation in DL,
and has led to the development of a variety of software packages, both
commercial and open source. However, very little research has focused
on formal aspects of DL.
This seminar describes our attempt to formally specify DL using the
RAISE Specification Language (RSL). Our specification methodology,
inspired by the 5S Framework by Goncalves and Fox, deals with a fairly
abstract level and aims to provide a basic model of the key DL issues
(digital objects, collections, users and communities) as well as their
relations within the DL framework and the implications of such relations
in terms of security and HCI.
- Zhao Liang
15:00, Thursday, 9 November 2006
Title: Object-Oriented Structure Refinement - A Graph Transformational Approach
Abstract: In UML, the general structure of objects, their attributes and relations are modeled
as a class graph, and an instance of a class graph is defined as an object graph.
The class graph of a system determines the general properties of objects and how
objects collaborate in realizing a use case. In this work, we define class graphs
and their object graphs as directed labelled graphs, and investigate in a graph
theoretical approach what changes in the object structure maintain the capability of
providing services. We define the general notion of structure refinements. A
structure refinement is a transformation from one graph to another that preserves
the capability of providing services, that is the resulting class graph should be
able to provide at least as well as the original graph. We give a small set of
structure refinement rules that is proved to be sound and complete for a kind of
structure refinement.
- Axel Simon, U. of Kent at Canterbury, UK
11:00, Friday, 17 November
Title: Fighting Crime with Geometry
Abstract: A buffer overflow in a C program occurs when input is read into a
memory buffer whose length exceeds that of the buffer. Overflows usually
lead to crashes but may even allow a malicious person to gain
control over a computer system. They are recognised as one of the most
widespread form of security vulnerability. In this talk I describe a
static analysis for detecting buffer overflows. The analysis is
conservative in the sense that it locates every possible overflow.
Furthermore, it is fully automatic in that it requires no
user annotations in the input program.
The key idea of the analysis is to infer a concise description for each
program point that over-approximates the possible variable
valuations that can arise at that program point. These descriptions
consist of finite sets of linear inequalities whose geometric
interpretation in form of polyhedra induce the possible variable
valuations. I will introduce the basic analysis ideas and describe the
pitfalls that arise when analysing real-world C programs. With respect
to the verification of programs that operate on string buffers, I demonstrate how to analyse C strings
whose length is determined by a NULL character in the string.
- Chen Xin, UNU-IIST fellow
15:00, Wed, 22 Novermber 2006
Title: Separation of Concern and Consistent Integration in Requirements Modelling
Abstract: The most effective means to handle the complexity of software systems
are separation of concerns and incremental development, and assurance of
correctness requires formal modelling and formal analysis. When
separation of concerns splits the model into several parts, an important
issue is to ensure consistency among these parts. In the seminar, we
propose an approach supporting separation of concerns and consistent and
incremental modelling of requirements.
- Dr. Dang Van Hung, UNU-IIST Research Fellow
15:00-17:00, November, Fri 24 - Wed 29, 2006
Title: Introduction to the B method and ProB
Abstract: The B method is the result of the inspirational work of Jean-Raymound
Abrial, who developed it with a team of researchers at BP Sunbury in the
later 1980s. It is a formal approach to the specification and
development of computer software systems. B draws together advances in
the formal methods that span the last thirty years, including the Z
notations, pre and post conditions, guarded commands, stepwise
refinement, refinement calculus and date refinement. It synthesises them
into a unified pragmatic and usable development methodology.
The method is based on a wide-spectrum pseudo-programming notation, the
Abstract Machine Notation (AMN), which provides a common framework for
the construction of specifications, refinements and implementations. AMN
provides structuring mechanisms which support modularity and abstraction
in an object-based style, making provable correctness a realistic and
achievable goal. The method is based around the concept of layered
development, which builds larger components from collections of smaller
ones.
There are also a lot of tool supports available for the B method now a day.
This course gives an introduction to the B method, the definition of
AMN, and technique to specify and design software using AMN. The course
also gives a short tutorial on ProB, an animator and model checker for
B abstract machines.
The course details are given at:
http://www.iist.unu.edu/home/Unuiist/newrh/II/2/1/6/page.html
- Siraj Shaikh, UNU-IIST
15:00, Friday 8 December 2006
Title: Analysing authentication protocols using CSP and Rank functions
Abstract: In an increasingly interconnected world, modern day computer
networks have become the bedrock for global communications and electronic
commerce, giving birth to a need for a variety of security protocols,
foremost of which are authentication protocols. This in turn has placed
great emphasis on the design and analysis of authentication protocols; a
task which is error-prone and deceptive in nature, proving somewhat of a
challenge to the academic community. The formal analysis of authentication
protocols has developed into a comprehensive body of knowledge, building
on a wide variety of formalisms and treating a diverse range of
authentication properties.
One formal approach is introduced by Schneider (1998), which involves
modelling cryptographic protocols using CSP, and verifying them using
Schneide's rank functions approach. In this talk, we will introduce
this approach and demonstrate it by using an example protocol by Woo
and Lam (1992). We describe the protocol in detail along with an
established attack on its goals. We then describe Schneide's rank
function theorem and use it to analyse the protocol.
- Dr. Dave Robertson, School of Informatics, The University of
Edinburgh http://www.dai.ed.ac.uk/groups/ssp/members/dave.htm
15:00, Thursday, 14 December 2006
Title: Opportunities and Limits for Open, Peer to Peer Knowledge Sharing
Abstract: Most current attempts to achieve reliable knowledge sharing on a large
scale have relied on pre-engineering of content and supply service, as
evidenced by service-oriented computing through to various current
approaches to "semantic web" construction. Such methods, like
traditional knowledge engineering, do not by themselves scale
to large, open, peer to peer systems because the cost of being precise
about the absolute semantics of services and their knowledge rises
rapidly as more services participate. We describe how to break out of
this deadlock by focusing on semantics related to interaction and
using this to reduce dependency on pre-engineered semantic agreement;
instead making semantic commitments incrementally at run time.
Our method is based on interaction models that are mobile in the sense
that they may be transferred to other components, this being a
mechanism for service composition and for coalition formation.
By shifting the emphasis to interaction (the details of which may be
hidden from users) we hope to obtain knowledge sharing of sufficient
quality for sustainable communities of practice without the barrier of
complex meta-data provision prior to community formation. I shall
describe work being done on the OpenKnowledge project (www.openk.org)
to explore this hypothesis.