- Dr. Wasim Uddin Khan, UNU/IIST fellow, from Computer Engineering
Department, Shie G.S. Institute of Technology & Science, Park Road,
Indore, M.P. India
4pm, Wednesday 2 February 2000
Title: Formalisation of Scheduling for Hard Real Time Systems
Abstract:
This work presents an approach for formalising real time properties
and behaviour of the schedulers for hard real time systems. A real
time temporal logic known as Duration Calculus will be used for
formalisation. Aperiodic, periodic, fixed priority and dynamic
priority schedulers are considered for our work. These four types of
schedulers cover most of the hard real time scheduling problems. We
describe assumptions, computation model, task request, requirements,
scheduling policies, feasibility and optimality for formalisation of
scheduling in Duration Calculus. The work may be extended further
for verification of requirements. This work is useful for working of
various types of operating systems, hard real time control in
industry, surgery, defence, space and various other real life
applications.
- Ms Ri Hyon Sul and Ms Pak Jong Ok, UNU/IIST fellows, from
PRK
Friday, 25 February, 3pm
Title: A University Library Management
System (ULMS)
Abstract: The project has achieved two goals:
1 A specification for development of the ULMS
2. A prototype on a PC for users to evaluate the ULMS
The development included the following steps:
- Initial applicative specification
- A refinement step to improve efficiency
- Imperative specification
- Translation to C++ on Unix
- Porting and compilation using VC++ on Windows98/NT
The presentation covers a number of technical issues:
- refinement and proof
- use of confidence conditions
- implementing quantified and comprehended RSL expressions
- porting and compiling code produced by the RSL translator to a PC
- implementing an RSL map using a standard database
We consider this experience demonstrates how to produce real software
with a comparatively small amount of hand coding and with very high
reliability.
- Mr Wu Xiaojun, UNU/IIST fellow, from Software Division, Dept. of
Electronics and Information, East China Shipbuilding Institute, Jiangsu, China
Friday 25th February, 11.30am
Title: Formal Development of Personnel System in RSL
Abstract: Many aspects of university management lend themselves
readily to computer support, including personnel management,
timetabling of lectures, storing of student records, and so on. In
this talk we describe and formally specify a system supporting the
first of these, the management of a university's personnel. We first
give an abstract specification of this system, then a more concrete
specification of the system. Finally, we translate the imperative
specification into C++ code in UNIX and tested some of functions with
C++. The testing results indicate that the generated code is useful in
software development practice.
- Li Shuguang and Jiang Qing, UNU/IIST fellow, from CAD
Engineering Center,Southwest Jiaotong University, Chengdu 610031,
P.R.China
10:00, Wednesday, 29 March 2000
Title: Combining Case-based and Model-based Reasoning: A Formal
Specification
Abstract: One of the characteristics of design is that designers rely
extensively on past experience in order to create a new design.
Because of this, the case-base reasoning (CBR) process from
artificial intelligence, which helps store, organise, retrieve, and
reuse experiential knowledge, is a good candidate for aiding
designers. A repository of cases is required for CBR, supported by
design information. We formally specify a pair of model and case
databases. The aim is to explore the structure of these databases,
the relations within and between them, as well as rule-checking
possibilities. A second aim is to produce a prototype
implementation for the exploration of further CBR design choices.
- Jin Zhendong, UNU/IIST fellows, from Department of Computer
Engineering and Science, School of Electronic Information
Engineering, Tianjin University, Tianjin, 300072, P.R.China
3pm,
Wed 19 April 2000
Title: Management Systems for Student Accommodation and
National Key Laboratories Network
Abstract: A joint project between UNU/IIST
and UNESCO Beijing office has dealt with the design of various
software systems for supporting university management. In this talk
we describe two of these systems: one dealing with the management of
student accommodation; the second dealing with the management of a
national network of research laboratories such as the National Key
Laboratories of China. We give a brief informal description of each
system as well as an outline of a formal specification in RAISE.
- Paritosh K. Pandya, UNU/IIST visitor, from TIFR, Mumbai,
India
10:00, Thursday, 27 April 2000
Title: Algorithmics of program
verification
Abstract: A key feature of modern science and engineering is
the existence of mature mathematical models and analysis techniques.
In a similar vein, logics of programs are an attempt to
develop adequate mathematical theories for representing the
behaviours of program-like systems. Due to the complexities of even
moderately sized software systems, it becomes necessary to have
computerised tool support for applying these logical theories.
A strong connection between logics of programs and automata
provides a handle to the problem of automating the checking of
logical specification of programs. Programs with large state spaces
can be tackled by having good symbolic representations for sets of
states. In last five years, tools based on these techniques have
shown some spectacular successes including verification of some
network protocols and algorithms which go inside chips such as the
pentium processor. In this talk, we will provide a broad
introduction to the field of logics of programs and give an overview
of the emerging area of algorithmic verification. We will briefly
touch upon the challenging problem of representing and analyzing
behaviours of real-time interactive systems.
- Paritosh K. Pandya, UNU/IIST visitor, from TIFR, Mumbai,
India
15:00 - 17:00, Tuesday, 2 May 2000
Title: DCVALID: A tool for modelchecking Quantified Discrete-time
Duration Calculus formulae
Abstract: Quantified Discrete-time Duration Calculus (QDDC) allows safety and bounded
liveness properties of systems to be specified.
An automata-theoretic decision procedure allows validity of such formulae
to be checked algorithmically.
Moreover, synchronous observers for QDDC properties can be generated
which can be used to model-check properties designs by reachability
analysis. A tool called DCVALID has been constructed using this approach.
In this talk we will introduce the logic QDDC and give several examples
of its use in modelling properties. We will also demonstrate how DCVALID
can be used to verify properties of reactive systems which are modelled as
QDDC, SMV, Esterel or SPIN designs.
- Wang Jianzhong, UNU/IIST fellow, from College of Computer Science & Technology, Box 58, Beijing University of Posts & Telecommunications, Beijing,
100876, P.R.China
15:00, Thursday, 18 May 2000
Title: Modelling and Verification of Network Player System with DCValid
Abstract:
We study the formal modelling and verification of a
network player system using Duration Calculus, a real time interval
temporal logic. The system is modelled by the conjunction of a number
of Duration Calculus formulae each capturing a basic property of the
system. That the system satisfies the requirement is expressed by
the entailment of the requirement formula from the system formula.
We use an automated tool DCValid for verification. DCValid
is a model checking tool and it cannot verify our system in the
general form, and therefore we consider a special instance and use
DCValid to verify it.
- Paritosh K. Pandya, UNU/IIST visitor, from TIFR, Mumbai,
India
10:00, Friday 19 May 2000
Title: Binary Decision Diagrams and Symbolic Model Checking
Abstract: Ordered Binary Decision Diagrams (ROBBDs) provide a canonical and
compact representations for n-ary boolean functions. There are efficient
algorithms for operations such as conjunction, disjunction, existential quantification over ROBBDs and also for functional composition using ROBDDs.
ROBDDs have been widely used in hardware industry for equivalence
checking of circuits and for symbolic simulation. They are widely used in modern symbolic model checkers for representing sets of states and transition relations.
In this talk, we will provide an introduction to ROBDDs and their use in
modelchecking CTL formulae. Tool SMV which implements these algorithms will be briefly described. Finally, the use of Multi-terminal BDDs to represent transition table of automata with large alphabets in the tool MONA will be discussed.
- Andres Flores and Luis Reynoso, UNU/IIST fellows, from Departamento de Informatica
y Estadistica, Facultad de Economia y Administracion,
Universidad Nacional del Comahue, Neuquév, Argentina
10:00, Monday 22 May 2000
Title: A Formal Model of GoF Object-Oriented Design Patterns
Abstract: Object-oriented design patterns identify groups of classes, together
with the key aspects of their functionality and interactions, which
commonly occur in a range of different design problems. The patterns
are generic and embody "best practice" solutions to particular
design problems, and thus offer designers a way of reusing proven
solutions to particular aspects of design rather than having to start
each new design from scratch.
However, patterns are invariably described informally in the
literature, generally using natural language together with some sort
of graphical notation, which makes it very difficult to give any
meaningful certification of software developed using them.
In this talk we describe an abstract formal model of the elements that
constitute a general object-oriented design - classes, their
properties, and the relationships between them - and we show how
common properties of the classes and relationships appearing in the
patterns in the GoF catalogue can be defined as generic functions
in this model. Finally, we explain how these functions can be used to
check whether (a subset of) a particular object-oriented design
matches a given GoF pattern, and illustrate this using the GoF
behavioural patterns.
- Professor Dines Bjørner, UNU/IIST visitor, from Dept. of IT,
Techn. Univ. of Denmark, DK-2800 Lyngby, Denmark
16:30-17:30,
Monday 22 May 2000
Title: Where do Software Architectures come from?
Abstract: David Garlan proposes one approach to the concept of software
architectures-but it is not clear from where the basic ideas deter-
mining his architectures come from.
In this seminar we will suggest a complementary approach in which
software architectures "derive" from domain requirements, with these
domain requirements "deriving" from domains.
We first examine, briefly, the Garlan software architecture concept.
Then we show an example development, from domain, via domain,
interface and machine requirements to first software architecture and
then program organisations. We use the term software architecture much
like the term computer architecture: That which the user sees. And we
use the term software (or program) organisation much like the term
machine organisation. The former amounts to a computers instruction ad
data repertoire, the latter to a machine's internal data flow (busses,
registers, channels, control, etc.) . Our concept of software
architecture have it implement domain and interface requirements, and
our concept of software organisation have it implement machine
requirements.
In "converting" domain descriptions to requirements we exemplify
techniques of domain projection, instantiation, extension and
initialisation. And in "converting" requirements to software design:
Software architecture and software organisation, we exemplify
techniques of distribution, concurrency, components, connectors,
ports, glue, etc., as in Garlan's approach.
- Professor Dines Bjørner, UNU/IIST visitor, from Dept. of IT,
Techn. Univ. of Denmark, DK-2800 Lyngby, Denmark
9:30-10:30, Tuesday 23 May 2000
Title: Domain Engineering
Abstract:
Before software can be designed, it must be required. And before it
can be required the problem, that it somehow solves, must reside in a
domain - the application domain. In this seminar I outline what it
could take to properly understand a domain: The development of domain
description documents: Briefs, rough sketches, analyses,
terminologies, narratives, formal specification, verification and
validation - such that these documents cover, individually, or with a
reasonable separation of concerns the following domain aspects: Domain
intrinsics- Bias, support technologies, rules & regulations, human
behaviour, etc. We illustrate these ideas and relate them to Michael
Jackson's lexicon of principles, practices and prejudices.
- Professor Dines Bjørner, UNU/IIST visitor, from Dept. of IT,
Techn. Univ. of Denmark, DK-2800 Lyngby, Denmark
9:30-10:30, Wednesday 24 May 2000
Title: Requirements Engineering
Abstract: Before software can be designed, it must be required. And before it
can be required the problem that it somehow solves1 must reside in a
domain - the application domain. Thus we cannot, we believe, develop
a requirements description unless we have first understood the domain.
We assume that such an understanding is therefore reasonably, but not
necessarily well, or completely developed (beforehand). Now
requirements focus on three, for two of them slightly overlapping, and
for the third, complementary, sets of requirements: Those that are,
so-to-speak, "derived" from the domain: The domain requirements; those
that shall govern the interface between the users and the machine
(software + hardware) - the CHI (or MMI) interface requirements;
and those, the machine requirements, that speak of performance,
dependability, maintainability, etc. In this talk I shall illustrate
techniques issues associated with requirements development:
Stake-holder perspectives, domain projection, instantiation,
initialisation and extension. Some issues can also be formalised, and
we shall, briefly, discuss those that can and those that can't.
- Professor Dines Bjørner, UNU/IIST visitor, from Dept. of IT,
Techn. Univ. of Denmark, DK-2800 Lyngby, Denmark
9:30-10:30, Thursday 25 May 2000
Title: On a Course in Software Engineering
Abstract:
We postulate that software engineering encompasses a number of
disciplines. We single out software development (domain engineering,
requirements engineering, software design - all using both informal and
formal approaches, intertwined, indispensably), and project & product
management as focal points.
We have developed, over the years, and are still developing, a
comprehensive set of lecture notes and student project material
covering, increasingly, these subjects.
In this seminar I wish to tell you about my aims & objectives, how I
have structured the lecture notes, my experience in teaching the
course, and - through all this - my view on what software engineering!
- Professor Dines Bjørner, UNU/IIST visitor, from Dept. of IT,
Techn. Univ. of Denmark, DK-2800 Lyngby, Denmark
9:30-10:30, Friday 26 May 2000
Title: An Operational Semantics Imperative CSP
Abstract: We define, syntactically, a parallel programming language in the style
of CSP - focusing only on the flow of sequential and concurrent
control flow. And we present a state transition semantics for this
CSP-like language. The language is motivated by some introductory
example parallel specifications of programs.
- Do Van Nhon, UNU/IIST fellow, from Department of Math-Computer
Science, College of Natural Sciences, National
University of Ho Chi Minh City, Viet nam
A Systematic Design of Real-time Systems Using Duration
Calculus
Title: 15:00, Thursday 1 June 2000
Abstract: We present a systematic way for the design and verification of
real-time systems using Duration Calculus via a toy example:
A motor Control System. We model real-time systems as synchronous systems
and formalise the synchronous interface between the components of the
systems as duration calculus formulae expressing the approximation between
state variables. Preliminary Designs are then derived from the safety
requirements and the interface. Functionality requirements are incorporated
to be consistent with the Preliminary Designs. The constraints over parameters
of the design are discovered and based on them we specify and prove the
correctness of the system in general.
We also apply our discretization technique to a real industrial example,
Biphase Mark Protocol. It works well for this case with some advantages
comparing with previous ones.
The model and techniques presented in this paper can be reused for
other problems as well.
- Henning Dierks, UNU/IIST Visitor, from Oldenburg, Germany
10:00, Tue 6 June 2000
Title: PLC-Automata - An Introduction
Abstract:
The language of PLC-Automata is suitable to specify
the behaviour of systems which frequently poll the
input from the environment and behave in a cyclic
manner. The name stems from the implementation
hardware PLC (Programmable Logic Controller) which
is often used in industry to implement safety-
critical systems.
In this talk the language is explained informally
and an overview of the main results for
PLC-Automata is given. Moreover, the tool
"Moby/PLC" for PLC-Automata is introduced briefly.
PLC-Automata are especially suitable to deal with
real-time problems. But in this talk real-time is
discussed on the informal level only. The formal
treatment is left to succeeding talks.
- Balkhis Abu Bakar, UNU/IIST fellow, from School of Information Technology, Universiti Utara Malaysia, 06010 Sintok, Kedah, Malaysia.
10:00, Monday, 26 June
2000
Title: Automated Result Verification with AWK
Abstract: We discuss result-verification as an alternative to
implementation-verification, its limitations, advantages and the
technical context to apply this technique in practice. The goal of
result-verification is to prove that one execution run of a program
satisfies its specification. Result-verification has fewer conditions
for its applications in practice, gives more opportunities for
automation and, based on the execution record not the implementation,
is suitable for complex heterogeneous systems. The technical context
proposed in the talk includes the following decisions: (1) The
execution record is a text file containing observations made during
program execution, like the operations invoked, values observed about
the resulting states etc. (2) Result-based specification is a
first-order predicate build with variables, functions, relations and
limited kind of quantification. The variables allow referring to the
fields within the lines of the record and how their values change for
different operations. (3) Specifications can be composed, we discuss
several composition methods depending if checking produces a yes/no
answer for the whole record or an answer for every observation within
the record. (4) Verification is carried out automatically by the
specification-generated verifier program, written in AWK. The AWK
interpreter is applied to both generate this program and carry out the
actual verification. The talk includes the demonstration of the
prototype verifier generator.
- Friedrich Wilhelm Schroeer, UNU/IIST visitor, from GMD FIRST, Germany
11am, Thursday, 29 June, 2000
Title: ACCENT: A Compiler-Compiler for the Entire Class of Context-Free Grammars
Abstract: The majority of users apply compiler construction tools for the
implementation of domain specific languages. These users are familiar
with the notion of context-free grammars, but they are not necessarily
experts in compiler construction. Unfortunately, preparing the
specification submitted to a tool often requires knowledge of
implementation details. Moreover, many official language
specifications cannot be processed by traditional tools.
We present a modern compiler-compiler (a member of the GENTLE toolkit)
that avoids the problems of LALR and LL parsers. It is capable of
processing all context-free grammars without any restrictions. Our
approach combines exhaustive parsing (Earley's Algorithm) to achieve
generality, and predictive parsing to improve efficiency.
In traditional parsers ambiguities are excluded by the limitations of
the the underlying technology. However, a general parser calls for a
high-level mechanism to deal with ambiguous grammars. We introduce a
systematic classification of the nature of ambiguities and an
annotation framework that allows to resolve them at the abstract level
of the grammar.
Furthermore, we discuss a companion tool that statically checks
grammars for ambiguities.
- Uwe Der, UNU/IIST visitor, from GMD, Germany
12am, Thursday, 29 June, 2000
Title: A Parallel Implementation of Job Shop Scheduling Heuristics
Abstract: In the talk, we present parallelized versions of simulated annealing
based heuristics that have been developed for job shop scheduling.
In our first implementation, we make use of the stochastic properties
of simulated annealing. That means we distribute instances of the
sequential algorithm on a parallel computer (for example, on a
pc-cluster). After a number of steps the processors exchange the
best solution found so far. In order to carry out our distributed
computing strategy we employed an MPI-based library developed at GMD.
We provide first computational results with different communication
strategies for some benchmarks introduced by S. Lawrence.
Bio facts:
- 1993: BSc.Math, Technical University of Berlin, Germany
- 1999: MSc.Math, Technical University of Berlin, Germany
- 1995 - 1999: Research Assistant at the GMD, Research Institute
for Computer Architecture and Software Technology
- 2000 - : Ph.D. Student, Research Fellow
- Dr. Zhiming Liu, UNU/IIST visitor, from
Department of Mathematics and Computer Science,
University of Leicester, UK
July 6th, 11th, 13th, 18th and 20th, 2000
Title: Fault-tolerant and Real-time Systems
- Specification and Verification of Fault-Tolerance, Timing, and Scheduling
Abstract: Fault-tolerance and timing have often been considered to be implementation
issues of a program, quite distinct from the functional safety and
liveness properties. Recent work has shown how these non-functional and
functional properties can be verified in a similar way.
However, the more practical question of determining whether a real-time
program will meet its deadlines, i.e., showing that there is a feasible
schedule, is usually done using scheduling theory, quite separately from
the verification of other properties of the program. This makes it hard to
use the results of scheduling analysis in the design, or redesign, of
fault-tolerant and real-time programs.
In these talks, we will show how fault-tolerance, timing, and schedulability
can be specified and verified using a single notation and model. This
allows a unified view to be taken of the functional and nonfunctional
properties of programs and a simple transformational method to be used
to combine these properties. It also permits results from scheduling
theory to be interpreted and used within a formal proof framework.
The notation and model are illustrated using a simple example.
We will use transitions systems as the program model and the Temporal Logic of
Actions (TLA) as the specification notation. If time allows, we will discuss
a way for linking this framework with the DC notation.
The talks will aim at the fellows at UNU/IIST at a level of details
understandable to 2nd and final year PhD students.
- Yingxu Wang, Prof., Ph.D, UNU/IIST visitor, from
Centre for Software Engineering,
The Swedish National Research Institute for Industrial Engineering,
Argongatan 30, S-431 53, Molndal, Gothenburg, Sweden
10:00, Friday 21
July 2000
Title: Software engineering research and practice in Europe
Abstract:
Software engineering is a discipline of increasing importance in
computer science and informatics, as well as in the software industry.
This talk reviews recent research and practices of software engineering
in Europe and in the author's work. Theoretical investigation on
foundations of software engineering and process algebra are introduced.
Empirical studies on comparative software engineering, software industry
organisation, and a unified software engineering process reference
model(SEPRM) are presented.
Perspectives on trends and research topics considered significant and
worthy of being explored are provided, such as process-based software
engineering, new mathematics for software engineering, bioinformatics,
and computing science, because this is one of the most dynamic,
innovative, and widely applied science and engineering areas.
Significant breakthroughs are being expected and let's work together to
make these happen.
- Qin Shengchao, UNU/IIST fellow, from Dept. of Informatics, School of Mathematics, Peking University, Beijing, 100871, P.R. China
10:00, Friday, 28 July, 2000
Title: An Algebraic Approach to Hardware/software Partitioning
Abstract:
Hardware and software co-design is a design technique which delivers
computer systems comprising hardware and software components. A
critical phase of co-design process is to decompose a program into
hardware and software. This paper proposes an algebraic
partitioning method whose correctness is verified in the algebra of
programs. We introduce the program analysis phase before program
partitioning and develop a collection of syntax-based splitting rules,
where the former provides the information for moving operations from
software to hardware and reducing the interaction between components,
and the latter supports a compositional approach to the program
partitioning.
- Dr. R. Ramanujam, UNU/IIST visitor, from
Institute of Mathematical Sciences, Chennai, India
3pm,
Monday, 7th August 2000
Title: Message passing in finite state environments
Abstract: When analysing message passing systems, one is forced to
take message buffers into account, and this usually
complicates analysis. Moreover identifying regular
behaviours of such systems is hard: matching receipts of
messages with their `send' events leads to (at least)
context free behaviour. We therefore study this problem
in the context of finite state environments, where buffers
are either bounded or implicitly bounded memory - in the
latter case, it may "forget" some messages. We present
an automaton model for the systems and a temporal logic
to reason about them. A model checking procedure is described.
The work reported is joint with B. Meenakshi (Institute of
Mathematical Sciences, Chennai, India).
- Dr. R. Ramanujam, UNU/IIST visitor, from
Institute of Mathematical Sciences, Chennai, India
10:00,
Wednesday, 9th August 2000
Title: Automata which navigate the Web
Abstract:
We present a simple theoretical model of web navigation, in which
each WWW user creates style specifications which constrain web
browsing, search and navigation using the user's own judgement of the
quality of visited sites. A finite state automaton is associated with
each specification, which is presented in a two-level modal logic
making up the acceptance condition for the automaton. We show that
many interesting queries regarding the user's web search can be
answered using standard automata theory.
(This is based on a joint paper with Kamal Lodaya presented at
"Half century of automata theory: conference on implementations
and applications of automata", July 2000, London - Ontario, Canada.)
- Dr. R. K. Ghosh, UNU/IIST fellow, from IIT Kharagpur, India
10:00, Friday, 11 August 2000
Title: Formal Specification of a Zonal Routing Protocol
in Mobile Ad Hoc Network
Abstract:
The report presents the formal specifications of a new routing scheme
in a Mobile Ad hoc NETwork (MANET) using RSL. The routing is based on
the concept of static zone definition. Each zone is assumed to be
about half the size of a cell. This ensures every node can reach any
node in its neighbouring zone. The proposed routing scheme unlike
other schemes exploits knowledge of advance motion plan of nodes to
allows fast movement of nodes while route discovery is on. It employs
a novel token based protocol to control flooding during route
discovery and route reply. We are not in a position to claim about
performance at the moment as we have just completed the writing of
formal specifications. However, the exercise has led us to believe
that finding optimal configuration for restricting flooding in another
known zone based routing protocol (ZRP) could require more elaborate
empirical tuning of parameters as opposed to the scheme proposed.
Separate zone caches are also maintained to facilitate fast discovery
routes as in other route discovery and maintenance schemes.
- Andres Flores, UNU/IIST fellow, from Departamento de Informatica
y Estadistica, Facultad de Economia y Administracion,
Universidad Nacional del Comahue, Neuquév, Argentina
10:00, Thursday 17th August 2000
Title: Analysis and Specification of GoF
Structural Patterns
Abstract: Design patterns are becoming an increasingly popular tool to help
with the design of software systems. However, the standard
presentation of patterns is informal, which makes it difficult to
demonstrate conclusively that a particular problem matches a
particular pattern or that a proposed solution is consistent with a
particular pattern. In this paper we use a formal model of a general
object-oriented design to show how the properties of each of the GoF
structural patterns can be specified formally. We discuss the
specification of one such pattern, the Decorator pattern, in detail
and we also discuss a range of issues that arose while specifying
other structural patterns.
- Hoang Thi Tung Lam, UNU/IIST fellow, from Technology Institute of Post and
Telecommunication, Ha Tay, Vietnam
10:00, Friday 18 August 2000
Title: Translation for a subset of RSL into Java
Abstract:
In this talk we give some solutions for the translation
from RSL into Java. Although we do not show all solutions, we hope that
from the obtained method the reader can continue to invent more.
We use Gentle for implementing a part of the translation for RSL into Java by
continuing from the rsltc type checker made by Chris George. Therefore,
we do not need to start from the parsing phase. We assume that the parsing phase
has been completed, and we already have an abstract syntax tree made by the
type checker.
- Prof. Armando Haeberer, UNU/IIST Board member
14:30-15:30, Wed
30 August 2000
Title: The Cooperation Between Government, Industry and Academy in
Developing a Software Industry, a South American Experience.
Abstract: This presentation is based on an essay jointly written by Ms. Marcia
Ferreira and the speaker. It is about the cooperation between
Industry, Government and University in South America. This material
served as a basis for a proposal of a new type of technology
developing laboratories, founded by these three sources. Part of this
material was converted into an article which will be published by the
journal Ensaio (belonging to the CESGRANRIO foundation).
There were at least three models for analysing this cooperation: - the
so-called Sabato's Triangle, which was proposed in 1968 by Jorge
Sabato and Natalio Botana - the National Systems of Innovation
originated in two types of reality, the Japanese situation analysed by
Freeman in the book Technology and Economic Performance: Lessons from
Japan, and that of the small and highly developed conuntries of
northern Europe, and - the so-called triple helix model.
What we do is to analyse the situation in South American countries
using Sabato's Triangle and then propose a new model of laboratories
following a strategy emerging from this analysis.
- Prof Mathai Joseph, UNU/IISTBoard Member
15:30-16:30, Wed
30 August 2000
Title: The Challenge of Building Software Industry in Developing
Countries
Abstract: Tata Consultancy Services (TCS) is Asia's largest software house and
the pioneer of the software industry in India. Many other successful
software companies in India have followed the business models created
by TCS. This presentation draws lessons from the history of TCS and
from the structures created by Dr. F.C. Kohli, who has led TCS for 32
years.
- Prof Pedra Veiga, UNU/IISTBoard Member
16:30-17:30, Wed
30 August 2000
Title: Networking Technologies in Portugal
Abstract: (Not available)
- Pujianto Yugopuspito, UNU/IIST visitor from Department of Computer Science and Communication Engineering,
Graduate School of Information Science and Electrical Engineering,
Kyushu University, Japan
10:00, Fri 22 Sep 2000
Title: On the Transformation of Relational Database to
Object-Relational Database
Abstract:
Relational Database is a mature database with a rigorous specification
and is broadly applicable. But the deficient in data representation has
been known since the software application changed to object
oriented. An effort should be taken to encounter the connection
between the existing Relational Database with a new software application
that is object oriented. The transformation of a Relational Database
to an Object-Relational Database is one of the solution. It still
preserves the legacy of Relational Database while the data model has
been extended to cater the object-oriented-ness.
The transformation can be formulated in the informal and formal
levels. Informal level uses diagrams that are a common way in
producing a database. Since an informal method contains some degree of
uncertainties and is ambiguous by its nature, a formal level is
required. In the formal level, formal methods of this transformation
process can ensure the correct an unambiguous description.
We present how the formal methods can be used on that transformation
problem by formalizing the informal diagrams underlying the
databases. A further refinement on object-relational database data
model can also be reasoned by using formal methods.
- Zhang Mingyi, UNU/IIST visitor, from Southwest Normal University,
Chongqing City, P. R. China, and also from Guizhou Academy of
Sciences, Guiyang, Guizhou, P. R. China
10:00, Wednesday, 27 September
2000
Title: Default Logic and its
Applications
Abstract:
Representation and reasoning of commonsense knowledge have become one
of the most familiar concepts in AI, and also a major challenge for
the research on new intelligence systems. An important and useful
logic-based approach to formalising commonsense reasoning is to use
the nonmonotonic logic. Among the most famous formalisms for
nonmonotonic reasoning, Reiter's default logic is the most natural and
simple one. It represents nonmonotonic rules by special inference
rules, called defaults, of the form A(x):B(x)/C(x), where A(x), B(x)
and C(x) are formulas from some logical language, and x is their
vector of free variables. Unlike classical inference rules, defaults
are rules that might have exceptions.
In this talk, we focus on default logic and its applications, since it
has been argued that default logic has the same expressive power as
other main nonmontonic formalisms. First, we give a brief introduction
to Reiter's default logic and its variants. We argue why we use
default logic, and what are its advantages and drawbacks. Second, we
propose another research approach to default logic. Following our
approach, some important open problems on the existence of extensions,
computability and complexity of main reasoning task for general
(non-normal) default theories in Reiter's framework and its variants,
etc, can be solved. Third, we present a uniformed semantical framework
for various default logics, which is based on Kripke's semantics
idea. Last, we give some implications of default logic by developing
proof methods: the so-called Truth Maintenance Systems, and
negation-as-failure in logic programming and deductive databases.
The talk is a survey on our recent work in the topic of default logic.
- Chris W George, UNU/IIST staff
17:00, Wednesday 4 Oct
2000
Title: Formal Specification of a Query Expression Generator
Abstract: Many Query languages work on the assumption that the user has a
knowledge of the database that is being queried and he uses the system
by typing in queries following a predefined format on the different
fields of the database. In this report we have defined a grammar for
describing the structure of a database, a term generator that
generates from a database structure a set of terms that can be
combined into queries, and a query generator that generates from the
combination of terms selected by a user a corresponding query
expression.
All this is done in the RAISE specification Language.
- W. Eric Wong, UNU/IIST visitor, from
Telcordia Technologies
Morristown, New Jersey, USA
15:00, Friday, 20 October 2000
Title: Advanced Techniques for Creating Dependable Software
Abstract:
Studies have shown that approximately 20% of a software system
is responsible for 80% of the faults; and over the lifetime
of an average software system, as much as 70% of the cost is
estimated to be dedicated to testing and maintenance. Experience
also indicates that the cost-benefit of code coverage testing of
unit code is very good, but usually levels above 80% code coverage
can be quite difficult to achieve. Clearly, an appropriate methodology
ought to be employed to address these high-leverage concerns. With
the increased emphasis on software quality and the pressure to deliver
software faster and cheaper, such a methodology should encompass
software design, architecture, development, testing, and maintenance
as a whole, and provide an integrated solution that leads to the
creation of more dependable software in a more effective way.
In this talk, I will discuss techniques aimed at helping software
practitioners accomplish the above goals.
Speaker's Biography
W. Eric Wong received his B.S. in Computer Science from Eastern
Michigan University, and his M.S. and Ph.D. in Computer Science
from Purdue University. He is currently a Research Scientist in
the Software Environment Research Group at Telcordia Technologies
(formerly known as Bellcore). His research interests are in
design metrics analysis, software testing, reliability,
debugging, maintenance and program comprehension.
Dr. Wong is one of the principal investigators at Telcordia
responsible for developing a set of metrics to evaluate
the overall quality of highly complex telecommunication systems
and to identify their fault-prone software modules.
He is also the key person for developing metrics for better
system understanding. Such metrics provide quantitative measurements
for the closeness between program features and program components,
as well as the overlap between different features.
Dr. Wong's work in software reliability includes studies on
predicting the reliability of heterogeneous software systems based
on the architecture and the failure behavior of their components,
and studies on the impact of testing coverage information and
different testing techniques on reliability analysis.
Results of his previous work in software testing, such as the impact
of code coverage on fault detection effectiveness and methodology for
selecting effective regression tests, have been integrated into
Telcordia's Software Visualization and Analysis Toolsuite.
In 1997, Dr. Wong received the Quality Assurance Special
Achievement Award from Johnson Space Center, NASA for his efforts in
helping software engineers at JSC improve the quality of their software.
- Yumbayar Namsrai, UNU/IIST visitor, from National University of
Mongolia
10:00, Thusday 16 November 2000
Title: Undergraduate Software Engineering Curriculum for Developing Countries
Abstract:
A number of professional computer societies and institutions have
given recommendations on how to design university curricula in
computer science and software engineering, and have also proposed
various model curricula based on these recommendations. However, these
are essentially aimed at universities in industrialised countries, and
in general it is difficult to apply them directly in developing
countries where quite different conditions apply. In this talk, we
give an overview of some of the recommendations, and we describe a
model curriculum in software engineering which is based on these but
which is specifically intended for use in universities in developing
countries. We also indicate how universities wishing to establish a
new computer science department can work towards this gradually by
introducing this curriculum over a number of years.
- Nitesh Shrestha, UNU/IIST fellow, from Birla Institute of Tech and Sci, Computer Science,
Master of Engg in Computer Science, Nepal
10:00, Monday, 27 November 2000
Title: Model-Based Travel Planning
Abstract:
Internet provides today's travellers with a great deal
information in support of travel planning. With so many options
available, finding the optimum solution to one's travel requirements
can be quite a challenge. In this talk we present a model-based
approach to systematic travel planning. The approach is: (1) minimal -
models are expressed with the minimum number of concepts; (2) formal -
the concepts have their meaning defined in mathematics; (3)
wide-spectrum - models capture all levels of abstraction from initial
requirements to final itineraries; (4) incremental - development
proceeds by making the requirements more concrete; (5) sound -
development applies the rules which guarantee that the final itinerary
satisfies the requirements. We present the models with formal
definitions in RSL and example applications. We also present a
prototype implementation of the model-based travel assistant, written
in emacs LISP.
- Ly Yongjian, UNU/IIST fellow, from ShangHai Jiaotong
University, China
10:00, Wed 29 Nov 2000
Title: An Operational
Semantical Model of Verilog
Abstract: In this paper, we present an
operational semantics of a non-trival subset of Verilog using the
approach proposed by Plotkin. We also preovide a model of
observation for open Verilog processes,and use observation
equivalence based on bisimulation to identify programs of the same
behaviour. The observation equivalence can be proved to be a
congruence for all verilog operators, so it provides a sound base
for deriving the algebraic laws for Verilog processes.
- Univan Ahn, UNU/IIST fellow, from Physics Faculty, Kim Il Sung University, Daesong District, Pyongyang, DPR Korea
10:00, Thu 30 Nov 2000
Title: C++ Translator for RAISE Specification Language
Abstract:
RAISE includes a wide spectrum specification language (RSL),
a method for the rigorous development of software systems, and a set of
accompanying tools. This report presents an implementation of a C++
translator for RSL. We used the GENTLE Compiler Construction
System to implement the translator and took the RSL type checker
as a starting point.
- Adegboyega Ojo, UNU/IIST fellow, from dept. of computer
sciences, faculty of science, university of Lagos, Akoka - Lagos,
Nigeria
15:00, Friday, 1 December 2000
Title: Distributed Production with Specification-Generated Processes
Abstract: We consider the problem to organize production among a set
of production cells to meet a given production goal. Each cell has a
limited capacity to store, manufacture and deliver products, and it
can interact with other cells by means of information and logistics
networks. The goal specifies the type of the product and the volume
required. We propose a solution to this problem in the form of an
algorithm which given a goal and a cell generates a sequence of
operations on the cell to implement this goal. Lacking the resources
locally the algorithm generates some auxiliary goals which it then
communicates to other cells, involving generating (recursively) more
processes and more goals etc. Lacking the resources globally, the
algorithm generates the goals to be satisfied by the environment. We
provide a formalization of the problem, propose a solution, offer
correctness arguments and present an email-based implementation. We
also describe some real-life applications.
- Phan Cong Vinh, UNU/IIST fellow, from Vietnam National
University-HCM City, Computer Science Dept., Ho Chi Minh City, Vietnam
15:45, Friday, 1 December 2000
Title: Protocol-Based Cooperation in a
Virtual Manufacturing Organization
Abstract: Cooperation between the members of a virtual manufacturing
organization can be described as following a certain protocol. In this
talk with investigate how it is possible to model such protocols
explicitly, for an organization modeled as a client-server system
where one member (a client) can request another (a server) to fulfill
a certain production goal. The goal describes the type of the product
and its required quantity. It is up to the server to decide if and how
to implement this goal. We present several protocols how the servers
can react to such requests and the clients receive their responses. We
also discuss how the choice of a protocol affects the behavior of the
whole organization.
- Hong Ki Thae, UNU/IIST fellow, from Computer Science Institute,
Academy Sciences DPR of Korea, Pyongyang, Unjong District,
Gyangmyong-dong, PRK
15:00, Monday, Dec 4th 2000
Title: Formal design of Hybrid Control Systems :
Duration Calculus
Abstract: A hybrid controller is a control program implemented on digital
computer for the control of physical plant. Recently the computer
embedded systems are increasingly used. The major part for such
systems is supervisor which performs logic control functions. Even if
the main part of the automation software is for continuous control, it
must be supported by discrete control logic which is responsible for
the supervision of control system components with respect to violation
of safety or performance conditions. Both from the point of view of
economic plant operation and of safety, it is highly desirable that
the control software, which performs logical operations on the plant,
works correctly.
Practice shows us design errors in such discrete control logic are
much more costly than in continuous controllers.
In this paper. We
present an approach to the design of hybrid system by combination of
many comprehensive formalization techniques. We use Duration Calculus
to specify of requirement and design and to model controller at
abstract level of system development. Then the high level designs are
further refined in control theory. A formal verification may be done
either in DC if it is possible, or in predicate calculus using the
semantics of DC or theorems from control theory . We ha show how
our combination techniques work and how the designs in DC are refined
into practically implementable hybrid controller design in a double
water tank case study which is one of the bench mark problem for
morden process control engineering.
- Gabriela Aranda, from Departamento de Informatica
y Estadistica, Facultad de Economia y Administracion, Universidad Nacional del Comahue, Neuquév, Argentina
10:00, Thursday 14 December 2000
Title: Specification of GoF Creational Patterns and Compound Patterns
Abstract:
Design patterns are a popular tool to help with the design of software
systems. However, the standard presentation of patterns is informal,
which makes it difficult to demonstrate conclusively that a particular
problem matches a particular pattern or that a proposed solution is
consistent with a particular pattern.
This talk reports on the continuation of the project on the
formalisation of design patterns, earlier work on which has seen the
development of a formal model of a generic OO design, formalisation of
how to link a design to a single pattern, and formal specifications of
GoF behavioural and structural patterns. We first of all report on the
specification of the third and final group of GoF patterns, the
creational patterns, then we go on to discuss an extension to the
basic model which allows a design to be matched against many possibly
overlapping patterns (including compound patterns) simultaneously.
- Virginia Mauco, UNU/IIST fellow, from Facultad de Cs. Exactas -
UNCPBA, Campus Universitario - Paraje Arroyo Seco, (7000) Tandil,
Pcia. Buenos Aires, Argentina
11:15 Thursday 14 Dec 2000
Title: Deriving an initial specification
Abstract: Formal methods help to increase software quality and reliability.
However, during the first stages of development when the interaction
with the stake-holders is very important, the use of client-oriented
techniques would be very useful to improve the communication between the
stake-holders and the software engineers.
In this report we analyse and develop the integration of client-oriented
requirements engineering techniques with formal specifications written
in the RAISE Specification Language. We present a preliminary set
of heuristics to help in the definition of an initial specification of
a given domain. We show how to derive types and functions, and how to
structure them in modules, starting from two models belonging to the
Requirements Baseline: the Language Extended Lexicon and the Scenario
Model. A Milk Production System, one of the components of the
Agricultural System Infrastructure, is the selected domain to carry out
this study
