- Ge Weimin
15:00, Janauary 14, 2005
Title: Introduction of Elearning
Abstract: Give the biref introduction about elearning, tell about the recently
work we have made about Elearning and the future work we are
planning to do.
- Dr. Elisa Baniassad, Department of Computer Science and
Engineering, The Chinese University of Hong Kong, Hong Kong
11:00, February 2, 2005
Title: Identifying Aspects in Requirements
Abstract: Aspect-orientation is a new approach for modularizing source
code. Aspects are said to "crosscut" objects, in that they allow
encapsulatio of concerns that do not align well with an object model. Typicalexamples of such concerns are logging, debugging, or synchronization. Aspect behaviour is described in separate modules, and woven into the core program during pre-compilation. Separating crosscutting concerns improves ease of development, ease of maintenance, and in some cases performance of the resultant systems.
As aspect-orientation gains in popularity, more and more people are
trying to incorporate aspect-modularization into their own systems.
If they are content to implement only the typical aspects listed
above, then they encounter few difficulties. However, to make full
use of aspect-modularization, system-specific aspects should be
identified, and aspect-oriented analysis should be introduced into the
early phases of the software lifecycle. Aspects, however, are
difficult to identify in requirements, where no object-model can be
assessed for mis-aligned concerns. This means that not all
crosscutting concerns will be modularized in design, and thus are
missed in implementation.
My work, together with Siobhan Clarke of
Trinity College Dublin, involves providing guidelines and tool support
for early-aspect identification. In this talk, I will go over what an
aspect is, how they are typically identified, and describe tools and
guidelines for identifying aspects in system requirements.
Biography:
Elisa Baniassad is an assistant professor at the Chinese University of
Hong Kong. She graduated with her Ph.D. from University of British
Columbia, Canada in 2002. She then held a National Science and
Engineering Research Council of Canada (NSERC) two-year Post Doctoral
Fellowship at Trinity College Dublin.
Elisa's work mainly focuses on identification of aspects in all lifecycle
artifacts, including requirements, design, and code. Her main research
interest is in finding ways to allow developers to view and manipulate
code along lines of abstraction that are appropriate for their own
backgrounds. Since developers are becoming more diverse, both culturally,
and in terms of technical training, flexibility in this support is
required at all levels. This pursuit involves tool development, and
empirical analysis of programmers.
- Dr. Stefano Bistarelli, Dipartimento di Scienze, Universita'
degli Studi "G.D'annunzio", di Chieti-Pescara, Italy
12:00, February 2, 2005
Title: Soft Constraints for Security
Abstract: Integrity policies and security protocols are usually defined by set of
rules describing which actions have or have not to be performed. We
describe a uniform framework to represent the security properties of
integrity and confidentiality/authentication by using the constraint
satisfaction framework. We show how the crucial goals of integrity and
confidentiality/authentication may be achieved in various forms, each of
different strength. Using soft (rather than crisp) constraints, we
develop a uniform formal notion for the two goals. They are no longer
formalized as mere yes/no properties as in the existing literature, but
gain an extra parameter, the security level. For example, different
messages can enjoy different levels of confidentiality, or a principal can
achieve different levels of authentication with different principals, or a
system can ensure a different integrity level.
BIOGRAPHY:
Dr. Stefano Bistarelli holds a PhD from University of Pisa. His PhD thesis
entitled "Soft Constraint Solving and Programming" received two important
awards: Best Italian PhD thesis in Theoretical Computer Science (awarded
by the Italian chapter of the European Association of Theoretical Computer
Science (EATCS)), and Best Italian PhD thesis in Artificial Intelligence
(awarded by the Italian Association of Artificial Intelligence (AI*IA)).
In 2001 he won Post-Doc positions at both the Mathematics and Computer
Science Department of Padova University and the Institute of Informatics
and Telematica (IIT) of the Italian National Research Council (CNR). In
September 2002 he won a permanent position as Assistant Professor at the
Science Department of Pescara University. He is also an external
researcher of the IIT-CNR.
In 2004 he published a book on soft constraints, currently the only one in
this important field. This book was published by Springer, one of the most
prestigious publishers in computer science as part of their Lecture Notes
in Computer Science series (volume 2962).
Dr. Bistarelli has recently begun to explore the applications of soft
constraints to problems in computer security, but has already built up an
impressive track record in the topic, publishing in the top journals in
computer security and well as top level Artificial Intelligence
conferences.
- Prof. Padmanabhan Krishnan, Faculty of IT, Bond University, Gold Coast, Australia
Monday and Thursday 10:00-12:00, Starting on Thursday February 3
until the end of March 2005 (no classes during the Chinese New Year week 7-11/02/2005)
Title: Software Assurance: Issues and Approaches
Abstract: Software assurance is gaining in importance for a variety of
reasons including government regulation, requirements of
enterprises etc. In this course, we aim to explore some of the
issues related to assurance. Topics include a brief overview of
the common criteria, technical issues related to threat analysis
and case studies of assurance projects.
The course will be delivered as a reading subject. In the first
few hours the basic issues and some background material will be
presented. A collection of about 25 papers will be given to all
students. All students must read all of them at a superfical level.
Based on their interests they must choose a relevant subset of papers
to read more carefully and present their findings to the rest of
the class. Examples of real systems such as secure Linux,
firewalls or Windows2000 can be explored.
- Krzysztof R. Apt, National University of Singapore, CWI and
University of Amsterdam, The Netherlands
11:00, February 18, 2005
Title: Rule-based Approach to Constraint Programming
Abstract: Rules keep appearing as a means of expressing computation and
information. Typical, relatively recent, examples are web-based
reasoning, data mining and the concept of business rules.
In this lecture we show that at various levels of abstraction
constraint programming (CP) can also be viewed as an instance of
rule-based programming. At each level this view sheds light on the
essence of CP.
In particular, at the highest level it allows us to bring CP closer to
the computation as deduction paradigm. At the lower levels it allows
us to address the issues of efficiency of computations and of
automatic generation of constraint propagation algorithms.
Short Bio:
Krzysztof R. Apt got a PhD in mathematical logic from the Polish
Academy of Sciences in Warsaw, in 1974.
He is a senior researcher at CWI, Amsterdam and Professor at the
University of Amsterdam, the Netherlands. For the past two years he
has been working at the National University of Singapore.
Apt published three books, most recently "Principles of Constraint
Programming", and fifty journal articles. He is the founder and
editor-in-chief of the ACM Transactions in Computational Logic.
Apt strongly believes that free access to scientific publishing is
both feasible and strongly desirable for the further advancement of science.
- Scott McNeil, Project Director, Global Desktop Project, 6114 LaSalle Ave 508, Oakland, California 94611, USA
15:00, March 7, 2005
Title: The Global Desktop Project: Building Technology and Communities
Abstract: For the past five years Linux has been the fastest-growing operating system in
the world, gaining new users at a rate greater than any other computer
platform. This global adoption is in part due to the open source
nature of Linux - anyone can freely access the source code to modify
and distribute. However, the vast majority of software that makes up
the Linux operating system has come from programmers based in western
countries. While access to Linux and other free software is very
beneficial to developing nations, many are missing out on what
essentially is the power of open source: technological self-determination.
In this talk I will discuss the maturation of Linux through standards,
what the last big infrastructure play for Linux is, a background on
the X Windows System, and the Global Desktop Project's efforts to grow
the number of open source software contributors in the developing world.
- Percy A. Pari Salas, UNU/IIST Fellow
15:00, March 11, 2005
Title: Test Case Generation by Specification Mutation and Constraint Solving
Abstract: Fault-based testing is a technique where testers anticipate errors in a
system under test in order to assess or generate test cases. The idea is to
have enough test cases capable of detecting these anticipated errors. This
paper presents a method of fault-based test case generation for pre- and
postcondition specifications. Here, errors are anticipated on the
specification level by mutating the pre- and postconditions. We present the
underlying theory by giving test cases a formal semantics and translate this
general testing theory to a constraint satisfaction problem. A prototype
test case generator serves to demonstrate the automatization of the method.
The current tool works with OCL specifications, but the theory and method
are general and apply to many state-based specification languages.
- Prof. Paddy Krishnan, Faculty of IT, Bond University, Gold Coast, Australia
18:00, March 16, 2005
Title: Science of Computing for School Children
Abstract: A typical IT curriculum in schools is focussed on computers rather than the principles behind the principles of computation.
The question of what is automatable and how to arrive at
automatable solutions is rarely taught.
There are number of reports which suggest that this results in
many students, especially those who are more mathematically or
scientifically minded, turning away from the scientific and
engineering aspects of IT.
This interactive seminar is aimed at both primary and secondary
school teachers who are interested in introducing the basic
concepts underlying IT in their school.
This is based on the ACM K-12 Education Task Force Curriculum
Committee's report and our personal experience in teaching both
teachers and students.
The key aspects are
- No computing resources are necessary.
- No specialist knowledge is assumed.
- Only an interest in abstract thinking and enthusiasm to teach
is required.
More details of this seminar and other relevant information is
available at
http://www.iist.unu.edu/~paddy/CSAct/
BIOGRAPHY:
Paddy Krishnan is a Professor of Computer Science at Bond
University, Australia. He is also the director of the recently
established Centre for Software Assurance. His current research
interests are in the area of security verification and model
based testing. In the past he has held positions at the University
of Canterbury, New Zealand, Siemens Research, Munich, Germany,
Aarhus University, Denmark and Texas A&M University, USA. He is
currently visiting IIST, UNU till the end of April 2005.
- Micahel J. Pont, University of Leicester, UK
15:00, March 17, 2005
Title: Time-Triggered Software Architectures for Embedded Systems
Abstract: This talk will provide an overview of current research work on
"time-triggered" (TT) software architectures in the Embedded Systems
Laboratory at the University of Leicester, UK. The focus of this work is on
"deeply embedded" systems, and typical applications are in the automotive
sector. In most cases, the systems we are concerned with must be extremely
reliable, and be produced at very low cost. The talk will consider both
single-processor designs and multi-processor (distributed) designs. No
background in embedded systems or time-triggered software will be
assumed.
- Long Quan, UNU-IIST Fellow from Peking University
15:00, March 23, 2005
Title: Use rCOS for Code Generation and Refactoring
Abstract: Relational Calculus of Object Systems (rCOS) is an object-oriented
specification language. It is includes a specification notation with
a relational model and a refinement calculus of object-oriented
designs. This talk is based on two papers: "Consistent Code
Generation from UML Models" and "Refactoring and Pattern-Directed
Refactoring: A Formal Perspective". In the first paper, we give
definitions for class diagrams and sequence diagrams in UML. Based on
these definitions, we give an algorithm for checking the consistency of a class diagram and a
sequence diagram. Furthermore, we develop an algorithm to generate
rCOS code from any given consistent class diagram and sequence
diagram. In the second paper, we formalize refactoring rules as the
refinement laws in rCOS.
We also show how some "grand-step" refinement laws can be used to formalize pattern-directed
refactorings.
- Chris George, UNU-IIST, Senior Research Fellow
16:00, April 1, 2005
Title: How to write a technical paper
Abstract: The title implies
- Bernhard K. Aichernig, UNU-IIST
14:30, April 8, 2005
Title: Fault-based Testing in UTP
Abstract: Existing theories of testing focus on verification. Their strategy is
to cover a specification or a program text to a certain degree in
order to raise the confidence in the correctness of a system under
test. We take a different approach in the sense that we present a
theory of fault-based testing. Fault-based testing uses test data
designed to demonstrate the absence of a set of pre-specified
faults. Here, the focus is on falsification. The presented theory
of testing is integrated into Hoare & He's unifying theory of
programming (UTP). As a result, new test case generation techniques
for detecting anticipated faults are obtained. The talk gives a
brief introduction to UTP and its refinement calculus and discusses
the testing concepts and techniques on this semantical basis.
BIOGRAPHY:
Dr. Bernhard K. Aichernig is a Research Fellow of UNU-IIST, the United
Nations University International Institute for Software Technology,
and an Assistant Professor of TU Graz, the Graz University of
Technology, in Austria, Europe. He is a board member of Formal Methods
Europe (FME), an international organization that promotes well-founded
techniques in software engineering. He holds a doctorate and a diploma
engineer degree from TU Graz. His research focuses on the foundations
of software engineering in order to achieve more reliable
computer-based systems. Recently, he studies the impact of Open Source
Software and its process. For further information we refer to his
homepage http://www.iist.unu.edu/~bka.
- Liu Xiaojian, UNU-IIST Fellow
16:00, April 15, 2005
Title: Modelling Component with UML
Abstract: UML20 standard gives some notations about Component, but the
relationship between component and its constituent class diagram is
still not clear.
In this talk, we will discuss a component model that intends to link the
component and its constituent object system. This will be based on several
papers that read about the following related topics:
- Notations for components
- Object system
- Trace semantics of components
- Internal interaction in an activity group
- Joseph Sifakis, Verimag, Grenoble, France
15:00, April 18, 2005
Title: Modeling Real-time Systems
Abstract: Modeling real-time systems raises non trivial problems for the
definition of usable modeling languages and the application of
model-based development approaches.
We identify key problems and present corresponding research directions
for the incremental construction of timed models for real-time systems.
We present a framework that may provide some solutions and an
associated methodology for model construction. Timed models of
real-time systems are obtained by adding timing constraints to their
application software. These constraints take into account execution
times of atomic statements, the dynamics of the external environment,
as well as quality of service requirements. The framework combines
two kinds of composition operators for timed components:
- Restriction operators which are unary operators parameterized by a
safety property. Their application on a component restricts its
behavior so as to meet the associated property. Dynamic priorities
correspond to a class of restriction operators which preserve
deadlock-freedom of their arguments.
- Parallel composition operators, parameterized by interaction
models. These models describe interactions between actions offered by
the composed components and their associated synchronization
requirements.
We show that the combination of parallel composition and restriction
operators allows compositional modeling of real-time systems, in
particular of aspects related to heterogeneous interaction and
execution, resource sharing and scheduling. Scheduling policies are
modeled by dynamic priorities. The framework supports composition of
scheduling policies and provides compositionality and composability
results for deadlock-freedom of scheduled systems.
We show applications of these results, including model-based
development of applications in Esterel and real-time Java, as well as
a partial implementation of the framework in Verimag's IF toolset.
References
Joseph Sifakis "Modeling real-time systems-challenges and work
directions" EmSoft01, LNCS 2211, Tahoe City, October 2001.
J. Sifakis, S. Tripakis, S. Yovine "Building models of real-time
systems from application software" Proceedings of the IEEE, Special
issue on modeling and design of embedded systems, 91(1):100-111, January 2003.
K. Altisen, G. Goessler, J. Sifakis "Scheduler modeling based on the
controller synthesis paradigm" Journal of Real-time Systems, Vol. 23,
pp.55-84, 2002.
- Mr Bernd Friedrich
16:00, April 22, 2005
Title: IT Project Management for Public Administration
Abstract: This seminar describes the management of e-government ICT
projects using the PRojects IN Controlled Environments (PRINCE2)
project management methodology (prince2.org.uk). PRINCE, developed by
British government, is widely recognized as a standard for ICT
projects in both public and private domains. In its second version,
PRINCE has evolved to support all kinds of projects. Various levels of
certification are available for PRINCE2.
The methodology was applied to the Nepalese Revenue Administration
Support (RAS) Project (taxtasy.net), which I managed from 1998 until
2004. The project has led to a significant increase in revenue
collection by the Nepalese government. In the course of the project,
software for income tax, value added tax and excise tax administration
was developed and implemented in the central tax department and 22 tax
offices, all connected. The seminar is illustrated with examples of
how PRINCE2 was applied throughout the RAS project.
- Professor GAO Qingshi, Institute of Intelligence, Languagues and
Computer Science, Beijing University of Sciences and Technology
10:00, April 25, 2005
Title: An Error and Shortcoming of Zadeh's Fuzzy Set Theory and A New Fuzzy
Set Theory: C-Fuzzy Set Theory
Abstract: A new fuzzy set theory, C-fuzzy set theory, is introduced in this
talk. It is a particular case of the classical set theory and not a
generalization, hence satisfies all formular of the classical set
theory. Add a limitation to C-fuzzy set that all fuzzy sets must be
"non-uniformly" each other, then it forms a family of sub-systems,
the Z-fuzzy set systems. It can be proved that the Z0-fuzzy set
system, one of Z-fuzzy set system, is equivalent to Zadeh's fuzzy
set system.
- Prof. Paddy Krishnan, UNU-IIST Visitor from Australia
16:00, April 25, 2005
Title: A Monitoring Policy Calculus
Abstract: In this talk I will present a simple calculus to demonstrate
how security policies can be specified and analysed. The policy language
is based on atomic actions which can be monitored, blocked or rewritten
to strings over the atomic actions. Policies can also be combined either
using alternatives, conjunction or via indicating a preference. This
allows for policies to change with the observed behaviour.
A formal semantics for these policies and their effect on external
behaviour will also be presented. Based on these semantics a few simple
equational rules can be developed. These rules help identify identical
policies and can also be used to detect conflict. I will also give a
number of simple examples to illustrate how the policy calculus can be
used.
- Chris George, Senior Research Fellow
10:00-13:00, 14:30-17:30, April 26-29, 2005
Title: Formal Software Development Using RAISE
Abstract: http://www.iist.unu.edu/home/Unuiist/newrh/II/2/1/1/page.html
- Dr. J W Sanders, Programming Research Group, Oxford University, UK
10:00-12:30, 15:00-17:00, May 2, 4, 9, 11, 23, 24 and 26, 2005
Title: Communicating Sequential Processes
Abstract: Concurrency is important to much of computation: from computing in the large (networks and their distributed systems-like an airline-reservation system) to computing in the small (VLSI chips and their parallel algorithms-like image-processing chips). Because of the complex manner in which coordinating components interact, we use formal methods for the specification, development and simulation of such systems.
This course introduces and uses Hoare's notation CSP (for Communicating Sequential Processes), a kind of process algebra. The syntax of CSP is shown to be natural and convenient for describing reactive state-based behaviour and for combining those behaviours in parallel. Emphasis is given to the use of laws for deciding when two behaviours are equivalent, which results in an algebraic theory of processes. But to complement that algebraic approach, a hierarchy of semantic models is studied to provide progressively more-detailed information about the way a process interacts with its environment. A system can be specified by a semantic property (at an appropriate level of abstraction) and implemented by an algebraic process meeting that property. This first part of the course is supported by a set of exercises, integral to an understanding of the material.
The last part of the course consists of case studies, worked through and presented by participants in groups, either from papers, the texts, or by applying the ideas of the course to their own work. Examples might be chosen from communicataion protocols, hardware design, deadlock analysis, real time, transaction processing, security, or a variety of design studies.
We stop short of an executable subset, FDR (for failures/divergences refinement), of CSP whose study is the subject of a further course.
- Dr. J W Sanders, Programming Research Group, Oxford University, UK
16:00, May 6 and 13, 2005
Title: Introduction to Quantum Programming
Abstract: What is quantum computation all about? Come and find out!
This seminar presents the ideas underlying the subject and shows how they can be incorporated in Formal Methods. It concentrates on computation on a single (quantum) computer, explaining the ideas from scratch. No background in physics is required, though connections is made with secondary-school physics for those who have taken it. Detail will be given of Grover's quantum search algorithm, capable of locating its target in an array of length π with high probability and worst case complexity only O(sqrt(n)), compared with the standard O(sqrt(n)) required by linear search. No prior knowledge of quantum computing is required.
Whilst largely tutorial in approach, the research contribution of this seminar shows that quantum algorithms can be specified and derived in the style of Formal Methods. This is joint work with Paolo Zuliani.
If there is sufficient interest, a second seminar will introduce distributed quantum computation, and include detail of a quantum cryptographic protocol.
- Dr. Mantis Cheng, Department of Computer Science, University of Victoria, B.C.
11:00, May 10, 2005
Title: The Great Divide (Implementing and Verifying Distributed Real Time Systems)
Abstract: To be able to verify a system, we need a rigorous behavioral and
performance model of the system. To specify the system model, we need a
formal modeling language. To implement the system, we need a practical
implementation language. In reality, the modeling language (e.g.,
Pi-Calculus) and the implementation language (e.g., C/C++) are so far apart
in semantics and expressiveness, our hope of verifying a distributed real
time system as implemented is slim. The problem is not just about
concurrency issue. We also must deal with error recovery and timing issues.
The semantics of our implementation language is so complex that relating
the implemented system to our rigorous formal model is non-trivial. In
distributed real-time control systems, one is often concerned mostly with
their communication and coordination aspects, where their data
representation aspect is not as critical. To separate these aspects from an
implementation in order to obtain an abstract behavioral model is tedious.
On the other hand, mapping an abstract behavioral model to an
implementation is just as complicated. Our great divide is how to relate
the theory (model-checking and formal methods) to our practice (building
commercial distributed real time systems).
In the talk, I will share with you our effort of working with one telecomm
company in tackling this issue. I will discuss our approach of providing a
formal semantics to a C/C++ like language for implementing distributed real
time systems. This hybrid coordination language allows us to address the
model checking issue (verification) and performance issue (timing
validation). The latter problem is crucial for commercial systems. It
doesn't matter if the system is verifiably correct; but if it cannot meet
its performance requirements as implemented, it is still useless. Our
challenge is to relate the "observations" (real time monitor) to the
"formal properties" (temporal, causal and timing).
Biography:
For the past 10 years, Dr. Cheng has been working in the areas of QoS-based
RTOS scheduler and high performance distributed real time systems. Apart
from being a technical consultant to Nortel's optical terabit routerww.iist.unu.edu/newrh/rhtoc.html
project (OPTera), he has been investigating the modelling, verification and
automated debugging issues of distributed real time systems. More recently,
he designed a concurrent coordination language, called COOL, which has a
formal semantics and is compilable into efficient C/C++ code. While at the
University of Victoria, he taught real time systems and operating systems
for over 15 years. He was also voted a "popular" professor in the UVic
Engineering Faculty in the 1999, 2000, 2001, and 2002 issues of MacLean
Magazine. Dr. Cheng was also Director and Chief Technology Officer of ACD
Systems Inc, which is the home of the ACDSee Photo Management System, from
1999 to 2001.
- Chris George, Senior Research Fellow
15:00, May 20, 2005
Title: Proof in PVS
Abstract: This is a hands-on introduction to doing proof in PVS. After a brief
account of the PVS proof system we will complete a proof arising from
the binary tree example from the recent RAISE course at UNU-IIST.
- Dr. Franck Xia, Department of Computer Science, University of Missouri-Rolla, USA
10:30, May 30, 2005
Title: An Attempt on a Seamless Semantics Theory for Software Artifacts
Abstract: In software engineering, it is fundamental to have a rigorous
understanding about the semantics of software artifacts. One problem is that specifications are often formalized in languages whose semantics
are not connected to that of programs, and it is difficult to find a mapping from specification to code that can ensure the correctness of code. In this talk, we explore the possibility of defining and reasoning about the semantics of specification and code from a programming language perspective with an appropriate level of abstraction. The challenge is that not all the semantic aspects of programs are well understood. To reach our goal, we start by identifying two semantic aspects, i.e. scope properties and control flow, which received no systematic treatment in the existing semantics theories for programming languages, and propose innovative solutions.
For OO specifications and programs, encapsulation, information hiding, and
inheritance mainly affect the scope properties of objects/methods. However, even in the programming language literature, there is
no general theory of scope. We elaborate a unified scope theory and apply it to UML specifications to demonstrate its effectiveness. With our approach, scope errors and inconsistencies in the OO specifications can be
detected early in the same way as during code compilation. In order to fully describe control flows in programs, we develop a new logic, called order logic, which enhances the semantics of Boolean logic such that the sequential order of events can be described. With the proposed order logic, the semantics of program constructs can be rigorously defined and Hoare triple can be replaced by a logic expression, enabling the discovery of interesting properties about pre- and post-conditions. Potential benefits of our semantics theory will be discussed.
BIOGRAPHY:
Franck Xia received his Ph.D. degree in Computer Science from Universite
Pierre et Marie CURIE (Paris VI), France in 1987. He worked as an independent software consultant in Paris for six years. Between 1993 and 1999, Dr. Xia was with the University of Macau. Currently, Dr. Xia is an Associate Professor of Computer Science at the University of Missouri-Rolla, Missouri, USA. His research interests include software engineering, pattern recognition, digital topology, computational geometry, and philosophy of sciences.
- Jay S. Bagga, Department of Computer Science, Ball State University, USA
16:00, 2 June, 2005
Title: Industrial Applications of Model Checking
Abstract: In this presentation we discuss a project that was carried out for City Machine Tool & Die, Inc., a company based in Muncie, Indiana, USA. The company manufactures custom designed machines for the automotive industry. Many of the machines are automated and controlled by programmable logic controller (PLC) programs. Since these machines form part of an assembly process in the automotive industry, their reliability is critical. One of the goals of City Machine was to reduce the occurrences of malfunctions in the machines caused due to defects in the controlling software. Our project involved the use of the model checking to verify certain
specifications for the machines.
We also discuss another application involving the use of the model checker SPIN to verify designs of some sequential circuits.
- Professor Dines Bjorner, Dr.h.c., MAE, MRANS, IEEE Fellow
11:00, June 3-22, 2005
Title: Miscellaneous Issues in A Software Engineering Methodology
Abstract: In nine lectures we intend to introduce a number of facets of computing science and software engineering. They are: (1) the both property- and model-oriented formalisation of what is described, prescribed or specified; (2) software engineering as properly proceeding from domain descriptions via requirements prescriptions to software specification and implementation; (3) attempts to establish domain theories, in this case for transportation; and (4) - more narrowly - Petri nets, message sequence charts (MSCs) and communicating transaction processes (CTPs).
For further information, please visit: http://www.iist.unu.edu/www/seminar/bjorner-macau.html
- Rodrigo Ramos, UNU-IIST Fellow
16:00, 9 June, 2005
Title: A Semantics for UML-RT Active Classes via Mapping into Circus
Abstract: The lack of a formal semantics for UML-RT makes it inadequate for
rigourous system development, especially if the preservation of behaviour is a major
concern when applying well-known model transformations, like refactorings and
refinements. In this paper, we propose a semantics for UML-RT active classes
through a mapping into Circus, a specification language that combines CSP, Z
and specification statements. As a consequence of the translation, we are able to
prove that model transformations preserve both static and dynamic behaviour, using
refinement laws and a relational semantics of Circus, based on the Unifying Theories
of Programming.
- Chris Peterson, Faculty of Engineering, University of Technology, Syndney
16:00, 29 June, 2005
Title: Software Project Management for Developing Countries
Abstract: Software is developed and implemented by enterprises that wish to increase their
efficiency and effectiveness. This process is often undertaken by persons who have little or no formal training in the field, particularly in developing countries. The results are frequently disadvantageous and often fatal to the enterprise. The
University of Technology, Sydney has designed a special short postgraduate program targeted at persons in developing countries who have or wish to have such software responsibility. The response to this program has proven to be significant as it provides a fast and effective approach to increasing software project management capability.
- Dr. Sebastian Brand, National University of Singapore (http://homepages.cwi.nl/ sbrand/)
16:00, Thursday, July 7, 2005
Title: A New Constraint-based Framework for Qualitative Reasoning
Abstract: We introduce a new constraint-based framework for qualitative
relational reasoning. A prime instance is spatial reasoning based on
a finite set of qualitative relations between spatial objects (such
as the cardinal directions "north", "north-west", or the topological
relations "inside", "bordering").
In our framework, in contrast to the customary approach, the
qualitative relations are modelled as constrained variables. This
choice allows to treat aspect integration, planning and qualitative
simulation in a natural way. Temporal domain knowledge is expressed
using linear temporal logic.
The entire specification is translated into a constraint satisfaction
problem which can be solved by standard constraint technology, making
specialised solvers unneeded.
- Becky Lo and Chin Tang, Microsoft Hong Kong Limited
16:00, Thursday, 7 July, 2005
Title: Briefing on Microsoft Products and Technology
Abstract: The presentation is about:
a. .Net and Windows value proposition: Technical demonstration to
showcase Windows platform and .Net capability
b. .Net and Java interoperability: Technical demonstration to show
.Net and Java interoperability based on open standard technology.
c. Microsoft eGovernment engagement case studies: To show the
experience and expertise of Microsoft in the public sector; what they
have done and what value they have provided.
d. Various technical issues: .Net and XML processing, web services
with .Net, web service security implementation in .Net, deploying .Net
applications on Linux and Apache web server.
There will be discussions after the presentation.
- Dr. Jun Pang, INRIA Futurs and LIX, Ecole Polytechnique
15:00, Thursday, July 21, 2005
Title: Cones and Foci Proof Method and its Application
Abstract: We define a cones and foci proof method, which rephrases the question
whether two system specifications are branching bisimilar in terms of
proof obligations on relations between data objects. Our method has
been formalized and proved correct using PVS. Thus we have established
a framework for mechanical protocol verification. We apply this
framwork to the sliding window size n and sequence numbers modulo
2n. We show that the sliding window protocol is branching bisimilar to
a queue of capacity 2n. The proof is given entirely on the basis of an
axiomatic theory, and was checked with the help of PVS.
(Within the process algebraic community, much effort has been spent on
analyzing sliding window protocols. Aart Middeldorp(1986) and Jacob
Brunekreef(1993) gave specifications in ACP and PSF,
respectively. Frits Vaandrager(1986), Richard Groenvled(1987, Jos van
Wamel(1992) and Marc Bezem and Jan Friso Groote(1994) manually
verified one-bit sliding window protocols, in which the size of the
sending and receiving window is one. Starting in 1990, we attempted to
prove the most complex sliding window protocol (not taking into
account additional features such as duplex message passing and
piggybacking) from Tanenbaum's 'Communication Protocols' correct
using mCRL. This turned out to be unexpectedly hard, which is shown by
the 13 years it took to complete this work.)
Short CV: Jun Pang is a postdoctoral researcher at INRIA Futurs. Before that, he
worked as a Ph.D. student at CWI and he graduated with his Ph.D. from
Free University Amsterdam in 2004. His research interests include
process algebras, formal verification and security.
Currently, he is working on probabilistic process algebras and apply
probabilistic methods for anonymity. During his Ph.D. study at CWI
Amsterdam, he has developed several verification techniques in the
setting of mCRL, and applied them to a wide range of distributed
systems, in combination of existing theorem provers or model checkers.
- Ms. Qin Ma, INRIA Rocquencourt
16:30, Thursday, 21 July, 2005
Title: Compiling Pattern Matching in Join-Patterns
Abstract: We propose an extension of the join-calculus - the applied
join-calculus, with pattern matching on algebraic data types. Our
initial motivation is twofold: to provide an intuitive semantics of
the interation between concurrency and pattern matching; to define a
practical compilation scheme from extended join-definitions into
ordinary ones plus ML pattern matching.
The new semantics is a smooth extension of the original one, since
both join-pattern matching and pattern matching rest upon classical
semi-unification (substitution). However the implementation in terms
of compilation is far more than just straightforward. More
specifically, there is a gap between (extended) join-pattern matching,
which is non-deterministic, and ML pattern matching, which is
deterministic (following the 'first-match policy'). Our solution to
this non-determinism problem relies on building a meet-lattice of
patterns to partition matching values into non-intersecting sets.
To assess the correctness of our compilation scheme, we develop a
theory of process equivalence in the applied join-calculus. We show
that the processes before and after transformation are statically
equivalent.
(Joint work with Luc Maranget at INRIA-Rocquencourt)
Short CV: Qin MA is a Ph.D. student at INRIA-Rocquencourt, MOSCOVA
project, France, and expect to graduate this September. Her research
interests mainly include: language design, formalism, and
implementation for concurrent, object-oriented, and functional
programming. In 2004, she was honored the fellowship for outstanding
Chinese students studying abroad out of a total of 13 awarded in
France.
Before her Ph.D. program in France, as the highest ranked student in
Nanjing University, China, she was honored to be the frist participant
of the joint Master's program between Nanjing University, Universite
Paris 7, and INRIA - and obtained both a Chinese Master's degree and
a French one.
- Vladimir Mencl, UNU-IIST Visiting Staff
16:00, Friday, 30 Sep, 2005
Title: Microcomponent-Based Component Controllers: A Foundation for
Component Aspects
Abstract: In this talk, I will first briefly introduce my general background
and research interests; afterwards, I will devote most of the talk
to describing results recently accepted to APSEC2005.
In most component models, a software component consists of a
functional part and a controller part. The controller part may be
extensible; however, existing component models provide no means to
capture the structure of the controller part, and therefore neither to
specify the controller part extensions.
In this talk, we describe a minimalist component model introduced to
capture the structure of the controller part, coining the term
'microcomponent' for the controller part elements. We further describe
the concept of a 'component aspect', introduced as a consistent set of
controller part extensions. Within this framwork, it is possible to
seamlessly integrate controller part extensions, applying them to the
components selected in the application's 'launch configuration'. We have
evaluated these concepts in a prototype implementation.
- Zhiming Liu, UNU-IIST Staff
16:00, Friday, 7 October, 2005
Title: Formal Component-Based Software Development --- The Need to Link
Methods and their Theories
Abstract: We report the recent progress in the development of rCOS. We discuss the goal of
component-based development and then introduce the notion of interfaces
and their semantic model called contracts. We define a component as
realization of a contract. A publication of a component only provides
a partial description of the contract that the component realizes, and
it is used for system assembling. The definitions of these notions motivate
the need of models of different views in different notations and at
different levels of abstractions. The analysis of properties of the
different views requires to link different reasoning and verification
techniques.
** rCOS: Refinement of Component and Object Systems, developed by He Jifeng,
Xiaoshan Li and Zhiming Liu
- Prof. Frantisek Plasil
15:00, Wed, 26 October, 2005
Title: Overview of behavior protocols for SOFA and Fractal software components
Abstract: The purpose of this talk is to share the experience with behavior
protocols (interaction protocols) - the component behavior
description introduced in our SOFA component model and emphasize the
key research challenges we have faced during its 6 years existence and
development. In particular, this includes the issue of finding the
'right' semantics of fulfilling the behavior contract in terms of both
horizontal (client-service) and vertical (nesting) cooperation of
components. The talk summarizes our findings published 'incrementally'
at different occasions. Our behaviour protocols are based on a
specialized process algebra, based on simple expressions defined with
the intention to make them easily readable for non-specialists. Even
though the expressions do not employ recursion, they provide
constructions for a (limited) use of nesting. Having trace-based
semantics, the specific features of the algebra include that the
parallel composition of two agents can identify a communication
error. It has the benefit that it can be decided whether (i)
incomplete bindings of components can cause an error, (ii) a faulty
architecture can work well in a given enviroment (the communication
errors in the architecture can be ignored due to the particular
(limited) use of its functionality by the environment). Key references
and other details can be found at http://nenya.ms.mff.cuni.cz
- Dr. Sun Meng, A Former UNU-IIST Fellow, Singapore National University
15:00 Thursday, 27 October, 2005
Title: On Refinement of Generic Component-based Software Architectures
Abstract: Although increasingly popular, software component techniques still lack
suitable formal foundations on top of which rigorous methodologies for the
description and analysis of software architectures could be built. This
talk aims to contribute in this direction: building on our previous work
on coalgebraic semantics, we will discuss component refinement at three
different but interrelated levels: behavioural, syntactic, i.e., relative
to component interfaces, and architectural. Software architectures are
defined through component aggregation. On the other hand, such
aggregations, no matter how large and complex they are, can also be dealt
with as components themselves, which paves the way to a discipline of
hierarchical design. In this context, the major contribution of our work
is a semantic characterization of refinement for state-based components,
parametric on a strong monad intended to capture components' behavioural
models, and the introduction of a set of rules for architectural
refinement.
Short CV: Sun Meng is a postdoc research fellow at School of Computing,
National University of Singapore. Before that, he worked as a PhD student
at School of Mathematical Science, Peking University, and as a visiting
fellow at UNU/IIST from March 2002 to June 2003. He graduated with his PhD
in January 2005. His research interests includes category theory,
coalgebra theory, formal approaches to software engineering, component
techniques and refinement calculus.
Currently, he is working on tools and techniques for model based software
debugging. During his PhD at Peking University, he developed a
heterogeneous calculus for composing component based on the coalgebraic
framework, proposed different kinds of refinement relations of generic
components modeled as coalgebras, and built a unifying semantics for
different UML models by using coalgebras.
- Joseph Okika, UNU-IIST Fellow
15:00 Thursday, 3 November, 2005
Title: TTCN-3 Testing for Industrial-Strength Development.
Abstract: This seminar presents the activities involved in model based development
of a Test Harness for a Control Software using the Electronic Control Unit
of a Marine Diesel Engine as a case study. The test harness supports the
execution of test scripts written in the Testing and Test Control Notation
version 3 (TTCN-3); a standardized language for defining test
specifications. The talk will cover the different aspects of TTCN-3 test
specification language, background, foundations and applications as well
as how it supports industry scale development.
- Prof. He Jifeng
15:00 Thursday, 10 November, 2005
Title: Linking Theories by Retraction
Abstract: Theories of concurrency can be distinguished by their choice of
pre-ordering relations to compare processes and to prove their
correctness. A link between two theories is a function L, which
maps the processes of the source theory onto those of the target
theory. Its image defines exactly the set of processes of the target
theory.
The ordering relation of the target theory is a composition of the link
L with the ordering relation of the source theory.
We will use the normal transition rules of a structured operational
semantics to define a series of linking functions:
W for weak simulation,
R for refusals,
T for trace refinement,
A for abortion,
D for divergences, etc.
We then show that each function is a retraction, in the sense that it is
idempotent, monotonic and decreasing. Finally we show thsat the composition is a
retraction as well.
The definition of a retraction ensures that
(1) the ordering of the target theory is weaker than the ordering of
the source theory;
(2) the healthiness conditions of the target theory are expressed as
fixed point equations of the form p=Lp
(3) when applied to processes of the target theory, the source ordering
and the target ordering have exactly the same meaning.
As a result, all the algebraic properties of the source theory are
preserved in the target theory
The separately defined links may be composed in a way that preserves
these important properties. In other words,
the transition systems of the alternative versions of CCS, as well as
the main standard versions of CSP, are retracts
of the universal transition system that underlies CCS
- ELJAMAL Mohamad Hani, UNU-IIST Fellow
15:00 Friday, 2 December, 2005
Title: Requirements Evolution and Impacts On Safety
Abstract: Requirements are generally considered the cornerstone of the development
of any system and system engineering, because requirements define the
design problems. Requirements engineering is a process used to provide
specifications. One specification of any systems contains highly number
of requirements. Our study is focus to operate system in safely spite of
us applying changes on the design of system and at the operational
level, because of that we must integrate the invariant properties or
safety requirements (in any specification of system) in the beginning of
development of any systems to respect these properties if we apply a
change. Many studies have focused on change analysis to identify and
characterize the causes of requirements volatility. But our aims are to
study the impact of the evolution of requirements on safety issues.
To meet our purpose we have split up the approach into three levels:/
--the first level is to know what is the type of the change request (on
design or at the operational level);
--the second level: we try to know which requirements are concerning
with the change by using a traceability model (refers to the ability to
describe and follow the life cycle of a requirement, in both a forwards
and backwards directions) for the last model of my system to give us
all links with the invariant properties;
--the third level: is to analyse if we can apply the change by analysing the invariant properties
(Safety Requirements).
- Juan Perna, UNU-IIST Fellow
15:00 Friday, 16 December, 2005
Title: Model checking RAISE specifications using SAL
Abstract: In this work we present the basic foundations for the verification by
means of model checking techniques of formal specifications expressed in
RAISE.
During this exposition, third party model checkers will be briefly
discussed and analysed for suitability under two main criteria: (a)
syntactic/semantic restrictions imposed by the model checker's language
and (b) the applied representation technique for the system (i.e.
symbolic or explicit).
Then, the selection of the Symbolic Analysis Laboratory (SAL) as the
model checking tool is justified and some RAISE syntactic constructions
are analysed for transformation into SAL. Foundations for the semantic
preservation during the translation are provided in the cases where the
justification is not a trivial one.
Finally, the design of extensions to RAISE to define transition systems
and to support temporal logic formulas is described and the tool that
implements the first version of the described translation procedure will
be also shown.