- Ralf Huuck, UNU/IIST visitor, from Institute of Computer Science and Applied Mathematics
Faculty of Engineering, Christian-Albrechts-University of Kiel,
Germany
Time: 11:00, Monday January 7th, 2002
Title: Towards Verification of Embedded Control Software
Abstract:
Programmable logic controllers (PLCs) occupy a big share in automation
control. However, hardly any validation tools for their software are
available. In this work we focus on the verification of two distinct
languages: Instruction List (IL) and Sequential Function Charts (SFC),
which are both defined in the IEC 61131-3 standard. A necessary
prerequisite for the formal verification of a system is a clear formal
semantics. Although defined in the standard this is currently not the
case for SFCs. We present various ambiguities of the SFC language and
propose a solution to this by defining a semantics, which comprises
different execution models and is adaptable to various
interpretations. The subsequent verification is based on this
semantics. According to the nature of the programming languages we
choose different verification techniques. For IL, which is a low level
assembly language, static analysis and abstract interpretation
techniques appear to be appropriate, while for the high level
description and coordination language SFC, model-checking is
used. Finally, key concepts and methods of the prototype verification
tools SFCheck for SFCs and Homer for IL are presented.
Papers in this context:
* Nanette Bauer, Ralf Huuck
Towards Automatic Verification of Embedded Control Software
http://www.informatik.uni-kiel.de/~rhu/apaqs01.ps.gz
* Nanette Bauer, Ralf Huuck, Ben Lukoschus
A Parameterized Semantics for Sequential Function Charts
http://www.informatik.uni-kiel.de/~rhu/bhl01.ps.gz
* Sébastien Bornot, Ralf Huuck, Yassine Lakhnech, Ben Lukoschus.
Utilizing Static Analysis for Programmable Logic Controllers.
http://www.informatik.uni-kiel.de/~softtech/vhs/ADPM2000.ps.gz
- Viktor Verbovskiy, UNU/IIST fellow, from the Institute of
Problems of Informatics and Control, Ul. Pushkina 125, Almaty,
480100, Kazakhstan
Time: 15:00, Tue 29 January 2002
Title: Integrating CSP and DC
Abstract:
Hybrid systems are iteractive systems of continuous devices and digital
control programs. Typical examples are digital modules that control a
physical environment evolving over time. The principal problem of the
subject is to model them so that given a specification for the
continuous component of the system, we cam extract, if this is possible,
form the desription of the total system and the specification of the
continuous component, the specification of the control program which
will force the continuous device to meet its specification.
This work presents a formal description language for hybrid systems,
which is an integrating of CSP, which describes digital control
programs, and DC for specification of continuous devices. We define
primitive systems and operators over systems in DC and prove that so
defined operators meet basic algebraic laws of these operators.
- Mr Hans Madsen Pedersen, UNU/IIST visitor, from Technical
University of Denmark
Time: 12:00 - 13:00, Friday, March 1st, 2002
Title: On Agent Communication Languages and Speech Acts
Abstract:
Agent Communication are essential in Multi-Agent
Systems (MAS), where a number of interacting autonomous agents
are communicating in order to perform some cooperative or
competitive task.
In this seminar we present some of the previous approaches
for developing agent communication languages (ACLs).
These approaches fell into two main categories: the mentalistic
(intentional) approach and the social approach. Mentalistic
approaches (such as KQML and FIPA ACL) are focused on the
cognitive (private) aspect of communication and defines an
ACL in terms of mental modalities, such as beliefs, desires
and intentions. Social approaches suggests that mentalistic
approaches are not suitable in Multi-Agent systems characterized
by being inherently open, autonomous and heterogeneous, like for
example electronic commerce. These approaches emphasizes
on interaction-oriented concepts such as conversations,
obligations, commitments and roles.
We introduce the use of Speech Act theory (by Searle and
Austin) in the development of ACLs.
Finally we sketch how to formally model and specify
Speech Act-based agent communication. In the formalization
we use RSL, Z, Object-Z and CSP. The formalization is
focused on the social aspect of communication, i.e.
obligations, commitments, roles, authorization, norms,
etc. We also consider how to specify Speech Act-based
conversations (such as negotiation) using these concepts.
- Mr Jim Lee, UNU/IIST visitor, from Chinese University of Hong
Kong
Time: 15:00 - 16:00, Friday, March 1st, 2002
Title: Reducing Search Space in Local Search for Constraint
Satisfaction
Abstract: Constraint satisfaction problems (CSPs) occur in all walks of
industrial applications and computer science, such as scheduling,
bin packing, transport routing, type checking, diagram layout, among
others. These problems are NP-complete in general. The traditional
approach to solving CSPs uses a combination of backtracking tree
search and constraint propagation, the latter of which increases
search efficiency by pruning search space dynamically during search.
Another class of solution techniques is based on local search,
which has been shown to be effective and efficient in solving some
large-scale and some computationally hard classes of CSPs. Local
search methods work by traversing the entire search space as guided
by some heuristic functions and trap-escaping strategies.
Typically local search methods for solving constraint satisfaction
problems such as GSAT, WalkSAT and DLM treat the problem as an
optimization problem. Each constraint contributes part of a penalty
function in assessing trial valuations. Local search examines the
neighbours of the current valuation, using the penalty function to
determine a "better" neighbour valuations to move to, until finally
a solution which satisfies all constraints is found.
In this talk we investigate using some of the constraints, rather
than as part of a penalty function, as "hard" constraints, that are
always satisfied by every trial valuation visited. In this way the
constraints reduce the possible neighbours in each move and also the
overall search space.
The treating of some constraints as hard requires that the space of
valuations that are satisfied is connected in order to guarantee that
a solution can be found from any starting position within the region.
Treating some constraints as hard also provides difficulties for the
search mechanism since the search space becomes more jagged, and there
are more deep local minima. A new escape strategy is needed.
We show in this talk how, for DIMACS translations of binary CSPs,
treating some constraints as hard can significantly improve search
performance of the DLM local search method.
- Dr Yifeng Chen, UNU/IIST visitor, from Leicester University,
UK
Time: 15:00, Wednesday, 17 April 2002
Title: A Predicative Semantics of Temporal
Logics
Abstract: In this talk, I will use a technique called generic composition
to study temporal logics. Predicates are treated as sets. Temporal
operators are defined as functions, and their axioms become
consequent laws. The underlying semantics of this approach
corresponds to Kripke's relational semantics and is closely
related to logic. Calculational reasoning involving different
temporal logics is supported. It turns out that the modalities of
possibility and necessity become generic composition and its
inverse respectively. Transformers between temporal
logics also become modalities. Various temporal domains are
unified under the notion of resource cumulation. Generic
composition provides high-level constructions and laws for the
reasoning of temporal operators. Its completeness theorem
guarantees that generic composition and its inverse have the same
expressiveness as the first-order logic.
- Chris George, UNU/IIST senior research fellow
Time: 15:00-17:00,
Friday 10 May, 2002
Title: - How to give a good technical presentation
- Writing technical reports
Abstract: Sime simple ideas can improve your presentation and report
writing skills. These seminars show how to present to or
write for your audience, so that they are more likely to remember what
you presented or read and understand what you wrote.
Some printed materials will be given in advance to UNU/IIST fellows.
Any external attendee who would like a copy in advance should contact
Coffee Das Dores (isc@iist.unu.edu, tel: 712930).
- Dang Van Hung, UNU/IIST research fellow
Time: Tue 30 July, 15:00
Title: An Introduction to Randomized Algorithms
Abstract: The last decade has witnessed a tremendous growth in the area of
randomized algorithms. During this period, randomized algorithms went
from a tool in computational number theory to finding widspread
application in many types of algorithms. Two benefits of randomization
have spearheaded this growth: simplicity and speed. For many
applications, a randomized algorithm is the simplest algorithm
avalable, or fastest, or both.
This introductory lecture presents basic concepts in the design and
analysis of randomized algorithms.
- Prof. Zhu Hong, UNU/IIST visitor from
Computer Science Department,
Fudan University, Shanghai
Time: Tuesday 6 August, 15:00
Wednesday 7 August, 15:00
Friday 9 August, 15:00
Monday 12 August, 15:00
Tuesday 13 August, 15:00
Thursday 15 August, 15:00
Friday 16 August, 15:00
Title: Algorithms and Complexity
Abstract: In the seven talks, basic Concepts on algorithms and complexity
are given, mainly citied from books by
1. Cormen, Leiserson, Rivest and fouth new author "Introduction to
Algorithms" MIT 2001 second edition.
2. Alsuwaiyel "Algorithms, Design Techniques and Analysis" World
Scientific 1999.
Additionally, some adavanced topics such as quantum computing,
bioinformatic computation, Approximatibility or inapproximatibility of
NP-Hard Optimization Problem, Interactive Zeroknowledge Proof System and
Crypotography.
First talk (August 6th) includes basic concept of algorithms and
complexity,
such as worst/average time complexity, space complexity, classes of complexity (P, NP, BPP, RP, PSPACE, etc.) some open
problems in complexity.
Second talk (August 7th) includes mathematical preliminaries of algorithms
and concepts of amortize complexity and smooth complexity. However more
contents are announced tomorrow in detail and will be adjusted after first
talk.
- Prof. L M Patnaik, UNU/IIST visitor, from Indian Institute of Science
Bangalore, India
Time: Wednesday 14 August, 15:00
Title: Hierarchical Location Management Algorithms for Mobile Computing
Abstract: Mobile Host detection is a significant problem in Mobile
Computing applications. Several techniques based on broadcast and
inform strategies have been proposed in the literature. We look at a
hierarchical algorithm for tracking mobile hosts and present its
performance obtained through simulation studies.
- Kevin Jiang Lü, UNU/IIST visitor, from South Bank
University/Brunel University, London, UK
Time: Thursday 8 August, 15:00
Title: Parallel Data Processing
Abstract: Parallelism is an effective technique to improve the performance
of data management systems through spreading the workload to different
processor elements. The formats of most data stored in computer systems
nowadays are either structured or semi-structured. This talk discusses the
issues of using parallel techniques in database systems which are designed
to manage structured data, and presents the techniques for developing a
purpose-built parallel semi-structured data management system.
BIO: Kevin Jiang Lü is a Senior Lecturer at South Bank University/Brunel
University, London, UK. His research areas include database system design,
implementation, and performance. He also teaches on assorted database
courses.
- Uzma Khadim, UNU/IIST fellow from Pakistan
Time: Friday 16 August,
10:00
Title: Developing an XML-Enabled Serials Management System
using RAISE: Specification
Abstract: We present the development of an XML-based system
using formal methods, in particular RAISE. The system aims
to support the management of serials in a library, including
the operations for borrowing, subscription, binding, fine
collection and others, and dynamic enforcement of various
library policies. The design helps to easily incorporate new
operations and policies, and clearly identifies the data
structures to be represented in the implementation as the
XML schema files and to be manipulated by XSL Transformations.
This talk presents the specification of the system written
in the RSL notation. In three weeks time, a companion talk
will describe the implementation.
- Adnan Sherif, UNU/IIST fellows from Brasil
Time: Friday 23 August,
15:00
Title: A Case Study Introduction to XML: Store Automation Software
Abstract: The purpose of this talk is to introduce the XML technology
via a case study. In the first part we answer the general questions
about XML like: What is XML and what are its applications? How is XML
different from HTML? What are the DTD files and Schemas? The second part
presents P2K, a store automation software developed by CSI Ltd. in
Recife-Brazil, and discusses how the development of P2K benefited
from using XML.
- L. S. Barbosa, UNU/IIST visitor, from Departamento de Informática
Universidade do Minho
Braga - Portugal
Time: Tuesday 10 September, 15:00
Title: Coalgebraic Structures in Program Construction
Abstract: Both initial algebras and final coalgebras are devices which provide
abstract descriptions of a variety of phenomena in programming, in
particular of data and behavioural structures, respectively.
The former are specified by a set of constructors and well known in
the programming practice. The latter resorts to a collection of observers
and have been recently recognised as a promising framework to model and
reason about dynamical, state-based systems.
Both initiality and finality, as universal properties, entail definitional
and proof principles, i.e., a basis for the development of program calculi
directly based on (actually driven by) type specifications. Moreover,
such properties can be turned into programming combinators and used, not
only to calculate programs, but also to program with.
This talk aims to provide an introduction to coalgebraic structures,
from a programming point of view, to foster further applications in the
area of program construction.
- L. S. Barbosa, UNU/IIST visitor, from Departamento de Informática
Universidade do Minho
Braga - Portugal
Time: Wednesday 11 September, 15:00
Title: Towards a Calculus of State-based Software Components
Abstract: "Genericity" is a topic which is not sufficiently developed in
state-based systems modelling, mainly due to a myriad of approaches
and behaviour models which lack unification.
This talk will introduce a generic notion of a state-based software
component by quantifying over the extra dimension of the behavioural
approach: a strong monad abstracting from each specific behaviour model.
This leads to the same pointfree, calculational style which is typical
of the so-called "Bird-Meertens school".
A semantic model will be presented whereby state-based components
are regarded as concrete coalgebras for some Set endofunctors,
with specified initial conditions. It will also be addressed
the development of associated component calculi to reason about
(and transform) state-based software designs.
- L. S. Barbosa, UNU/IIST visitor, from Departamento de Informática
Universidade do Minho
Braga - Portugal
Time: Thursday 12 September, 15:00
Title: Coinductive Interpreters for Process Calculi
Abstract: This paper suggests functional programming languages with
coinductive types as suitable devices for prototyping process
calculi. The proposed approach is independent of any particular
process calculus and makes explicit the different ingredients
present in the design of any such calculi. In particular structural
aspects of the underlying behaviour model (eg, dichotomies such as
active vs reactive, deterministic vs non-deterministic) become
clearly separated from the interaction structure which defines
the synchronisation discipline.
The approach is illustrated by the detailed development in
Charity of an interpreter for a family of process languages.
- Arifa Bhutto, UNU/IIST fellows, from Pakistan
Time: Thursday 5
September, 15:00
Title: Developing an XML-Enabled Serials Management System
using RAISE: Implementation
Abstract: We present the development of an XML-based system
using RAISE. The system aims to support the management of
serials in a library, including the operations for borrowing,
subscription, binding, fine collection and others, and
dynamic enforcement of various library policies.
In a seminar two weeks ago, we presented the specification of
this system using RSL. This talk presents the implementation
using XML, in three parts: XML schema files to represents the
format of library documents, XSL Transformations to implement
the inspection of library policies and the execution of
library operations, and Apache server software (in particular
Cocoon - the XML publishing framework for Apache server) to
organize the execution of operations in response to external
requests. We also discuss the (informal) relationship between
the specification and the implementation.
- Prof. He Jifeng, UNU/IIST senior research fellow
Time: 15:00-17:00,
Thursday 26 September, Thursday 03 October, Tuesday 08 October, 2002
Title: Toward a Unifying Theories of Programming
Abstract: A theory of programming is intended to support the
practice of programming by relating each program to the
specification of what it is intended to achieve. An Unifying
theory is one that is applicable to a general paradigm of
computing, supporting the classification of many programming
languages as correct instances of the paradigm. A diversity of
presentation is seen in a theory of programming, which has to
explain the meaning of the notations of a programming language.
Understanding the relationship between presentations ensures
that the diversity is only beneficial; it is also an excellent
indicator of the value and maturity of the theory as a whole.
- Adnan Sherif, UNU/IIST Fellow From Brazil
Time: 15:00-16:00, Monday 7 October,
2002
Title: Towards a Time Model for Circus
Abstract: In this work we propose a time
model for Circus . The model is an extension to the model proposed
by the unifying theories of programming and used by Circus. We take
a subset of Circus and study its semantics in the new model. We create an abstraction
function that maps the timed model to the original model. The main
objective of this mapping is to create a relation between the two
models. This allows the exploration of some properties of the timed
semantics in the untimed model. We study a toy example to illustrate
the use of this mapping.
- Dimitar Guelev, UNU/IIST visitor from Birmingham University, UK
Time: 15:00,
Tuesday, 5 November 2002
Title: Logical Interpolation and Projection in the Duration Calculus
Abstract:
We present a generalisation of an interval-related interpolation theorem
about abstract time Interval Temporal Logic (ITL, Moszkowski, 1985, Dutertre
1995), which was first obtained by Guelev in 2000. The generalisation is
based on the abstract time variant of a projection operator in the Duration
Calculus (DC, Zhou, Hoare and Ravn, Hansen and Zhou 97), which was
introduced by Dang Van Hung in 1999, and later studied extensively in by
Guelev and Dang, 2002. We shortly describe a way to understand interpolation
in the context of formal verification. We give an example showing that DC
does not have the Craig interpolation property in general. We establish a
special form of Craig interpolation for abstract time DC. The generalisation
of interval-related interpolation, which we call projection-related
interpolation, has this DC-specific form too. We show that both Craig and
projection-related interpolation hold about the P-fragment of DC. Our proofs
of these theorems for the P-fragment entail algorithms for the construction
of the interpolants.
- Dimitar Guelev, UNU/IIST visitor from Birmingham University, UK
Time: 15:00,
Wed 13 Nov 2002
Title: Features of Automated Systems and Their Verification
Abstract: Features are separately designed extensions to automated systems meant to
enhance their functionality. Upgrading systems by adding features is a cheap
yet inherently unreliable, because features are often designed apart from
the basic system, when it has already been put in operation. Moreover,
features sometimes extend systems which have not been meant to be extended
at the time of their design.
In this talk we give a survey of the technique used to specify verify
extensions of systems with features by model checking.
We discuss the notion of feature interaction and the detection of
interaction as a case of verification. We give a rough classification of
features according to the way they affect the working of a basic system.
We present and motivate the general notion of feature constructs as an
element of specification and programming languages dedicated to the
description of modifications of systems. In particular we present the
feature construct designed and implemented by Mark Ryan and Malte Plath in
the University of Birmingham, which extends the imput language of the model
checker SMV. We give an example of the use of this construct to specify
features of a lift system.
- Dimitar Guelev, UNU/IIST visitor from Birmingham University,
UK
Time: 15:00,Wed 13 Nov 2002
Title: Logical Analysis of Feature Integration
Abstract: We propose a representation of feature integration in several kinds of
automated systems. It is based on substitution of predicate symbols by
definable predicates. We formalise the description of the actions which are
taken upon integrating features into systems. We assume that these actions
correspond to decomposing the logical formula S which describes the
potential behaviours of the system into a formula S0 for the basic part of
the system with some additional predicate letters, e.g. one for each mutable
part, and a substitution S1 to instantiate these predicate letters with the
descriptions of the actual mutable parts, which themselves are described as
predicates. Thus we obtain a feature-ready description S1S0 (read
"substitution S1 applied to formula S0") of S.
Feature integration into feature-ready descriptions S1S0 of systems is then
specified as inserting substitutions F between the basic part description S0
and the mutable parts description S1, to obtain a description S1FS0 of the
system with the feature described as F integrated. F describes the
integration of a feature by replacing (some of) the mutable parts appearing
in S1 and evetually assigning them revised roles, by having occurrences of
predicate letters for S1 to instantiate.
Patterns involving several distinguished levels of mutability of parts and,
correspondingly, feature integration in the form
Sn Sn-1...S1 S0 -> Sn Fn Sn-1 Fn-1 ... F2 S1 F1 S0
appear in some case studies, with n depending on the type of systems
considered.
We show how several specification formalisms for features known from the
literature, which have been motivated by various observations, can be
fit into this formal framework. Among these formalisms are Samborski's
model, which was strongly inspiring for the approach, the feature construct
for SMV by M. Plath and M. Ryan, the integration of active rules in
databases and others.
We believe that this formalisation of feature integration is compatible with
high level descriptions of the considered systems and preserves the access
to the relevant algorithmic verification methods available for other
formalisations of feature integration. The formalisation allows some
verification problems that treat feature-supplied properties and immutable
basic systems' properties of systems with features to be separated from each
other. It also allows simple logical definitions of some classes of features
known from the literature.
The logic we use in examples of systems' description is the duration
calculus.
- Prof. Bektur S. Baizhanov, UNU/IIST visitor from Institute of
Problems for Informatics and Control of Academy of Sciences of
Kazalhstan, Almaty
Time: 15:00, Thursday 21 November
Title: On generic boolean
first order queries of databases over infinite stable domain
Abstract: In
the relation model of databases a database state is thought of as a
finite collection of relations between elements. For many
applications it is convenient to pre-fix an infinite domain where
the finite relations are going to be defined. Often, we also fix a
set of domain functions and relations. These functions and relations
are infinite by their nature. Some special problems arise if we use
such an approach.
In the focus of talk there are the first order (FO) queries that are
invariant under (order-) preserving "permutations"- such queries are
called (order-) generic. It was shown that the expressive power of
FO logic over finite models embedded in a model (domain with
functions and relations) M is determined by stability-theoretic
properties of M. We show that if M is stable then every class of
finite structures that can be defined by FO query, can be defined in
pure FO logic, i.e. in the language of database relations.
- Prof. Franz Wotawa, Institute for Software Technology, Graz
University of Technology, Austria
Time: 15:00 Thursday 28 November
Title: On the Relationship between Program Slicing and Model-based Debugging
Abstract:
Program slicing is a general, widely-used, and accepted technique
applicable to different software engineering tasks including
debugging, whereas model-based diagnosis is an AI technique originally
developed for finding faults in physical systems. During the last
years it has been shown that model-based diagnosis can be used for
software debugging. In this talk we discuss the relationship between
debugging using a dependency-based model and program slicing. As a
result we obtain that slices of a program in a fault situation are
equivalent to conflicts in model-based debugging.
- Prof. Wang Yi, UNU/IIST visitor, from Upssala University, Sweden
Time: 15:00, Friday, December 6, 2002
Title: Rate-Monotonic Scheduling and Beyond
Abstract:
In classic scheduling theory, real-time tasks (processes) are usually
assumed to be periodic, i.e. tasks arrive (and will be computed) with
fixed rates periodically. Analysis based on such a model of computation
often yields pessimistic results. To relax the stringent constraints on
task arrival times, we propose to use automata with timing constraints
to model task arrival patterns. In a previous work, it is shown that
the general schedulability checking problem for such models is decidable.
In this talk, I will show that for fixed priority scheduling strategy,
the schedulability checking problem can be solved by reachability
analysis on timed automata using only extra 2 clock variables.
The analysis can be done in a similar manner to response time analysis
in classic Rate-Monotonic Scheduling. We believe that this is the optimal
solution to the problem, a problem that was suspected undecidable
previously.
If time permits, I will also try to argue that the computation model
we adopted "could" be used for hardware and software co-design and
co-simulation e.g. for performance analysis and optimization.
