- Pei Yu, UNU/IIST Fellow From Nanjing University, P.R.China
15:00
Friday 17 January, 2003
Title: Model Checking Reactive Systems for Interval Based Properties
Abstract:
A reactive system satisfies a property iff all its behaviors satisfy =
the property. For a system with behaviors of infinite sequences of =
states and an infinitary property, i.e. property defined over infinite =
sequences of states, the definition of the satisfaction relation is =
quite straightforward. In this paper, we propose a satisfaction relation =
between an infinite system behavior and a finitary property defined =
over finite sequences of system states, so that some interval based =
safety properties and liveness properties can be specified as finitary =
properties. We also show that the decision process of whether a reactive =
system satisfies a finitary property can be carried out automatically.
Particularly, we use DQRDC(an extension of a subset of DC, with disrete =
time model) to specify the interval based properties and perform =
checking using the Spin model checker.
- Sun Meng, UNU/IIST Fellow from Beijing University,
P.R. China
15:00 Friday 24 January, 2003
Title: Component-Based Coalgebraic Specification and Verification in RSL
Abstract: Component-based software development has become a popular
paradigm in software engineering. From the theoretical point of
view, components can be seen as coalgebras. We present a coalgebraic
technique for component-based system specification and verification
which is based on RSL, the wide spectrum specification language
of the RAISE method. A bisimulation relationship between components
is defined for reuse of components and also used in the behavior
verification of
specification development. Finally we use an example to show how final
coalgebras
are used to construct the minimal implementations of given specifications.
- Sun Meng, UNU/IIST Fellow from Beijing University,
P.R. China
15:00 Friday 14 February, 2003
Title: Towards a Coalgebraic Semantics of UML: Class Diagrams and Use Cases
Abstract: A coalgebraic semantics for UML class diagrams and some
discussions
on the coalgebraic semantics for use cases are given. The semantics of a
class in
UML class diagrams is defined as the category of coalgebras of the
corresponding
class specification. Associations among classes are interpreted as
coalgebraic
observers. The generalization hierarchy of classes is specified by the
inheritance
morphism among them. Some examples on checking the internal consistency
for class diagrams by exploiting the coalgebraic semantics are introduced.
- Prof. Wang Yi, UNU/IIST Visitor from Upssala University, Sweden
15:00 18, 20, 24 February, 2003
Title: Real-Time Systems Modelling and Verification
Abstract: The talks will discuss Model checking in a nutshell, CTL, LTL and model
checking algorithms.
- Prof. Wang Yi, UNU/IIST Visitor from Upssala University, Sweden
15:00 Tuesday 25 February, 2003
Title: Optimal Partition and Performance Estimation in S/H Co-Design
Abstract: One of the major concerns in hardware/software co-design
is to find S/H partitions optimizing system performance
(e.g. response time) under given resource constraints.
Assume that a system is a set of function modules that may
be implemented as software using a micro-processor or
as hardware circuits. In this work, we study how to partition
the set of modules into software and hardware threads
according to given precedence and resource constraints.
We show that the partitioning problem can be transformed into
an integer programming problem for the case of static resource
sharing. For dynamic resource sharing, we show that
the problem can be solved by optimal reachability analysis
for timed automata.
- Ri Hyon Sul, UNU/IIST Fellow from North Korea
15:00, Thursday 13
March 2003
Title: Complete Verification System for Timed RSL
Abstract: The Timed RAISE Specification Language(TRSL) is an extension
of the RAISE Specification Language with time constructors. TRSL
provides time-dependent operations, but can not specify real time
requirements at an abstract level. In this paper we present a
technique for verifying the correctness of TRSL specifications
against the real-time requirements described as predicates over
the observables based on unifying theory of programming. We give a
denotational semantics to a subset of TRSL expressions and develop
a set of proof rules, of which soundness and completeness is
proved. This approach allows to prove the correctness of TRSL
expressions at the syntactical level while hiding the detail of
semantic model. Our work follows the idea and methodology of Hoare
and He's unifying theory of programming.
- Choe Sun Yong, UNU/IIST Fellow from North Korea
16:00, Thursday 13
March 2003
Title: Apply Object-Orientation and UML to the Development of
Web-based Learning System
Abstract:
With the development of Internet technology, the study of theories and methods in the
development of distance learning system is being increased. In this talk, we consider a Web-based learning system as a
client-server system which gives and receives education between the teachers and the students through the Internet and WWW.
We show how object-oriented techniques and UML can be used in
modelling and development of a web-based learning system.
- Jin Naiyong, UNU/IIST Fellow from Shanghai, China
15:00,
Thursday, 20 March
Title: Resource Semantic Models for Programming
Languages
Abstract: Traditional system specifications always abstract from resource.
However, it is unavoidable to append resource constraints in later
system implementation. This paper defines a hierarchy of semantic
models for programm's execution with limited resources. Each model
in the hierarchy is a refinement to the one defined formerly. We
also investigate homomorphism and algebraic laws in these models.
Based on that, we develop a set of program transformations to deal
with the situation that resource are in shortage.
- Purandar Bhaduri, Martin Leucker, Antonio Cerone and Antonio
Grau
Thu 18 Sep 2003
Title: Model checking UML requirements
specifications
Validating Formal Specifications of information systems through
animation
Parallel model checking
Abstract: Not available
- Jean-Raymond Abria
22-26 September
Title: Course on B
Abstract:
- Chris George, UNU/IIST Director
29 September - 3 October,
daily schedule to be announced
Title: Formal Software Specification
Using RAISE
Abstract: See Section II/2/1
- Prof. He Jifeng, UNU/IIST Senior Research Fellow
6 -10 October
2003, daily schedule to be announced
Title: Introduction to Unifying Theories of Programming
Abstract: A theory of programming is intended to support the practice of programming
by relating each program to the specification of what it is intended to achieve.
A unifying theory is one that is applicable to a general paradigm of computing,
supporting the classification of many programming languages as correct
instance of the paradigm. A distinct characterist of
the logic programming paradigm is that each execution of a program profuces
not just a single answer but a collection of answers, allowing the later
parts of the program to select between them. A specification of such a program
is therefore just a predicate describing
the size, content, and other properties of the set of options offered.
THe actual behaviour of a particular program is also described by a predicate, namely the strongest specification that it is cetain to satisfy. The semantics of the programming language is given by a shallow embedding into the predicate
calculus.
- Dang Van Hung, UNU/IIST research fellow
16 - 21 October
2003, 15:00-18:00 daily
Title: Duration Calculus: A Logical Approach to Real-Time Systems
Abstract: See Section II/2/2
- Long Quan,
UNU/IIST Fellow from Peking University
3pm Friday 31 October 2003
Title: The Equivalence of Statecharts
Abstract: This paper proposes a compositional operational semantics for a
nontrivial subset of Statecharts and defines an equivalence
relation between Statecharts using bisimulation on configurations.
An input/response trace model is also investigated at the level of
observable behaviour.
- Dr. Xu Qiwen,
Faculty of Science and Technology,
University of Macau
3pm -5pm, Thursday the 6th, Friday the 7th and Thursday the 20th November 2004
Title: Introduction to Distributed Algorithms and Model Checking with Spin
Abstract:
The basic concepts of distributed systems will be explained,
together with a number of fundamental distributed algorithms, such as
those for distributed time stamp, snapshot and mutual exclusion.
Distributed
algorithms are difficult to analyse, due to a large amount behaviours
they can exhibit. Spin model checking system is mainly developed by
Holzmann at AT&T. It is based on the automaton theoretic approach of
Vardi and Wolper. We will introduce Promela, the modelling language of
Spin, in particular features useful for distributed systems. A
demonstration
of the system will be given. Finally, the automaton theoretic method for
LTL will be explained.
The course is roughly divided into the following 3 sections:
- introduction to distributed algorithms
- introduction to Spin system
- introduction to automaton theoretic method
Slides on distributed algorithms are based on the slides of my course
on Distributed Operating Systems and Algorithms
http://www.sftw.umac.mo/fstqx/slide.ppt
Slides on Spin are at
http://www.iist.unu.edu/qxu/spin.htm, along with
a number of examples.
- Bernhard Aichernig, UNU/IIST research fellow
17 - 21 November,
daily schedule to be announced
Title: Foundations of Software Testing
Abstract: To
be announced
- Zhiming Liu, UNU/IIST research fellow
10 - 14 November,
daily schedule to be announced
Title: OO Software Development using
UML
Abstract: The course provides the students with the engineering principles,
methods and practice of how a large system can be specified, designed
and implemented using object oriented techniques.
Prerequisites
It is required that the course participants have knowledge of and
experience of programming. Experience of programming in an
object-oriented language, such as Java or C++, will be very
helpful. And it is desirable that participants of this course
should have some basic knowledge of Software Engineering topics such
as software cycles, project planning, management, software testing.
Aims & Objectives
The overall purpose of the course is to give an understanding of the
problems of large-scale software development and how this can be
solved using object oriented techniques. The main aim of the course is
to teach the understanding and use of object oriented methods to
analyse, specify, design and implement large computer systems.
At the end of the course the students should be able to:
- analyse customer requirements;
- use UML for specification of a system of a moderate size;
- produce a design based on an object oriented specification;
- implement a design; and
- be very clear about activities to carry out and the artifacts to
produce in a software development,
- have a sound grasp of the basic principles and techniques in
object-oriented software development,
These notes are mostly based on the lectures on a module called
Software Engineering and System Development that I have been teaching
at Leicester University since 1998. The module is core to 2nd year BSc
in Computer Science students, final year BEng and MEng students on
electronic and software engineering students, and optional to BSc
Maths and Computing Science students, Maths students, and Combined
Science students.
- Prof. Mathai Joseph, UNU-IIST visitor, from Tata Research Development and Design Centre,
54B Hadapsar Industrial Estate, Pune 411 013, India
15:00, 12 November 2003
Title: Where and When Will Industry Use Formal Reasoning?
Abstract:
It is many years since the term `formal methods' was introduced, but their
use in
industrial software engineering is still very limited. This raises the
question of whether there
is a `method' to the use of formal theories in solving practical problems?
Large-scale
software development is defined in terms of methods, many of which are
tightly wired into
development environments and project management tools. None of these is a
`formal' method; equally, no application of formal reasoning into the
development
process resembles a `method' as known in software engineering.
Formal techniques and large-scale software development methods have been
used
successfully for different kinds of problems. Very little progress has been
made in
bringing these two development techniques closer together.
In this talk, we discuss the ways in which formal techniques can be used to
improve the
quality and productivity of large-scale software development. Data from
industrial
projects shows that the improvements that result can be significant.
Further areas where
formal techniques can be used are discussed.
- Prof. Keijiro ARAKI, Department of Computer Science and Communication Engineering,
Kyushu University, Japan
24 November
2003, 15:00
Title: Research Project on Embedded Software Development Methodology in
Kyushu University
Abstract: In the last year, Kyushu University strted a big project named
Innovative Cluster for Silicon Sea Belt (CLUSS) supported by the
Ministry of Education, Culture, Sports, Science and Technology of the
Japanese Government. The CLUSS project mainly focuses on System LSI
(or Sytem on Chip) design and manufacturing, but it also contains a
research group on embedded system software development. After a brief
overview of the CLUSS project on System LSI design, I will make an
introduction to the research plan of the embedded software development
including domain analysis, modelling, formal specification,
verification/validation, reusable component libraries, run-time
environment, real-time operating systems, etc.
Slides
- Satyajit Acharya, UNU/IIST fellow from Department of Computer and Informations Sciences University of Hyderabad, Hyderabad, INDIA
26 November
2003, 15:00
Title: Application Specifications for MOBILE COMPUTING
Abstract: The presentation is about the extension of the notational capabilities of Objectcharts to specify the issues related to the mobile computing. We discuss the specialty and the limitations found in mobile computing to motivate the readers on the necessity of having methods for developing mobile computing applications. We have shown that while making use of all the niceties of Statecharts as well as Objectcharts, the formalisms can be extended for developing mobile computing applications. First, we discuss the need for an extension of Objectchart notation by showing the limitations of Objectcharts in specifying mobile computing applications. Second, we propose an extension to Objectcharts, referred to as Mobicharts. The proposed Mobicharts can specify the important characteristics of mobile computing applications. We illustrate typical mobile computing characteristics such as migration, hoarding, cloning, synchronization, sharing and disconnected operations using Mobicharts.
This talk is based on the following two published papers:
1. "MOBICHARTS: A Notation to Specify Mobile Computing Applications", Satyajit Acharya, Hrushikesha Mohanty, R.K. Shyamasundar, In IEEE Proc. of the 36th Hawaii International Conference on System Sciences (HICSS 03)
2. "Mobichart for Modeling Mobile Computing Tasks", Hrushikesha Mohanty, Satyajit Acharya, R.K. Shyamasundar, R.K. Ghosh, In IEEE TENCON 2003 - Convergent Technologies for the Asia-Pacific, October 14-17, 2003, Bangalore, India
- Zhiming Liu, UNU/IIST research fellow
Monday 01 - Wednesday 03
December, 10.30 - 12.30 am, 3.30pm - 5.30pm
Title: OO Software Development
with UML
Abstract: I plan to have two part in this course. The first part will be lectures on the course material and the second part will be seminars on the recent research on formal methods in OO development. UNU/IIST fellows are required to attend both, but academic members of staff who are in office now are encouraged to attend the seminars in order to give us feeadback comments.
The course provides the students with the engineering principles, methods and practice of how a large system can be specified, designed and implemented using object oriented techniques.
Prerequisites: It is required that the course participants have knowledge of and experience of programming. Experience of programming in an object-oriented language, such as Java or C++, will be very helpful. And it is desirable that participants of this course should have some basic knowledge of Software Engineering topics such as software cycles, project planning, management, software testing.
Aims & Objectives : The overall purpose of the course is to give an understanding of the problems of large-scale software development and how this can be solved using object oriented techniques. The main aim of the course is to teach the understanding and use of object oriented methods to analyse, specify, design and implement large computer systems.
At the end of the course the students should be able to:
analyse customer requirements;
use UML for specification of a system of a moderate size;
produce a design based on an object oriented specification;
implement a design; and
be very clear about activities to carry out and the artifacts to produce in a software development,
have a sound grasp of the basic principles and techniques in object-oriented software development,
These notes are mostly based on the lectures on a module called Software Engineering and System Development that I have been teaching at Leicester University since 1998. The module is core to 2nd year BSc in Computer Science students, final year BEng and MEng students on electronic and software engineering students, and optional to BSc Maths and Computing Science students, Maths students, and Combined Science students.
After the introduction to the course material, I will present some of the results of our research on formal methods for object oriented developed. This include the formal model for OO design and its application to the unified formal definition of some UML models.
- Bernhard K. Aichernig, UNU/IIST research fellow
9. - 12.12.;
Tue-Thu, 11:30 - 13:00 and 16:30 - 18:00;
Fri, 10:30 - 13:00 and 15:30 - 18:00
Title: FOUNDATIONS OF
SOFTWARE TESTING
Abstract:
The course focuses on specification-based testing and
relates formal specification techniques to standard software testing
techniques. Both functional as well as structural testing methods
will be covered. The contents includes
- Introduction to Issues in Testing
- The Oracle Problem
- Specification Styles
- Boundary Value Testing
- Equivalence Class Testing
- Robustness Equivalence Class Testing
- Decision Table-Based Testing
- Test Sequencing
- Algebraic Testing
- Path Testing
- Data Flow Testing
- Mutation Testing
- Industrial Experiences
- Pu Geguang, UNU-IIST Fellow from Peking University
15:00, 17 December 2003
Title: An Optimal Approach to Hardware/software Partitioning for Synchronous Model
Abstract: Computer aided hardware/software partitioning is one of the
key challenges in hardware/software co-design. A new approach to hardware/software partitioning for synchronous communication model will be introduced in this seminar.
We transform the partitioning into a reachability problem of timed automata. By means of an optimal
reachability algorithm, an optimal
solution can be obtained in terms of limited resources in hardware.
To relax the initial condition of the partitioning for optimization, two
algorithms are designed to explore the dependency relations
among processes in the sequential specification. Moreover, we
propose a scheduling algorithm to improve the synchronous communication
efficiency further after partitioning stage. Some experiments are conducted with model checker UPPAAL to show our approach is both effective and efficient.
- Qin Shengchao, UNU-IIST Visitor from National University of Singapore
15:00, 18 December 2003
Title: Region Inference for an Object-Oriented Language
Abstract: Region-based memory management offers several important advantages
over garbage-collected heap, including real-time performance, better
data locality and efficient use of limited memory. The concept of
regions was first introduced for a call-by-value functional language
by Tofte and Talpin, and has since been advocated for imperative and object-oriented languages. Scope memory,
a lexical variant of regions, is now a core feature in a recent
proposal on Real-Time Specification for Java (RTSJ).
Recent works in region-based programming for Java have focused on region-checking which requires manual effort in choosing regions with appropriate lifetimes. In this paper, we propose an automatic region-inference type system for a core subset of Java. To provide an inference method that is both precise and practical, we support classes and methods that are region-polymorphic; and with region-polymorphic recursion for methods. One challenging aspect of our
inference rules is to ensure safe region programming in the presence of class subtyping, method overriding and downcast operations. Our set of region inference rules can handle these object-oriented features safely, without creating
dangling references.
- Prof. He Jifeng, UNU/IIST Senior Research Fellow
10:00, 19 December 2003
Title: A Step Towards a Unified Theory for Concurrency
Abstract: A fundamental concept of any theory of concurrency is an
ordering relation, usually
called a simulation or a refinement, which enables similar concurrent
proceses to be compared in some meaningful way. Different theories
distinguish
themselves in their choice of definition for this ordering. Our aim in
unifying theories
of concurrency is to combine the merits of both kinds of oedering: the
simple proofs offered
by simulation and the wide applicability ofr refinement.
