- Jens Ulrik Skakkebæk, Department of Computer Science,
Technical University of Denmark; now CRI Inc., Denmark.
Thursday,
9-Feb-1995
Title: Towards a Duration Calculus Verification
Assistant in PVS
Abstract: The Duration Calculus (DC) is an interval
temporal logic for reasoning about real-time systems. This
presentation describes an approach to constructing a tool, a verification assistant, that supports proofs in DC. In the
approach, the verification assistant is implemented by encoding
the semantics of DC in the specification logic of PVS, a
general-purpose specification and verification environment from
SRI International, USA. A Gentzen style sequent proof system for
DC is developed and shown to be sound with respect to the semantic
encoding. The similarities between the proof systems of PVS and
DC are exploited so that DC semantic level proofs carried out in
PVS appear as proofs in the DC proof system. The resulting system
retains the specification and verification capabilities of PVS
within the framework of DC. The approach can be applied to
specification logics other than DC.
The encoding of DC in PVS is presented and the verification
assistant illustrated by a running example.
Following the presentation, there will be a demo PVS for people
who interested. Hopefully, there will be also be a demo of DC in
PVS.
Joint work with N. Shankar, SRI International, USA
- Philip Chan, UNU/IIST Fellow, DLSU, Manila, The
Philippines
Thursday, Feb. 16, 1995
Title: Real-Time Disk Scheduling
Algorithms
Abstract: We have all experienced how fast modern microprocessor
technology is advancing. And although disk storage capacities are
also improving at an impressive rate, disk performance improvements
are occurring at a rather slower rate. This has made the
performance of disk systems a dominant factor in overall system
behavior. On a real-time system, there is even a greater need to
consider how disk access performance is affecting the ability of the
system to meet its real-time constraints.
This presentation provides an overview of recent research work in
real-time disk scheduling. It will be shown that disk access
performance is affected by several factors such as the dynamics of
the disk, the characteristics of the disk requests and the
transactions that issue them, and the disk scheduling algorithm
used. Comparative simulation study results of existing real-time
disk scheduling algorithms will also be presented.
- Fu Hongguang, UNU/IIST Fellow, CICA Chengdu, PR of
China
Thursday, Feb. 23, 1995
Title: The Inverse Kinematics of
Manipulators and readable proofs for geometry theorems
Abstract: The inverse
Kinematics problem of manipulators is fundamental for computer
controlled robots. Given the pose of the end effector( the position
and orientation), the problem corresponds to computing the joint
displacements of that pose. The ideal of readable proofs for
geometry theorems is eliminating the invariants of geometry. We
shall discuss how to apply this approach to the inverse kinematics
of robot arms.
- Mia Indrika, UNU/IIST Fellow, Univ. of Indonesia,
Jakarta
Thursday, Mar. 2, 1995
Title: Toll-way System in Indonesia
Abstract: Toll system is a system which provides toll way management and
service to toll way user.
Toll way user has to pay toll fare based on the vehicle type and the
distance from entrance gate to exit gate. In entrance gate user get
a ticket, in exit gate user give the ticket back and pay the toll
fare.
Toll equipments are installed in every toll plaza (toll office) and
in every toll booth which is located in toll gate.
The existing equipments and the system are obsolete already. They
will be replaced with the new system that has better performance on:
- security
- accuracy on transaction recording
- reliability
This presentation provides the specification of new toll system based
on the specification written by toll company.
- Prof. Marek Rusinkiewicz, University of Houston, TX,
USA
Monday, Mar. 6, 1995
Title: From Transactions to Transactional
Workflows
Abstract: The basic transaction model has evolved over time to
incorporate more complex transaction structures and to selectively
modify the atomicity and isolation properties. In this talk we will
discuss the application of transaction concepts to activities that
involve coordinated execution of multiple tasks (possibly of
different types) over different processing entities. Such
applications are referred to as transactional workflows. We discuss
the specification of transactional workflows and the issues involved
in their execution.
- Dr. Xu Qiwen, UNU/IIST Research Fellow
Friday, Mar. 3, 1995
Title: On
CSP
Abstract:
- Prof. Klaus Berkling, University of Tsukuba, Japan
Wednesday,
Mar. 8, 1995
Title: A `Fast' Representation of the Lambda Calculus
Abstract: In
this talk we will present a representation of the lambda calculus
which deviates from the classical definition in three ways:
- De Bruijn Indices are used throughout
- beta-conversion is independent of complicated preconditions,
which would have to be evaluated before performing the conversion,
and
- alpha-conversion is completely eliminated. It is subsumed under
the index adjustments done locally by integer arithmetic.
Because of these features, this `fast' direct implementation lends
itself to fast implementation.
- Dr. Kanchana Kanchanasut, AIT, Bangkok, Thailand
Thursday, Mar.
16, 1995
Title: A shortest path algorithm for Manhattan graph
Abstract: In this
talk, the speaker will present an algorithm to find a shortest path
in a Manhattan graph - a graph in which the vertices are points in
Zd and the weight on each edge is the Manhattan distance between
its two incident vertices. The algorithm is of O(V+E)logV time
complexity but for a specific class of graphs it can be reduced to
O(V)
- Prof. Zhou Chaochen, UNUIIST Principle Research
Fellow
Thursday, Mar. 23, 1995
Title: A Duration Calculus with Infinite
Intervals
Abstract: This talk will explain why and how we extend Duration
Calculus with infinite intervals.
The extended calculus defines a state duration over an infinite
interval by a property which specifies the limit of the state
duration over finite intervals, and excludes the description
operator. Thus the calculus can be established without involvement
of unpleasant calculation of infinity. With limits of state
durations, one can treat conventional liveness and fairness, and can
also measure out liveness and fairness by properties of limits.
Including both finite and infinite intervals, the calculus can, in a
simple manner, distinguish between terminate behavior and
nonterminate behavior, and therefore directly specify and reason
about sequentiality.
- He Weidong, UNUIIST Fellow, BVA & A, Beijing, PPC
Thursday,
Mar. 30, 1995
Title: Stability of Hybrid Systems
Abstract: The stability of the
system is of primary interest and must be investigated. Hybrid
control systems contain conventional feedback loops and logic
decision making components, how to analyze stability of hybrid
control systems and how to design stable hybrid control systems are
intriguing problems. Based on the Lyapunov's stability theory, we
present an approach to cope with the stability of hybrid control
systems in this paper. Decision maker and digital controllers can be
designed to guarantee that the system is stable.
- Philip Chan, UNU/IIST Fellow, DLSU, Manila, the
Philippines
Thursday, Apr. 6, 1995
Title: Scheduling Policies for Tasks
with Real-Time Constraints and Shared Resources
Abstract: Operating systems
have been a subject of design and implementation for many years.
Despite their widespread use in almost every computing environment,
formal techniques have been applied only on relatively simple
aspects of their dynamic behavior. This is mainly due to the fact
that operating systems are very complex software systems and it is
difficult to formally describe properties of real-time operating
systems and their components unless these are simplified.
This lecture presents preliminary results on formalizing real-time
schedulers for tasks with shared resources. The objective of doing
this formalization is two-fold: (a) to show the expressive
capabilities of DC in formalizing not only simple systems but also
more complicated ones; and (b) to use optimization techniques
presented in [HZ94] for comparing existing policies.
This aims to encourage others to formally treat real-time aspects of
operating systems which in the past are conventionally a piece of ad
hoc territory in computer science.
References:
[HZ94] He Weidong and Zhou Chaochen. "A Case Study of Optimization,"
UNU/IIST Report No. 34, December 1994.
- Wang Ji, UNU/IIST Fellow, CIT/NUDT, Changsha, PR of
China
Thursday, Apr. 13, 1995
Title: On Formal Description of Hybrid
Systems
Abstract: This presentation is to present a formal language for
describing hybrid systems and define a semantics of the language in
Extended Duration Calculus with infinite intervals. First, we
discuss the various causalities between dynamics and events in
hybrid systems. Inspired by the extended TCSP[He94], we try to
present Hybrid CSP to describe hybrid dynamic systems whilst the
intrinsic interactions between continuity and event will be captured
more faithfully than ever. Henceforth, drafting a duration semantics
for HCSP, we could get the insights into formal semantics of hybrid
systems.
- Mia Indrika, UNU/IIST Fellow, Univ. of Indonesia,
Jakarta
Thursday, Apr. 20, 1995
Title: CSP Specification of Toll-way
System in Indonesia
Abstract: In this seminar, the speaker presents partial
work of applying formal method to specify toll-way system. Toll-way
system consists of several components that are running in parallel.
At the first step, we use CSP to specify the behavior of the system.
Hopefully, with this formalization we will be able to show that the
system meet some properties.
- Prof. Wang Ju An, University of Macau
Thursday, Apr. 27,1995
Title: A Duration Calculus Approach to Specifying a Steam-boiler Control
System
Abstract: This report presents a general method to cope with hybrid
control system specification and verification by making full use of
both the simplicity of finite automata and the excessive expressing
power of Mean Value Duration Calculus. The method consists of four
steps: First, specify the requirements of the whole system through
Mean Value Duration Calculus formulas. Second, use two real-time
communicating automata to characterize the design decisions, which
describe the plant and control subsystems respectively. Third,
translate the automata into Mean Value Duration Calculus formulas.
Finally prove the design decisions conforming to the requirements
specification. Taking the steam-boiler problem raised by J.-R.
Abrial[1] as a running example, we demonstrate the above method in
three versions of abstractions. Each version represents an abstract
level for capturing the original problem requirements and provides a
complete procedure of applying the above method. Specification
refinements and the corresponding implementation refinements are
also discussed thoroughly.
- Dr. Xu Qiwen, UNU/IIST Research Fellow
Thursday, May 4, 1995
Title: Hierarchical Design of a Chemical Concentration Control System
Abstract:
The system is used to control chemical concentration and it has both
nontrivial dynamics and a control program. We investigate how DC can
be applied to the design in control theory and how durational
specifications can be developed into programs.
- Prof. Dines Bjøner, UNU/IIST Director
Monday, May 8, 1995
Title: Domain Analysis, Requirements Capture & Software Development --
illustrated by an Example: "Air Traffic"
Abstract: What is Air Traffic? We
try to illustrate an answer to this question by presenting the
basics of an Intrinsics description of Airports and Airways, of Time
Tables, and of Traffic: Actual, Scheduled and Re-scheduled. The
answer illustrates use of "theories" of 3D Bodies, Graphs, Time,
Time Tables, etc. Our answer also allow us to "speculate" about
other Domain Analysis components than Intrinsics: Support
Technology, Rules & Regulations, Staff and Client Behavior,
Computing & Communications Platforms - all in preparation for
Requirements Capture. We are then in a position to isolate "exact"
meta-requirements as to what Requirements Capture "is all about"!
From sketches of a Requirements Specification we can then - incl.
further injection of ideas -- construct a suitable Software
Architecture (i.e. give its Specification).
The talk illustrates UNU/IIST's R&D work with young Fellows from
Developing Countries on:
Software Support for Infrastructures
One of UNU/IIST's main three lines of Programmatic Activity.
- Chris George, UNU/IIST Research Fellow
Thursday, May 11, 1995
Title: Distributed rescheduling of trains
Abstract: The Running Map Tool developed
by the PRaCoSy project helps users develop timetables for scheduling
trains. Rescheduling involves adapting timetables as they are
"executed" by trains to deal with lateness, breakdowns, etc. In
addition, timetables for an area are in fact distributed to
"dispatch units" covering sub-areas. Dispatch units reschedule
trains in parallel, and trains may move from one dispatch unit's
area to another.
The seminar addresses the software architecture needed to support
such a system and its development into a concurrent, distributed
system.
- Roderick C.A. Durmiend, UNU/IIST Fellow, The Philippines
Tue,
09 May 1995
Title: Protocol Design and Verification for a Digital
Multiplex Radio Telephone System
Abstract: This presentation aims to
present an overview of a project that aims to develop a protocol for
a digital multiplex radio telephone system utilizing the Time
Division Multiplex (TDM) and the Time Division Multiple Access
(TDMA) techniques. The system shall be composed of a central
station, repeater stations and remote stations interconnected by
microwave radio links. The protocol should provide efficient
allocation of a limited bandwidth to remote stations serving many
subscribers, and should be able to handle PCM-encoded voice and data
transmissions. Furthermore, this project aims to design and develop
the protocol given the requirements and constraints of the system;
and to determine and verify the efficiency and correctness of the
protocol.
- Prof. Luis M. Camarinha-Matos, New University of Lisbon and
Uninova Institute, Portugal
Thurday, 11 May 1995
Title: Research
Activities in Robotics and CIM at the Center for Intelligent
Robotics
Abstract: This talk will give an overview of the main research
activities on Robotics and Computer Integrated Manufacturing being
carried in the Center for Intelligent Robotics (CRI) of Uninova.
The UNINOVA, Institute for the Development of New Tecnologies, is a
non-profit University-Enterprise association, that was formed in
1986 by the Faculty of Sciences and Technology of the New University
of Lisbon (FCT/UNL), the Portuguese Industrial Association (AIP),
the Professional Training and Employment Institute (IEFP), a
financial holding (IPE) and other 30 companies. The main theme of
UNINOVA is to pursue scientific research, technical development,
high level training and the creation of new technological innovation
centers and small size industries. The Institute is organized in
several centers. One of these centers is the Center for Intelligent
Robotics.
A presentation of the structure, activities and main results of this
Center will be made. Particularly, details of major projects -
recently finished or being developed - will be given. Among these, a
particular reference to international projects:
- Esprit CIM-PLATO: CIM Toolbox
- Brite CIM-TOFI: CIM System with IMproved capabilities for
Furnitury Industry
- Esprit ROADROBOT: Operator Assisted Mobile Road Robot for Heavy
Duty Civil Engineering Applications
- Esprit Basic Research B-LEARN II: Behavioral Learning: Combining
Sensing and Action (Application of Machine Learning Techniques in
Robotics)
- ECLA CIMIS.net: EC - Latin America Exploratory Collaborative
Activity "Distributed Information Systems for CIM"
- ECLA FlexSys: EC - Latin America Exploratory Collaborative
Activity "Design of FMS/FAS systems for SMEs"
- Mr. Jose Barata, New University of Lisbon and Uninova Institute,
Portugal
Friday, 12 May 1995
Title: Frame-based approaches for
integration of shop floor controllers towards Intelligent
Supervision Systems
Abstract: Various modeling perspectives for
manufacturing systems, both from the structural and dynamic behavior
points of view, will be discussed. The utilization of
object-oriented and frame-based paradigms in this modeling context
will be discussed as well as the connection of models to the real
device controllers. The synthesis of control programs from a Petri
net model is also presented in this general modeling framework.
- Prof. Kasav Vithal Nori
Sat. 20 May 1995
Title: Object Modeling in
Engineering Science Applications
Abstract: The work is rooted in a prototype
development experience of an Integrated Simulation Environment for
Chemical Process Plants, in which it is possible to simulate
multiple behaviors of the plant in its operations. Behavior is
modeled through equations. Modeling is equivalent to building
equations and simulation is effected by solving them using a solver.
Given this separation of concerns, the system allows: multiple
behaviors to be associated with its elements; composition of
systems; assignment of behavior of interest; solving for system
state; and continuing with the last two steps. In retrospect, the
above experiment admits rich possibilities for an object oriented
framework. An operational view of the framework is presented. The
structuring of this view suggests the possibility of a type algebra
suitable for modeling such a world of objects.
- Prof. Kasav Vithal Nori
Sat. 20 May 1995
Title: Academic and
Industrial Software Processes: Bridging the Gap
Abstract: The academic view
of the software process is epitomized in program refinement calculi.
Through such a view, quality of software is clearly stated up-front,
and its realization substantiated through the deployment of the
calculus to calculate the resultant program. Causal trace of the
process, and built-in justification at each stage, make the process
both suitable for evolutionary maintenance and audit. Such calculi
are limited by the technology (programming notation) for which they
are defined. Industrial software processes, on the other hand,
stress manageability, levels of understanding (leading to
delineation of responsibilities), and cope with all technologies
needed in the process as well as the resultant product. Their
definitions of quality are not sharp. Industrial processes also cope
with the need to carefully identify the problem to solved.
To know that the academia and the industry are addressing the same
issues, there is a need to align these two viewpoints, leading to a
statement about the gaps between them. Once identified, the gaps can
be bridged, leading to a two-way flow of better ideas between the
academia and the industry.
In this talk, such a gap is identified in relation to the TRDDC
experience of doing industrial-research, and the approaches we have
adopted to bridge it are sketched.
- Hong Mei, UNU/IIST fellow, Fudan University, PR of
China
Thursday, 25-May-1995
Title: About FSA and RAISE
Abstract: A brief
introduction on the FSA system fulfilled by the group in Fudan
University will be given. FSA is a knowledge-based software
development environment. It consists of a wide-spectrum
specification language FSAL and an object-oriented knowledge base.
Some comparison of FSA and RAISE is also presented. - Hong
Mei, UNU/IIST fellow, Fudan University, PR of China
Friday,
30-Jun-1995
Title: A Generic Concurrent Distributed Architecture
Abstract: The
work is to give a generic concurrent architecture for a distributed
train rescheduling system. It is developed from the general
distributed map theory.
We suppose that a distributed train rescheduling system has one
dispatch center and several dispatch units each of which manages a
set of stations. Based on the general distributed map theory(Tech.
Rep.No. 42), we use a distributed time-table management.
We design a group of servers to store the partitioned time-table and
to provide buffers for communications among dispatch center,
dispatch units and stations.
- Dong Yulin, UNU/IIST Fellow, China Railway Construction Co., PR
of China
Friday, 14-Jul-1995
Title: Master Thesis Presentation
Abstract: This
thesis is about the formal and rigorous development of RoManS (Route
Management System) for railway station route management. Route
management deals with train traffic within a station, and route
trains according to timetables and station layout so that smooth,
accident-free (somehow optimal) train traffic can be ensured. RoMans
is software that can support station staff in managing routes.
In this thesis, we are concerned with three main "phases": domain
analysis, requirement capture and software development. Domain
analysis is the process of obtaining knowledge of the environment in
which the software serves; that is of all properties upon which
subsequent software may have to rely in order for it to function
according to expectations correctly and properly. Domain analysis
must be taken as a part of software construction and is primarily
pursued (and documented) prior to requirements capture. Requirement
capture is now a process which, from the resulting descriptions of
the domain analysis, extracts their interactions to come up with a
requirements specification. Architecture design is then derived. In
this design the gross structure of the system becomes apparent in
terms of high-level components and connections among these
components. The architecture design is then further developed into
concrete design and translated into C code. A formal method, RAISE
and its development methods, is applied in all of these phases.
- Mohammad Rais, UNU/IIST Fellow, National Institute of Science
Technology & Development Studies (CSIR), New Delhi,
INDIA
Thursday, 27-Jul-1995
Title: Application of Geographic Information
System (GIS) for Land Suitability Analysis
Abstract: Geographic Information
System (GIS) is a system for capturing, storing, checking,
manipulating, analyzing & displaying data which are spatially
reference to earth. It is emerging as a powerful technology for
studying spatial issues. This provides the facility of integrating
together of non-spatial & spatial data from a number of sources,
including maps, field survey equipment, photogrammetry, and remote
sensors, within a single system.
Through the integration of data which were previously the domain of
individual disciplinary specialist, an interdisciplinary perspective
to geographical problem solving is encouraged.
The land & water management in agriculture is the one of the most
complex interdisciplinary & spatial problem which requires an
integrated approach. The present study is an attempt to demonstrate
the application of G.I.S. for studying the land suitability in
agriculture. The area of study is a sub-district in North India.
- Ngo Quoc Tao, UNU/IIST Fellow, Institute of Information
Technology (IoIT), Hanoi, Vietnam
Thursday, 3-Aug-1995
Title: Automatic
Map-Data Entry
Abstract:
In the talk, an algorithm for recognizing items in maps is
presented. The algorithm has been implemented under MAPSCAN, a
SOFTWARE PACKAGE FOR AUTOMATIC MAP DATA ENTRY. The difficulties in
implementing the algorithm and how to overcome them also are
discussed.
The speaker will talk about and demo the main featues of MAPSCAN,
which are summarized as follows.
MAPSCAN is a software package for processing maps by using
techniques of vectorization and text recognition. MAPSCAN transforms
a raster map files into vector files which can be treated further by
well-known applications for map processing: Maplnfor, MapViewer,
PhotoStyler, AutoCAD, AutoSketch,... Due to its user-friendliness,
MAPSCAN is suitable for the engineers, technicians who deal with the
generating/editing maps in computers. MAPSCAN works with the
geography maps with:
- boundaries of territorial areas, rivers, routes, specific lines
- texts which represent the name of areas
Also MAPSCAN works with mechanic drawing maps. Input of MAPSCAN is
bitmap files of various types: TIF, PCX, IMG with size up to 20 MB.
Requirement of Computer Configuration:
- IBM/PC AT 386/486 or compatible, MS-DOS ver 3.0 or
higher
- EGAVGA Graphic Monitor, mouse
- 4M or 8M extended RAM should be recommended.
Application
- GIS and Mapping: Topographic Contours,
Communication Neworks
- Automatic Input Mechanical Drawing into CAD
software
- Logos, Art Design and Font Making
- Yang ZhenYu, UNU/IIST Fellow, Beijing University of Aeronautics
and Astronautics, PR of China
Thursday 14-Sept-1995
Title: Modeling and
Control of Hybrid Control Systems
Abstract: Hybrid control systems contain
two distinct kinds of subsystems, namely timing evolving and event
driven subsystems, which interact with each other and operate in
real time. I will discuss a formal model and control of hybrid
control systems from the viewpoint of control theory. In order to
design and analyze hybrid control systems, an equivalent discrete
event model of an extended plant (EDEM-EP) is extracted for a kind
of hybrid control systems as an input-output controlled automaton.
Based on the EDEM-EP the synthesis of decision-maker is discussed,
and a methodology of designing the DM is proposed. As an example, an
EDEM-EP and a decision-maker of the inverse pendulum control system
are constructed to illustrate proposed methodology.
- Chris George, UNU/IIST Senior Research Fellow
Thursday,
12-Sep-1995
Title: A budget system in RSL
Abstract: On his recent trip to
Vietnam he did a rapid domain analysis of a system to make and
analyse budgets. The work is very simple but illustrates the use of
domain analysis to clarify and define concepts. This seminar
presents the domain analysis he did.
- Roderick C.A. Durmiendo, UNU/IIST Fellow, The
Phillipines
Thursday, 12-Sep-1995
Title: Formal Development of a Digital
Multiplexed Radio Telephone System
Abstract: We discuss the formal
development of a Digital Multiplexed Radio Telephone System, an
extension of the Telephone System Domain. We first present a domain
analysis of the system , derive an abstract applicative
specification and identify the system's invariants and properties.
We also discuss the process of refinement we undertook until we
arrive at a decomposed specification of the system. We show the
method of verification to prove implementation and partial
implementation of the steps. Finally, we present the resulting
concurrent imperative specification.
- Tomasz Janowski, UNU/IIST Research Fellow
Thursday,
19-Oct-1995
Title: On Branching Time and Provable Fault-Tolerance
Abstract: In
order to ensure that software, in addition to being free of design
faults, is tolerant of physical faults that may affect the
underlying hardware, we normally introduce some form of redundancy,
like additional instructions (software redundancy), components
(hardware redundancy) or executions (time redundancy). However, for
systems composed of many concurrent components, involved in ongoing
interactions with their environment and with themselves, redundancy
management may lead to intricate problems which require difficult
design decisions and consequently increase the risk of introducing
design faults itself. It is therefore important that we are able to
verify fault-tolerance and ways of doing so, using standard
techniques and syntactic transformations (to represent effects of
faults) are well-known and long-applied. Seemingly, no new
techniques for provable fault-tolerance are needed.
We show that this is not always the case. Since occurrences of
faults are unpredictable (though undesirable they may occur anyway
and even assumed to be present they may indeed never take place),
after proving correctness for the anticipated faults, correctness
for some, or even none of them should be guaranteed. However, this
fault-monotonic property is violated for many kinds of reasoning
(both assertional and equational) based on the branching-time
semantics. We shall demonstrate this for bisimulations and its
corresponding modal logic, and show how to refine both into a
fault-monotonic theory for provable fault-tolerance. Subsequently,
we show how to build up a framework which extends CCS and supports
incremental (and compositional) refinement for an increasing number
of anticipated faults. Design of a distributed database serves as an
illustrative example.
- Phan Hong Giang, UNU/IIST Fellow, IoIT, Hanoi,
Vietnam
Thursday, 26-Oct-1995
Title: Interval-valued Probabilistic Logic
for Logic Programs
Abstract: Entailment problem in knowledge base where a
portion of knowledge is given by a pair of a sentence of
propositional logic and an interval representing its truth
probability is computationally difficult. Its solution amounts to
solving linear programming problems. We present an
approximate method, which reduces the entailment problem to one of
finding "prime implicants" of the target sentence expressed
through the names of sentences in the knowledge base. Then we show
that in the case of probabilistic logic programs the set of such
prime implicants can be found by using a modification of well-known
SLD-resolution.
- Rechard Moore, UNU/IIST Research Fellow
Thursday, 9-Nov-1995
Title: Experiences in Developing a Proof Theory for VDM Specification
Abstract: As
part of the standardisation of the VDM specification language
(VDM-SL) a model-based denotational semantics of the language is
being developed. This is poorly suited to conducting proofs about
VDM-SL specifications, however, so we have attempted to translate it
into an axiomatic (proof-theoretic) semantics. The talk reports on
some of the problems we encountered, and discusses some possible
solutions and their repercussions.
- Professor Armando Haeberer, Brasil, UNU/IIST Visiting
Professor
Friday, 24-Nov-1995
Title: The ARTSWARE Project
Abstract: The
ARTSWARE project comprises two separate dimensions: development with
research, and exploratory research. The first dimension, which
originated the project, consists of the ARTS project (Formal
Approach to Real Time Systems Development). The ARTS project was
originated in a contract between Equitel (Siemens Brazil) and the
Laboratory of Formal Methods of the Dept. of Informatics of PUC-Rio
(LMF-DI). The project's partners are Equitel, LMF-DI, FAST
(Forshunginstitut fuer Anguewandte Software Technologie), Munich,
the Institut fuer Informatik of the
Ludwig-Maximilians-Universsitaet-Muenchen, and the Imperial College
of the University of London. The aim of the project is to provide a
new methodology and a prototype of its respective support system,
for the object-oriented development of real time and concurrent
systems. It is based on the modification and extension of a set of
existing methods, but the distinctive basis and originality of this
project is its formal approach to specification, prototyping,
validation, verification and enhanced testing. Other goals pursued
in its development are: early prototyping with early performance
evaluation, transformation, traceability, and reuse. Firstly, we
analysed existing object-oriented methodologies such as
Shlaer-Mellor's, Rumbaugh's, Jacobson's, and Booch's, with respect
to real time and concurrent systems development. Then, a new
object-oriented methodology is being developed, maintaining the
appropriate parts of the existing ones, but completing them with
specific support for the reuse of software components and for real
time concurrent programming. The formal approach on which the
intended methodology is founded is based on the following principles
and paradigms: the very first definitions of the behaviour of the
system are modelled using temporal logic, while its functional
behaviour is modelled by means of a Meseguer-like extension to
abstract data types; the configuration of the distributed concurrent
system is shaped as a "chemical system composed by molecules and
their interactions" (representing objects and messages); its
mathematical representation is given by multisets of objects; its
dynamic behaviour is described by both non-deterministic concurrent
rewriting of such configurations, and some kind of Modal Action
Logic extended with deontic modalities of permission and obligation.
This formal approach serves as a common semantics basis for
integrating the different diagrammatic notations of object-oriented
development, particularly those diagrams modelling objects and
classes and describing dynamic behaviour and interaction. such
semantic basis will render possible the maintenance of a level of
inferences and proofs hidden behind the user level containing
ordinary user-oriented notation. Along with this intended
methodology, support tools for the development and management of the
corresponding object-oriented diagrams, including traceability, are
being developed. Facilities as version controls and a data base of
classes are also being included. The tool suite, moreover, supports
the development of use case analysis, diagrams for object
interaction, prototyping, validation and animation of designs using
rewriting tools, testing based in use cases, semi-automatic
code-generation from designs, and code optimisation by
transformation tools. Some support for the reuse of components is
foreseen as well. It is a typical applied research project,
characterised by the generation of products and results within
strict deadlines, and observing the following basic technological
restrictions: part of the technology used, though it already exists,
has not yet been implemented or put to use in industrial quality
products; part of it exists in the form of laboratory prototypes;
part is available commercially off-the-shelf, and; finally, part
does not exist and has to be researched and developed. The
fundamental characteristic of this dimension is that research and
development result from a search for appropriate solutions within
the scope and the requirements of the project they have stemmed
from, and,once they are they are found, their relation with existing
knowledge, their extent, the search for alternatives, or the
exploration of discovered paths are absolutely closed off. For this
reason, this first dimension spins off both precompetitive and basic
research. The second dimension can be called an exploratory
research dimension. According to what has previously been exposed,
there are, in the ARTS project, several paths which will be left
unexplored, implementations that, for reasons of technological risk,
have not been (or will not be) carried out on the most advanced
platforms. Let us consider, for instance, the general
supportenvironment. Apparently, it should be one of the latest
generation object-oriented operation systems, such as OpenStep,
Taligent, or Cairo. Such systems present a series of valuable
advantages for the implementation of environments like ARTS, but
the risk involved in making a wrong decision is extremely high.
Which of the systems will win the race and become - in, say, four
years - the market standard? This is obviously a difficult question
and the risk of implementing an industrial prototype like ARTS on
any of them is of an unacceptable size. We can make an analogy with
the risk of having filmed a wonderful award-winning film in
beta-max, not foreseeing VHS would become the standard. The obvious
decision in ARTS was to choose as a support base an object-oriented
database and a meta-Case that communicate according to an accepted
standard, such as ODBC or CORBA, and of which there are
implementations on the most widespread software/hardware platforms
in the market. However, what will happen with ARTS in four years,
only two years after its beta-version is launched? The panorama
does not seem very encouraging, if one of the mentioned operative
systems becomes the market standard. In that case, ARTS should have
the destiny of a good movie filmed in Super-8 and not copied in VHS.
This is one of the reasons for this second dimension. If such is the
case, in four years the beta-version of ARTS should be
re-implemented on a last-generation platform, in order not to risk
falling into oblivion. There are other examples of the need to
count on an exploratory dimension. One of the central modules of
the ARTS methodology support environment is a rewriting system which
will not only automatically produce code by transformations, but
also be used to exercise object-oriented analysis and design
diagrams, of which one of the semantics shall be Meseguer-like
Conditional Rewriting Logic. It was decided that, in ARTS, TXL would
be used, which has implementations for all the platforms of interest
to the project. There are, of course, far more sophisticated
systems, but these are larger and their implementations are usually
"laboratorial". An indispensable exploratory investigation is the
carrying out, parallel to the development of ARTS' industrial
prototype, of experiments with such systems, and the production of
an alternative "laboratory implementation" of certain modules of
this prototype. The project ARTSWARE's subprojects are, apart from
ARTS: Software Development Process; Reimplementation of Plato in
OpenStep and Taligent; Software Metric Support; Abstract Data Views
and Abstract Object Views in the Context of Reuse; Algebraic Object
Specification and Very Efficient Rewriting Systems;
Semantic-Oriented Code Generation;Data Integration using CORBA and
OODBMS; Early and Late Requirements Engineering; Concurrent
Manipulation of High Velocity Network Distributed Object Hypergraph;
Concurrent Control of Software Engineering Environments.
ARTSWARE's partners are LMF-DI; the State University of Maringa; the
Federal Universities of Pernambuco, Rio Grande do Sul, and
Fluminense; and Equitel, in Brazil, and The Imperial College, the
LMU, FAST, UBW, Christian-Albrechts Universitaet Kiel, Universitaet
Kaiserslautern, Politecnica di Milano, the University of Toronto,
the University of Waterloo, Aarhus University, the Technion, and
UNU/IIST
- Professor Armando Haeberer, Brasil, UNU/IIST Visiting
Professor
Thursday, 30-Nov-1995
Title: Calculating Programs in Fork
Algebras
Abstract: Fork Algebras are an extension of Relation Algebras that
were shown to encompass the expressive power of First Order Logic
with Equality. These algebras were developed by Baum, Frias,
Haeberer and Veloso and have strong connections with Tarski and
Givant's Quasi Projective Algebras and Maddux's Pairing Algebras.
Since they are finitely axiomatizable and, therefore, representable,
one can keep in mind while calculating the input/output nature of
its standard model, i.e., set theoretic relations over infinite
binary trees. The reason for the development of fork algebras,
expressiveness and representation issues and a short program
derivation will be presented.
- Dang Van Hung, UNU/IIST Research Fellow
Thursday, 7-Dec-1995
Title: Sampling Semantics of Duration Calculus
Abstract: In the talk, the problem of discretization of continuous time in
Duration Calculus (DC) is addressed. For a DC formula D, for a
sampling step h, a sampling semantics [[D]]h is defined to
express the properties of discrete observations of its models, while
original semantics [[D]] expresses the properties of the models.
In practice, only sampling semantics is implemented. So, an
implementation D of a system specified by S, both are assumed to
be written in DC, is correct iff [[D]]h <<=[[S]]. Some
rules for proving the correctness of an implementation are given.
The problem of digitization is also considered. Some
forms of digitizable DC formulae are shown.
- Prof. Jeannette M. Wing, Computer Science Department
Carnegie Mellon University
Pittsburgh, PA 15213
Tue, 27-Dec-1995
Title: A Behavioral Notion of Subtyping
Abstract: The use of hierarchy is an important component of object-oriented
design. Hierarchy allows the use of type families, in which higher
level supertypes capture the behavior that all of their subtypes have
in common. For this methodology to be effective, it is necessary to
have a clear understanding of how subtypes and supertypes are related.
We take the position that the relationship should ensure that any
property proved about supertype objects also holds for its subtype
objects. In this talk I will present a new way of defining the
subtype relation, which not only meets this criterion but also is easy
for programmers to use. I will also discuss the ramifications of this
notion on the design of type families and on the contents of type
specifications.
This is joint work with Barbara Liskov.
- Prof. Jeannette M. Wing, Computer Science Department Carnegie
Mellon University Pittsburgh, PA 15213
Tue, 28-Dec-1995
Title: Using
Belief to Reason About Cache Coherence
Abstract: The notion of belief has
been useful in reasoning about authentication protocols. In this
talk, I explain how the notion of belief can be applied to reasoning
about cache coherence in a distributed file system. This work uses
an extended subset of a logic of authentication defined by Burrows,
Abadi, and Needham to analyze validate-on-use and invalidation-based
protocols, including Mummert's recent "large granularity protocol"
for use in weakly connected environments. Using this variant of the
BAN logic, we were able to find flaws in the design of the large
granularity protocol. We found the notion of belief not only
intuitively appealing for reasoning about our protocols, but also
practical given the optimistic nature of our system model. In the
talk, I will also report on some promising recent results on the use
of model checking to verify these protocols.
This work is joint with Lily Mummert and M. Satyanarayanan.
