- Dr. Vladimir Zadorozhny, UNU/IIST fellow, from Institute for
System Programming, Russian Academy of Science, Russia
Monday, 20 Jan
1997
Title: Issues of Meta-Upgrade
Abstract: During the development of
application software systems (or, just applications), it seems
quite natural to separate
- applied semantics of application, or PRAGMATICS (what kind
of real-life problem it should solve), and
- system semantics of application, or "details" of
IMPLEMENTATION (e.g., persistency, data access, distribution,
etc.)
Though pragmatics dominates in this pair, main problems of
development are usually resulted from "second-class"
implementation details. The quotation marks reflect the common
trend, under which implementation often push pragmatics off to
backstage, and even put it under. It results in hard development,
as well as bad controlled and contradictional system evolution
(the most impressible example is the problem of legacy systems).
The Meta-Upgrade (MU) Technology is an approach to development of
open integrated object systems. It adopts the idea of
IMPLEMENTATION TRANSPARENCY for application developer and is
significantly based on Metaobject Protocol Technology.
MU-Technology allows to extend initial applied semantics by
connecting the application objects to different metaobject
contexts in systematic, flexible and efficient manner.
It should be noted that well-known Common Object Request Broker
Architecture (CORBA) can be considered as a special case of
MU-Technology aiming to DISTRIBUTION TRANSPARENCY. In this
connection we consider how it is possible to extend CORBA
Interface Definition Language (IDL) to support general
meta-upgrade activity (in particular, for purposes of
semantics-based reasoning).
- Kaare Sloth Jensen, UNU/IIST fellow, from Danish Technical
University
Wed, 29 Jan 1997
Title: On a model for Agents which Trade
Resources
Abstract: In this colloquium, ongoing work will be presented.
The work concerns a model of resources and agents which trade
these resources on markets. Possible application for this model
within the domain of trading include: market simulation and
automatic electronic trading. There are, however, also prospects
that the model may be of use as a general computation model
comparable to the multiset/coordination models of computation
known from the literature (Chemical Abstract Machine, Gamma,
Linda, ..).
- Bo Stig Hansen, UNU/IIST Research Fellow
Fri, 31 Jan 1997
Title: Some
Experiences in Domain Modelling before Requirements Capture
Abstract: In
this colloquium, we report on some experiences from a project
regarding requirements definition for an accounting system. In the
project, a domain model for accounting was developed and this was
used as a basis for formulating the requirements.
- Prof. Alexandre Zamulin from Novosibirsk Academy
Tue, 18 Feb
1997
Title: Introduction to Multi-Level Specifications
Abstract: A multi-level
specification language provides two or more levels of specification
in contrast to conventional specification languages supporting only
one level of specification. The language Ruslan designed by the
author is one of the first multi-level specification languages. It
possesses such features as modularity, overloading, higher-order
functions, polymorphism, type and kind classes, and subtypes. The
specification level 1 is represented in Ruslan with specifications
of data types, type classes, and independent functions. The
specification level 2 is represented by specifications of kinds
which are types of types. The higher specification levels introduce
kinds of kinds. Algebraic background of multi-level specifications
and conventions used in the specification language Ruslan are
discussed in the talk.
- Prof. Alexandre Zamulin from Novosibirsk Academy
Wed, 19 Feb
1997
Title: Experience in Multi-Level Specifications
Abstract: The purpose of the
talk is to illustrate the need and use of the multi-level
specification technique introduced in the first talk for the
specification of some constructs typical of programming languages
and data models. The necessity for three levels of specification is
illustrated in the talk with the specification of Pascal-like range
types. Record types are an interesting object of specification
because they themselves are subjects of some operations specified at
level 2. Third example illustrates the use of record types for the
specification of the relational data model.
- Prof. Alexandre Zamulin from Novosibirsk Academy
Thu, 20 Feb
1997
Title: Typed Gurevich Machines
Abstract: A Typed Gurevich Machine is
represented with a type-structured algebraic specification augmented
by a number of transition rules of a conventional Gurevich Machine
(previously known as Evolving Algebras) indicating in which way an
algebra of a given signature evolves to another algebra of the same
signature. A function update is a primitive algebra transformation.
Two classes of functions are distinguished, static functions which
do not change when an algebra evolves, and dynamic functions which
do change when an algebra evolves. Data type operations are static.
The semantics of data types and static functions is given by axioms,
the semantics of dynamic functions is given by transition rules.
- Prof. Arne Solvberg, from The Norwegian University of Science and
Technology (NTNU), Trondheim, Norway
Monday 24
February
Title: Information Systems Engineering: a discipline in a
methodological evolution
Abstract: Decreasing costs of computers and
telecommunication have led to a deep penetration of information
technology in our society, both in the workplace and in the private
sphere. Information can be made available for little cost to
everybody by everybody. Information systems are established by
integration of commercially available software components. Computers
and people interact closely and they influence on each others
behaviour. Organisations are restructured into networks of
cooperating autonomous units. Competition is global. Information
system engineering comprises design of business processes,
organisation, patterns for human-computer interaction, as well as of
data system design. Information systems engineering is transformed
into a multi-disciplinary design discipline which increasingly will
be based on formal system models and common engineering approaches.
The talk will be based on seeing Information Systems Engineering as
a technical discipline rather than a discipline of (computer)
science. A few highlights from ongoing research will be presented as
well, from workflow modeling and data warehousing.
- P.H. Leung, from Hong Kong Polytechnic Univ., Hong Kong
Monday. 21 Apr 97
Title: The Domain Modeling of Air Traffic Control: A
Formal Approach
Abstract: A software development method which helps
assuring the correctness of the systems developed with little
dependency on domain users and supports high re-usability of
software components is expected. The rationales are as follows.
Domain users make a lots of assumptions and common sense in their
work. These assumptions and common sense are usually not mentioned
to software developers, and hence they are omitted in software and
lead to errors. Re-usability of software is low. This leads to
expensive development. Furthermore, experience of a domain learned
in one development is not systematically carried forward to another
project. This makes repeated occurrence of the same problem in
different projects and makes training expensive.
In this seminar, a method which splits requirement capture into
domain modeling and requirement definition will be presented.
Domain models are models of the real world domain. They are
expressed in terms of software specification languages and have well
defined semantics. They are used to tackle the mentioned
problems.Requirements can then be defined precisely by the
components of these domain models. Consequently, reliable software
can be developed from the domain models and requirement definitions
by formal refinements technique. The principles of this development
method, first, will be presented. Based on these principles, a
domain modeling method and requirement definitions will be
discussed.
- Arun Kumar Pujari, UNU/IIST fellow, from University of Hyderabad,
India
Tuesday, 22 Apr 97
Title: Reasoning with qualitative temporal
information
Abstract: This lecture aims at presenting a survey of the work
done on the algorithmic aspects of Interval Logic. Several
formalism for expressing and reasoning about temporal constraints
have been proposed in the literature. They can be classified either
according to the types of temporal constraints they deal
(qualitative, quantitative or both) or according to the types of
temporal elements they consider (intervals , points or both).
Allen(1983) proposed a formalism for dealing with qualitative
temporal information and this is known as Allen's Interval Logic.
Vilain and Kautz in 1986 proposed Point Algebra and later, discussed
about a SIA (pointizable algebra). There have been some more
formalisms such as ORD-Horn formalism, Binary Disjunctive Formalism
etc. However, there has been always a tradeoff between
expressiveness and computational effectiveness. Though the Interval
Logic (Interval Algebra) can be thought of as the largest class
among these, the algorithms for reasoning ( minimal consistent set
or, reporting satisfiability) have remained intractable. On the
other hand, Point Algebra, SIA etc. admit efficient algorithms for
reasoning. The research is to reach a level of reasonably expressive
model with tractable algorithm.
The aim of this presentation is briefly review the different
approaches and algorithms and highlight the unsolved problems. It is
also show its extension to spatial reasoning and hence, in GIS.
- Prof. Jose Nuno Oliveira, UNU/IIST Visitor, from the University
of Minho, Portugal
Tue 6 May
Title: Formal Specification, Rapid
Prototyping and Program Calculation - an Industrial Experiment using
the CAMILA/SETS Approach
Abstract: This talk reports on INESC 2361 group's
experience on using formal methods throughout a large Eureka project
(EU 379) whose partners were software companies neither trained nor
interested in such methods.
The main target of the consortium was the design and implementation
of an object-oriented meta-CASE system which should include a
mechanism for comparing, classifying and retrieving arbitrary
information concerning large software systems. The unit of
information in such a system should combine the so-called "enumerative"
and "faceted" classification schemes proposed elsewhere for large
library systems. This entailed the introduction of fuzzy logic in the
underlying-object model, in order to cope with features of human
reasoning such as "classifying by analogy" and "terminological
vagueness".
Encharged of specifying the system's overall architecture from the
early stages of the project, INESC researchers decided to produce a
formal specification specially concerned with keeping the fuzzy
behaviour of the system unambiguous. Lack of communication with INESC
partners was solved by deriving a CAMILA prototype from the system's
specification (CAMILA is a rapid prototyping shell which animates part
of the SETS design calculus) which was disguised behind a UI layer
running on Windows 3.1.
This proved to be a good strategy. Early feedback on the hard
technical subtleties of the design (as unveiled by the formal
specification) could be obtained by our partners by observing
the prototype's behaviour. The overall exercise included the
"reverse specification" and CAMILA prototyping of other sub-systems
(such as eg. the underlying object-repository server) which could thus
be integrated in the (then rather slow but still very useful!)
prototype. Eventually, all main implementation decisions could be
validated by calculation (in SETS). In the system's final prototype,
running on Windows 3.1, all CAMILA code gave room to C++ code.
This R&D contract remains INESC 2361 Group's best experience on
collaborating in heterogeneous consortia involving partners unused
to formal software design methods.
- Prof. Jose Nuno Oliveira, UNU/IIST Visitor, from the University
of Minho, Portugal
Wed 7 May
Title: An Experiment in CAD Tool Formal
Specification
Abstract: 3D graphics, multimedia and virtual reality are
available thanks to enormous advances in hardware support. There is
an overwhelming offer in the CAD market for architects and civil
engineers -- eg. AutoCAD, AutoARQ, AutoVision, 3D Studio,
PowerPak, ... But, are this tools working at the right level of
abstraction? Are building descriptions doomed to be represented by
(huge) collections of low-level graphical entities? Or do they
possess an intrinsic, high-level "algebraic structure" which is
simple and can be reasoned about?
This talk illustrates the application of *formal methods* to the
stepwise development of a simple CAD tool for building-specification
and automatic building-plan plotting in which house designs are
described by mathematical expressions written according to a house
design *algebra* and subject to invariant properties which check for
building well-formedness.
A formal model is developed (later prototyped in a rapid-prototyping
shell) which has mainly to do with automatically generating building
plans from abstract descriptions. At prototype level, this is first
achieved by structurally calculating LaTeX picture format drawings as
a pictorial semantics of the abstract descriptions. In a second phase,
the adopted output graphical server is the Autocad (TM) system.
Our experience has been that, not only formal methods greatly
increased confidence on the building-description language correctness,
expressive power and conciseness, but also rapid prototyping provided
good feedback on what was being designed, at a very low cost.
- Prof. Jose Nuno Oliveira, UNU/IIST Visitor, from the University
of Minho, Portugal
Thu 8 May
Title: Formal Calculi Applied to Software
Component Knowledge Elicitation
Abstract: For many years, traditional
software development has been based on informal, graphical
notations such as E-R diagrams, DFDs, flowcharts etc. supported by
CASE tools. However, most CASE systems are oriented towards
production-management rather than to the end-product. This may be
so because their designers couldn't probably understand what a
software product "really is". Because software modules are recorded
as raw files, their essence is never recorded. Software companies
end up with massive repositories of "drawings" which cannot be
searched for and therefore are hardly re-used.
This talk reports on a formal-method-based strategy devised for
such large "drawing" repository re-engineering. The work was carried
out by INESC group 2361 for an Italian software company. Our
experiment was focussed on E-R diagrams and was based on a SETS
calculus semantics for such drawings. This made it possible to reason
about such informal pieces of information and, in particular, to
introduce hierarchical classification into E-R diagram repositories,
supported by a software design calculus. Some effort was also put on
developing tools for semi-automatic assistance in such a process
which, however, could never be tested on a large scale basis.
- Prof. Jose Nuno Oliveira, UNU/IIST visitor, from the University
of Minho, Portugal
Wed 14 May
Title: A Calculational Approach to Reverse
Specification
Abstract: The Student Records Office of Minho University has
run for many years on top of a "home made" information system which
was, until a couple of years ago, by and large undocumented. The
situation became more and more risky until three final year
students were encharged of the process of reversing the underlying
Oracle code (under my supervision) and of recording as much of the
missing information as possible.
Two of these students used 'ad hoc' techniques while one of them
resorted to formal methods. The strategy here focussed on reversing
the database structure by "inverse calculation" in the SETS
(inequational) calculus. This started by inferring low level
SETS expressions directly from the Oracle data. Then laws of the
calculus were triggered "from right to left" (that is, by replacing
an instance of B by an instance of A in a law A < B, which means
"B implements A") sometimes requiring the conjecture of low-level
invariants which the other members of the team confirmed by intuition.
The outcome of this systematic exercise was a concise formal
specification of the whole system structure, which was subject to two
subsequent experiments:
(1) the "RIAPA", a document containing the University's rules
for student assessment and course follow-up, could eventually be
formalized as a non-trivial datatype invariant written on top of
the formal specification derived by inverse calculation;
(2) subject to "forward engineering" again, one would calculate
a smaller database system saving a good deal of redundant data.
On the whole, informal and formal methods blended well in rescuing
this information system from eventually collapsing down.
- Prof. Jose Nuno Oliveira, UNU/IIST Visitor, from the University
of Minho, Portugal
Fri 16 May
Title: Can Distribution be (Statically)
Calculated?
Abstract: A potential application of software calculi such as
SETS concerns *horizontal refinement*, that is, the decomposition
of large software systems in terms of re-usable *components*. Many
laws of SETS work in this direction, particularly the ones which
"push the product construct outwards", possibly leading to
exponentiations. This is because they help in factorizing complex
state structures of monolithic designs into collections of simpler
structures which may have been dealt with already, and may thus be
re-used.
This talk reports on on-going research which seems to provide
evidence that the "amount of concurrency" gained in a *horizontal
refinement* step can, if expressed in SETS, be calculated and
reasoned about. We base our concept of communication and
synchronization on (categorical) product and exponentiation.
Hash-tables are provided as a suggestive illustration of the
exponentiation-type of concurrency. A hashed data-structure, regarded
as a monolithic structure, can at compile-time be factored into a
collection of n-similar (sub-)structures -- a kind of "fractal"
effect on data structuring -- which can be regarded as concurrent,
communicating processes. This (usually ignored) "gain in concurrency"
is the fact that operations on disjoint collision sub-structures are
independent and can overlap in time. Regarding the hash-effect as
mere data optimization is thus a limited view of hashing. Instead
of "data hashing" one should talk about "process hashing".
- Professor Jan Bergstra, UNU/IIST Visitor, from University of
Amsterdam, Programming Research Group, The Netherlands
Tuesday, 20
May 97
Title: An introduction to process algebra, style ACP
Abstract: We will
discuss the principles of ACP style process algebra and its main
operators in the time free case. This will involve atomic actions,
alternative composition, sequential composition, parallel
composition and encapsulation. Further features will include
iteration, state operators, conditions and priorities.
- Professor Jan Bergstra, UNU/IIST Visitor, from University of
Amsterdam, Programming Research Group, The Netherlands
Wenesday,
21 May 97
Title: Process algebra with discrete time
Abstract: We will discuss a
relative discrete time version of process algebra as well as a
version using absolute discrete time. Special emphasis is on
expansion axioms for the merge (parallel composition) and its
auxiliary operators left merge and communication merge. We
introduce two notations for discrete time process algebras. One is
suited for the purpose of axiomatisation, the other one for
practical work. Abstraction in discrete time is discussed as well.
- Professor Jan Bergstra, UNU/IIST Visitor, from University of
Amsterdam, Programming Research Group, The Netherlands
Thursday,
22 May 97
Title: Process algebras for real time and real space
Abstract: In
real time and real space process algebra the actions have a
temporal coordinate respectively a temporal and three spatial
coordinates. We discuss the problem of axiomatisation and we
provide several examples. We will distinguish three formats:
absolute, relative and parametric time. The use of state operators
and priorities is illustrated for the description of asynchronous
communication.
- Professor Jan Bergstra, UNU/IIST Visitor, from University of
Amsterdam, Programming Research Group, The Netherlands
Friday, 23
May 97
Title: Parametric time, signals and conditions
Abstract: We discuss
parametric discrete time process algebra, which is the integration
of absolute and relative discrete time. We present the time
spectrum expansion of a process. The mechanism of signals emission,
conditions and signal inspection will be presented in the untimed
case first, its adaptation to the timed case is discussed as well.
That adaptation has been among the topics of research of Middelburg
and his fellows at unu-iist in recent months.
- Professor P S Thiagarajan, UNU/IIST Visitor, from Institute of
Math, Madras, India
Tue, 20 May 97
Title: A Product Version of Dynamic
Linear Time Temporal Logic
Abstract: We present here a linear time temporal
logic which extends the propositional temporal logic of linear time,
along two dimensions. Firstly, the until operator is strengthened by
indexing it with the regular programs of propositional dynamic logic
. Secondly, the core formulas of the logic are decorated with names
of sequential agents drawn from fixed finite set. The resulting
logic has a natural semantics in terms of the runs of a distributed
program consisting of a finite set of sequential components that
communicate by performing common actions together. We show that our
logic, denoted DLTLotimes, admits an exponential time decision
procedure. We also show that DLTLotimes is expressively
equivalent to the so called regular product languages. Roughly
speaking, this class of languages is obtained by starting with
synchronized products of (omega-)regular languages and closing
under boolean operations.
- Souleymane Koussoubé, UNU/IIST fellow, from African's
Institute of Computer Science (IAI), Gabon
Tue, 27 May
97
Title: Knowledge-Based Systems : Formalisation & Application
Abstract: After
an overview of Knowledge-Based Systems (KBS), we will present a
formal model (at different levels of abstraction) of such systems.
We will address such aspects of a KBS as knowledge representation,
coherence, inference, ... We will present an application of KBS to
Insurance domain as well.
- B. Warinschi, UNU/IIST fellow, from University of
Bucharest
Tuesday, May 27, 97
Title: Timed frames and transition systems
Abstract: Frames are a convenient way to represent transition systems. A frame
model and a graph model for discrete time process algebra are
presented in order to convey the algebraic manipulation capabilities
of frames. Timed frame models can be used in order to give formal
semantics for SDL.
- R. Soricut, UNU/IIST fellow, from University of
Bucharest
Tuesday, May 27, 97
Title: Discrete Time Network Algebra for
Timer Handling in SDL
Abstract: We propose a process algebra model of
asynchronous dataflow networks as a semantic foundation for the
specification language SDL. The model, which extends a model of
network algebra, is close to the concepts around which SDL has been
set up. It is able to cover all behavioural aspects of SDL except
process creation.
- Y.S. Usenko, UNU/IIST fellow, from Taras Shevchenko University
of Kyiv
Tuesday, May 27, 97
Title: Discrete time process algebra and the
semantics of SDL
Abstract: A process algebra semantics of phiSDL
without channels (phi-SDL) is presented. The presented
semantics is suitable for generating finitely branching transition
systems for specifications in phi-SDL, and proving statements
about them. The presented semantics is grounded on the proposed
combination of the extensions of process algebra with discrete
relative time, conditions, signals, state operator and counting
process creation operator.
- Hoang Thi Tung Lam, UNU/IIST fellow, from Posts & Telecomms
Training Centre 1, Hatay, Vietnam
Wed, 28 May 97
Title: Specification of
a Switching Communications System
Abstract: Nowadays electrical
communications systems are being used more and more widely to
provide global connections between very large numbers of people. In
order for such systems to operate efficiently and effectively,
control must be distributed to local sub-networks, with each
sub-network being responsible only for a small part of the system
and passing on the responsibility to some adjacent part of the
system whenever it is unable to perform the whole of a requested
task itself. In this talk we describe a generic hierarchic
communications system which is structured in this way and the
message-passing mechanism by which responsibility is delegated. We
also give a brief overview of a formal specification of this in RSL.
- Prof. Leonid A. Kalinichenko, from Institute for Problems of
Informatics, Russian Academy of Sciences
from Mon, 2 Jun to Thu, 5
Jun, 1997
Title: Development of semantically interoperable information
systems
Abstract: The gap between existing Object Analysis and Design (OAD)
methods applying mostly top-down technique and the demand of the
middleware interoperation architectures and methodologies for the
development based on a composition of interoperating components
remains to be large.
A number of various computational, data and knowledge models based
on an object paradigm is continuously increasing. These models are
used for development of software and data services, information
systems and their subsystems that technically can easily become
components of the middleware. Such heterogeneity and lack of
well-defined semantics of the respected models creates a big
obstacle for their interoperability.
But probably the largest obstacle for the interoperability of
components consists in the application semantics of components
technically interrelated through the middleware. Reconciliation of
their application concept base that is an obvious prerequisite for
their interoperation constitutes a problem.
The approaches to fill in the gaps mentioned are briefly overviewed.
We strictly distinguish between application semantics and object
model semantics.
Using the "canonical" model we believe that terms widely used in
various object models need to be carefully defined to give them
precise semantics. To give the canonical model exact meaning, we
construct a mapping of this object model into the B AMN notation
providing precise meaning for the language. Thus, we get the semi
-formal object model and its formal counterpart that we can use
together as a common paradigm for:
- uniform representation of various object models;
- uniform specification of pre-existing components;
- different models used on the phases of requirement planning,
analysis and design of the information systems.
The concept of refinement of the specifications relying on the
pre-existing components becomes inherent for the model.
An approach of mapping of existing object models into the canonical
one is discussed.
Application semantics of components we consider separately in frame
of the ontological approach. Semi-formal and formal (model- based)
specifications for concepts are provided. We base the ontological
model we introduce on the canonical object model.
Component-based information design issues in the semantically
interoperable environment are briefly discussed.
Type specifications and their reducts are chosen as the basic units
of specification manipulation. The `algebra' of type specifications
is introduced for that. Reducts of the component type
specifications are used as minimal fragments potentially reusable
for the respected reducts of the analysis model types. Process of
design of the semantically interoperable information systems is
discussed.
- Dr. Xu Qiwen, UNU/IIST Research Fellow
Thu, 5 Jun 97
Title: Introduction to the hardware description language Verilog
Abstract: Modern
hardware design uses hardware description languages to describe the
systems at various abstraction level. A hardware description
language is an extension of conventional programming languages with
concurrency, real time and hardware-oriented data structures.
Typically, the design paradigm is: 1, describe the system at a high
level concentrating on logical behaviours; 2, simulate the high
level design using the simulator of the description language; 3,
re-code the design at a lower level; 4, simulate the lower level
design; 5, synthesis the hardware. A challenge is how to use formal
methods as a complement to simulation.
Verilog is the most widely used hardware description language in
industry (reportedly having 2 times business of VHDL), and it needs
support of formal methods in various aspects. This talk introduces
the language with several examples.
- Mark Greenstreet, UNU/IIST Visitor, from Department of Computer
Science, University of British Columbia, Canada
Mon, 16 Jun 1997
Title: Verifying that Continuous Circuits Implement Discrete Behaviors
Abstract:
High speed digital designs increasingly rely on circuits whose
analog behavior is critical to their correct operation and
performance. Typically, circuit simulators such as SPICE are used
to verify that a circuit in an analog model correctly implements a
digital behavior. Such simulation based approaches are tedious and
cannot account for all possible inputs, loads, or model parameters.
In this talk, I will show how dynamical systems theory can be used
to establish the digital behavior of analog circuits. In this
framework discrete behaviors correspond to topological properties of
the continuous, and I will present an practical algorithm for
verifying these topological properties. This approach allows
traditional SPICE models to be used for transistor behavior, and the
circuit can be verified for a large range of inputs or model
parameters. I will illustrate the approach using Seitz's arbiter
circuit and the high speed, Yuan-Svenson toggle element as examples.
- Chris George, UNU/IIST Senior Research Fellow
Tue, 24 June
1997
Title: Combining and distributing hierarchical systems
Abstract: It is
possible with RAISE to specify and do most refinement in an
applicative framework, and then transform the concrete applicative
specification into an imperative sequential or concurrent one. This
transformation changes from a style more appropriate to proof of
refinement to a style more appropriate to implementation.
The resulting imperative specification is typically hierarchical,
with upper levels calling the functions of lower ones. This talk
illustrates a further stage of development in which the hierarchical
structure is transformed into a distributed one, and components
communicate asynchronously. This also allows "horizontal"
communication between components of previously separate hierarchies.
A major design aim is to reuse the hierarchical specification, as
far as possible extending the existing modules by standard, generic
components. The method should achieve correctness by construction,
and be amenable to quality control.
The method is illustrated by collaborative work done between
UNU/IIST and the Vietnamese Ministry of Finance in developing a
specification of a national financial information system.
- Marisa Sanchez, UNU/IIST fellow, from Universidad Nacional Del
Sur, Baha Blanca, Argentina
Thu, 26 June 97
Title: Specification-based
Testing
Abstract: We will discuss algebraic specification based testing with
particular attention to the approach described by Gilles Bernot,
Marie Claude Gaudel and Bruno Marre, which presents a theory and a
tool for testing programs against formal specifications. The aim of
this presentation is to briefly describe some issues concerned with
the application of this approach in a RAISE (Rigorous Approach to
Industrial Software Development) development.
- Aristides Dasso, UNU/IIST fellow, from Universidad Nacional de
San Luis, Argentina
Thu, 26 June 97
Title: A Course on Formal Methods
Using RAISE
Abstract: An introductory course on Software Engineering using
Formal Methods. The course includes an example (Credit Card) of a
RSL specification, as well as some teaching materials.
- Gueorgui Satchok, UNU/IIST fellow, from Minsk, Republic of
Belarusia
Wednesday, 25 June
Title: Metropolitan In-street On-route
Passenger Transport: Monitoring and Control
Abstract: Monitoring and control
of metropolitan in-street on-route passenger transport is among the
most acute problems that cities face today. In this talk we present
a simple domain model for metropolitan transport, show how the model
helps specifying applications in this domain, and how development
from the shared domain model facilitates integration of the set of
applications to solve a practical task. The task is control and
monitoring of on-route passenger transport and the work is carried
out using RAISE.
- Ou Song, UNU/IIST fellow, from South China University of
Technology, Guangzhou, PRC
Wednesday, 25 June
Title: Formalising the
Process of Software Design: Implementation, Analysis, Automated
Support
Abstract: We present an RSL model for the software design process,
as carried out within a pair of formal languages: one
property-oriented to write design requirements and one
model-oriented to write design decisions, and within any semantic
theory to prove such decisions correct. A software process is a
sequence of steps to turn a property into design, using a mixed
notation and gradually replacing property-oriented constructors by
model-oriented. The model is to help analysis, design and
automation of a software process.
- Yumbayar Namsrai, UNU/IIST fellow, from the National University of
Ulaanbaator, Mongolia
Monday, 30 June 97
Title: Displaying and Printing
Multi-lingual Documents
Abstract: Abstract: The domain analysis of
multi-lingual (ML) documents and requirements to ML document
processing tools were made by our colleagues and a formal model of
ML documents was suggested.
We will discuss a new model and a formal specification of the
displaying part of the MultiScript system (tool).
- Li Xuan Dong, UNU/IIST fellow, from Nanjing
University
Thursday, 3 July 1997
Title: Checking Hybrid Automata for
Linear Duration Invariants
Abstract: In this talk, we consider the problem
checking hybrid systems modelled by hybrid automata for a class of
duration properties called linear duration invariants, which are
constructed from linear inequalities of integrated durations of
system states. Based on linear programming, an algorithm is
developed for checking a class of hybrid automata for linear
duration invariants.
- Professor Arun Kumar Pujari, UNU/IIST fellow, from University
of Hyderabad, India
Tue, 8 July 1997
Title: Neighbour Logic & Interval
Algebra
Abstract: This is in continuation with the seminar given by the speaker in
April. In the earlier seminar, it was a survey of the
results on different subalgebras which admit polynomial time
algorithm for satisfiability problem. The main theme of the seminar
was " a trade-off between expressive power and tractability" of
different subclasses of Interval Algebra.
The second seminar is to outline the work done since then by the
speaker. It is to establish a link between the Neighbourhood logic
formalism and the above formalism. This process led to some
interesting outcome. The aim of this talk is to outline these new
results.
The seminar will be more general in nature and will be independent
of the first seminar.
- Dr Paritosh K Pandya, UNU/IIST visitor, from TIFR, Mumbai,
India
Thu, 9 Oct 1997
Title: DC Valid
Abstract: Monadic second order logic can
be used for specifying languages over infinite words. An
automata-theoretic decision procedure allows the checking of
validity of MSO formulae. For a large subset of discrete-time
duration calculus, the validity its formulae can be reduced to the
validity of corresopnding MSO formulae. These techniques are
combined and implemented in a model-checking tool called DCVALID.
We will introduce the tool DCVALID and present an overview of the
theory behind it.
- Dr Hiroshi Uchida, UNU/IIST Visitor, from The United Nations
University, Institute of Advanced Studies (UNU/IAS)
Sat, 25 Oct
1997
Title: Machine Translation and UNL (Universal Network Language)
Abstract: Not
received yet
- Dr Paritosh K Pandya, UNU/IIST visitor, from TIFR, Mumbai,
India
Mon, 27 Oct 1997
Title: A compositional semantics of
SL
Abstract: Synchronous reactive languages are given semantics under the
synchrony hypothesis which states that computation and
communication do not take time. As a result, instantaneous dialogs
can occur between concurrent processes. Duration Calculus of Weakly
Monotonic Time (WDC) is an extension of DC which incorporates the
view that a dicrete sequence of states can arise at the same time
point in a behaviour. As a result, it is well suited to give
semantics of synchronous langauges.
SL is a new synchronous reactive language, related to Esterel.
Unlike Esterel, every SL program is guaranteed to be coherent and
deterministic. We will describe a compositional semantics of SL
using WDC. The semantics translates every SL program into a WDC
formula capturing its behaviour. It provides a convenient logical
framework for analysing properties of SL programs.
- Professor Anders P. Ravn, UNU/IIST Visitor, from DTU, Denmark
Thu 20 Nov 1997
Title: Engineering of real-time systems - with an experiment in hybrid control
Abstract: This talk reports on development of a multithreaded, multiprocessor
program for an embedded system. It covers all phases of the development from
requirements through successively refined designs with formal verification
to implementation. The program controls an experimental
hydraulically powered manipulator with two links. The
architecture uses local control for each of the links, and has
a mode switched control algorithm which detects and reacts
on changes in model parameters due to variations in the forces
acting on the link.
The result shows that it is feasible to check a design against
realistic top level requirements with specific assumptions about th
control and mode detection algorithms. The design is detailed
to an architecture that isolate these and other algorithms supplied
by control engineers, thus providing a precise interface description
with a potential for reuse.
Specifications of requirements and designs are expressed in duration calculus,
a real-time interval logic, which is also used in verification. The
implementation is done in `occam' for a network of four `transputer`'s.
Low level timing constraints are checked manually by calculating
path lengths.
Final paper available
Joint work with: Thomas J. Eriksen, Michael Holdgaard and Hans Rischel,
IT,DTU
- Prof Yulin Feng, UNU/IIST Visitor, from
Institute of Software, Chinese Academy of Sciences,
PRC
Thu 27 Nov 1997
Title: Introduction to ISCAS and Component Software Engineering in Object Orientation
Abstract: The development of object oriented technology cause a great changes to
traditional methods of application software design and such changes make it
possible that application systems can be constructed through some software
components. A component framework is not simply a set of prepackages
solutions from which a customer may pick and choose, it involves an actual
custom tailoring and reengineering during the 1990's mass customization. The
talk is prepared to a brief description of our research on component software
engineering in object orientation, including object models, specification
languages, design methodology and OO trends and perspectives etc.
- Prof Enhua Wu, UNU/IIST Visitor, from
Institute of Software, Chinese Academy of Sciences,
PRC
Thu 27 Nov 1997
Title: Research on Image Synthesis, Scientific Visualization and Virtual Reality
Abstract: Realistic image synthesis or photo-realistic graphics generation has its
important applications in many areas such as CAD/CAM, Computer Animation and
Filming, Visualization in Scientific Computing and Virtual Reality. Simulation
of lighting effect is vital in producing realistic images of physical
environments. In this topic, the primary techniques of global illumination, in
particular the radiosity technology, with the contribution by the speaker in
this field will be introduced. As very important research and application
areas in computer graphics, Visualization in Scientific Computing and Virtual
Reality are closely associated with image synthesis. In this topic, the
related research work on these fields, as well as some applications will
be also introduced.
